Skip to content

Commit

Permalink
chore: adapt to multiple goal linter 3 (#12372)
Browse files Browse the repository at this point in the history
A PR analogous to #12338 and #12361: reformatting proofs following the multiple goals linter of #12339.
  • Loading branch information
adomani committed Apr 30, 2024
1 parent 335470e commit ce2e171
Show file tree
Hide file tree
Showing 92 changed files with 484 additions and 424 deletions.
20 changes: 10 additions & 10 deletions Mathlib/Algebra/Algebra/Spectrum.lean
Original file line number Diff line number Diff line change
Expand Up @@ -248,14 +248,14 @@ theorem unit_smul_eq_smul (a : A) (r : Rˣ) : σ (r • a) = r • σ a := by
theorem unit_mem_mul_iff_mem_swap_mul {a b : A} {r : Rˣ} : ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a) := by
have h₁ : ∀ x y : A, IsUnit (1 - x * y) → IsUnit (1 - y * x) := by
refine' fun x y h => ⟨⟨1 - y * x, 1 + y * h.unit.inv * x, _, _⟩, rfl⟩
calc
(1 - y * x) * (1 + y * (IsUnit.unit h).inv * x) =
1 - y * x + y * ((1 - x * y) * h.unit.inv) * x := by noncomm_ring
_ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.mul_val_inv, mul_one, sub_add_cancel]
calc
(1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) =
1 - y * x + y * (h.unit.inv * (1 - x * y)) * x := by noncomm_ring
_ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.val_inv_mul, mul_one, sub_add_cancel]
· calc
(1 - y * x) * (1 + y * (IsUnit.unit h).inv * x) =
1 - y * x + y * ((1 - x * y) * h.unit.inv) * x := by noncomm_ring
_ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.mul_val_inv, mul_one, sub_add_cancel]
· calc
(1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) =
1 - y * x + y * (h.unit.inv * (1 - x * y)) * x := by noncomm_ring
_ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.val_inv_mul, mul_one, sub_add_cancel]
have := Iff.intro (h₁ (r⁻¹ • a) b) (h₁ b (r⁻¹ • a))
rw [mul_smul_comm r⁻¹ b a] at this
simpa only [mem_iff, not_iff_not, Algebra.algebraMap_eq_smul_one, ← Units.smul_def,
Expand Down Expand Up @@ -484,8 +484,8 @@ variable [IsScalarTower R S A] {a : A} {f : S → R} (h : SpectrumRestricts a f)

theorem algebraMap_image : algebraMap R S '' spectrum R a = spectrum S a := by
refine' Set.eq_of_subset_of_subset _ fun s hs => ⟨f s, _⟩
simpa only [spectrum.preimage_algebraMap] using
(spectrum S a).image_preimage_subset (algebraMap R S)
· simpa only [spectrum.preimage_algebraMap] using
(spectrum S a).image_preimage_subset (algebraMap R S)
exact ⟨spectrum.of_algebraMap_mem S ((h.rightInvOn hs).symm ▸ hs), h.rightInvOn hs⟩

theorem image : f '' spectrum S a = spectrum R a := by
Expand Down
6 changes: 4 additions & 2 deletions Mathlib/Algebra/Category/ModuleCat/Images.lean
Original file line number Diff line number Diff line change
Expand Up @@ -63,13 +63,15 @@ variable {f}
noncomputable def image.lift (F' : MonoFactorisation f) : image f ⟶ F'.I where
toFun := (fun x => F'.e (Classical.indefiniteDescription _ x.2).1 : image f → F'.I)
map_add' x y := by
apply (mono_iff_injective F'.m).1; infer_instance
apply (mono_iff_injective F'.m).1
· infer_instance
rw [LinearMap.map_add]
change (F'.e ≫ F'.m) _ = (F'.e ≫ F'.m) _ + (F'.e ≫ F'.m) _
simp_rw [F'.fac, (Classical.indefiniteDescription (fun z => f z = _) _).2]
rfl
map_smul' c x := by
apply (mono_iff_injective F'.m).1; infer_instance
apply (mono_iff_injective F'.m).1
· infer_instance
rw [LinearMap.map_smul]
change (F'.e ≫ F'.m) _ = _ • (F'.e ≫ F'.m) _
simp_rw [F'.fac, (Classical.indefiniteDescription (fun z => f z = _) _).2]
Expand Down
3 changes: 2 additions & 1 deletion Mathlib/Algebra/CharP/Quotient.lean
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,8 @@ end CharP
theorem Ideal.Quotient.index_eq_zero {R : Type*} [CommRing R] (I : Ideal R) :
(↑I.toAddSubgroup.index : R ⧸ I) = 0 := by
rw [AddSubgroup.index, Nat.card_eq]
split_ifs with hq; swap; simp
split_ifs with hq; swap
· simp
letI : Fintype (R ⧸ I) := @Fintype.ofFinite _ hq
exact CharP.cast_card_eq_zero (R ⧸ I)
#align ideal.quotient.index_eq_zero Ideal.Quotient.index_eq_zero
37 changes: 20 additions & 17 deletions Mathlib/Algebra/DirectLimit.lean
Original file line number Diff line number Diff line change
Expand Up @@ -706,14 +706,15 @@ theorem of.zero_exact_aux [Nonempty ι] [IsDirected ι (· ≤ ·)] {x : FreeCom
isSupported_sub (isSupported_of.2 <| Or.inr rfl) (isSupported_of.2 <| Or.inl rfl),
fun [_] => _⟩
· rintro k (rfl | ⟨rfl | _⟩)
exact hij
rfl
· exact hij
· rfl
· rw [(restriction _).map_sub, RingHom.map_sub, restriction_of, dif_pos,
restriction_of, dif_pos, lift_of, lift_of]
dsimp only
have := DirectedSystem.map_map (fun i j h => f' i j h) hij (le_refl j : j ≤ j)
rw [this]
exact sub_self _
on_goal 1 =>
dsimp only
have := DirectedSystem.map_map (fun i j h => f' i j h) hij (le_refl j : j ≤ j)
rw [this]
· exact sub_self _
exacts [Or.inl rfl, Or.inr rfl]
· refine' ⟨i, {⟨i, 1⟩}, _, isSupported_sub (isSupported_of.2 rfl) isSupported_one, fun [_] => _⟩
· rintro k (rfl | h)
Expand All @@ -732,9 +733,10 @@ theorem of.zero_exact_aux [Nonempty ι] [IsDirected ι (· ≤ ·)] {x : FreeCom
· rw [(restriction _).map_sub, (restriction _).map_add, restriction_of, restriction_of,
restriction_of, dif_pos, dif_pos, dif_pos, RingHom.map_sub,
(FreeCommRing.lift _).map_add, lift_of, lift_of, lift_of]
dsimp only
rw [(f' i i _).map_add]
exact sub_self _
on_goal 1 =>
dsimp only
rw [(f' i i _).map_add]
· exact sub_self _
all_goals tauto
· refine'
⟨i, {⟨i, x * y⟩, ⟨i, x⟩, ⟨i, y⟩}, _,
Expand All @@ -745,9 +747,10 @@ theorem of.zero_exact_aux [Nonempty ι] [IsDirected ι (· ≤ ·)] {x : FreeCom
· rw [(restriction _).map_sub, (restriction _).map_mul, restriction_of, restriction_of,
restriction_of, dif_pos, dif_pos, dif_pos, RingHom.map_sub,
(FreeCommRing.lift _).map_mul, lift_of, lift_of, lift_of]
dsimp only
rw [(f' i i _).map_mul]
exact sub_self _
on_goal 1 =>
dsimp only
rw [(f' i i _).map_mul]
· exact sub_self _
all_goals tauto
-- Porting note: was
--exacts [sub_self _, Or.inl rfl, Or.inr (Or.inr rfl), Or.inr (Or.inl rfl)]
Expand All @@ -759,8 +762,8 @@ theorem of.zero_exact_aux [Nonempty ι] [IsDirected ι (· ≤ ·)] {x : FreeCom
obtain ⟨k, hik, hjk⟩ := exists_ge_ge i j
have : ∀ z : Σi, G i, z ∈ s ∪ t → z.1 ≤ k := by
rintro z (hz | hz)
exact le_trans (hi z hz) hik
exact le_trans (hj z hz) hjk
· exact le_trans (hi z hz) hik
· exact le_trans (hj z hz) hjk
refine'
⟨k, s ∪ t, this,
isSupported_add (isSupported_upwards hxs <| Set.subset_union_left s t)
Expand Down Expand Up @@ -971,9 +974,9 @@ instance nontrivial [DirectedSystem G fun i j h => f' i j h] :
Nonempty.elim (by infer_instance) fun i : ι => by
change (0 : Ring.DirectLimit G fun i j h => f' i j h) ≠ 1
rw [← (Ring.DirectLimit.of _ _ _).map_one]
intro H; rcases Ring.DirectLimit.of.zero_exact H.symm with ⟨j, hij, hf⟩
rw [(f' i j hij).map_one] at hf
exact one_ne_zero hf⟩⟩
· intro H; rcases Ring.DirectLimit.of.zero_exact H.symm with ⟨j, hij, hf⟩
rw [(f' i j hij).map_one] at hf
exact one_ne_zero hf⟩⟩
#align field.direct_limit.nontrivial Field.DirectLimit.nontrivial

theorem exists_inv {p : Ring.DirectLimit G f} : p ≠ 0 → ∃ y, p * y = 1 :=
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Algebra/DirectSum/Internal.lean
Original file line number Diff line number Diff line change
Expand Up @@ -187,7 +187,7 @@ theorem coe_of_mul_apply_aux [AddMonoid ι] [SetLike.GradedMonoid A] {i : ι} (r
exact DFinsupp.sum_zero
simp_rw [DFinsupp.sum, H, Finset.sum_ite_eq']
split_ifs with h
rfl
· rfl
rw [DFinsupp.not_mem_support_iff.mp h, ZeroMemClass.coe_zero, mul_zero]
#align direct_sum.coe_of_mul_apply_aux DirectSum.coe_of_mul_apply_aux

Expand All @@ -202,7 +202,7 @@ theorem coe_mul_of_apply_aux [AddMonoid ι] [SetLike.GradedMonoid A] (r : ⨁ i,
exact DFinsupp.sum_zero
simp_rw [DFinsupp.sum, H, Finset.sum_ite_eq']
split_ifs with h
rfl
· rfl
rw [DFinsupp.not_mem_support_iff.mp h, ZeroMemClass.coe_zero, zero_mul]
#align direct_sum.coe_mul_of_apply_aux DirectSum.coe_mul_of_apply_aux

Expand Down
28 changes: 18 additions & 10 deletions Mathlib/Algebra/Group/UniqueProds.lean
Original file line number Diff line number Diff line change
Expand Up @@ -123,7 +123,9 @@ theorem iff_card_le_one [DecidableEq G] (ha0 : a0 ∈ A) (hb0 : b0 ∈ B) :
simp_rw [card_le_one_iff, mem_filter, mem_product]
refine ⟨fun h p1 p2 ⟨⟨ha1, hb1⟩, he1⟩ ⟨⟨ha2, hb2⟩, he2⟩ ↦ ?_, fun h a b ha hb he ↦ ?_⟩
· have h1 := h ha1 hb1 he1; have h2 := h ha2 hb2 he2
ext; rw [h1.1, h2.1]; rw [h1.2, h2.2]
ext
· rw [h1.1, h2.1]
· rw [h1.2, h2.2]
· exact Prod.ext_iff.1 (@h (a, b) (a0, b0) ⟨⟨ha, hb⟩, he⟩ ⟨⟨ha0, hb0⟩, rfl⟩)

-- Porting note: mathport warning: expanding binder collection
Expand Down Expand Up @@ -407,8 +409,8 @@ open MulOpposite in
obtain ⟨a0, ha0, rfl⟩ := mem_map.mp hc
obtain ⟨b0, hb0, rfl⟩ := mem_map.mp hd
refine ⟨(_, _), ⟨ha0, hb0⟩, (a, b), ⟨ha, hb⟩, ?_, fun a' b' ha' hb' he => ?_, hu⟩
simp_rw [Function.Embedding.coeFn_mk, Ne, inv_mul_eq_one, mul_inv_eq_one] at hne
· rwa [Ne, Prod.mk.inj_iff, not_and_or, eq_comm]
· simp_rw [Function.Embedding.coeFn_mk, Ne, inv_mul_eq_one, mul_inv_eq_one] at hne
rwa [Ne, Prod.mk.inj_iff, not_and_or, eq_comm]
specialize hu' (mem_map_of_mem _ ha') (mem_map_of_mem _ hb')
simp_rw [Function.Embedding.coeFn_mk, mul_left_cancel_iff, mul_right_cancel_iff] at hu'
rw [mul_assoc, ← mul_assoc a', he, mul_assoc, mul_assoc] at hu'
Expand Down Expand Up @@ -458,8 +460,10 @@ open UniqueMul in
let A' := A.filter (· i = ai); let B' := B.filter (· i = bi)
obtain ⟨a0, ha0, b0, hb0, hu⟩ : ∃ a0 ∈ A', ∃ b0 ∈ B', UniqueMul A' B' a0 b0
· rcases hc with hc | hc; · exact ihA A' (hc.2 ai) hA hB
by_cases hA' : A' = A; rw [hA']
exacts [ihB B' (hc.2 bi) hB, ihA A' ((A.filter_subset _).ssubset_of_ne hA') hA hB]
by_cases hA' : A' = A
· rw [hA']
exact ihB B' (hc.2 bi) hB
· exact ihA A' ((A.filter_subset _).ssubset_of_ne hA') hA hB
rw [mem_filter] at ha0 hb0
exact ⟨a0, ha0.1, b0, hb0.1, of_image_filter (Pi.evalMulHom G i) ha0.2 hb0.2 hi hu⟩

Expand Down Expand Up @@ -531,7 +535,7 @@ theorem _root_.MulEquiv.twoUniqueProds_iff (f : G ≃* H) : TwoUniqueProds G ↔
⟨card_pos.2 (hA.image _), card_pos.2 (hB.image _), hc.imp And.left And.left⟩)
simp_rw [mem_product, mem_image, ← filter_nonempty_iff] at h1 h2
replace h1 := uniqueMul_of_twoUniqueMul ?_ h1.1 h1.2
replace h2 := uniqueMul_of_twoUniqueMul ?_ h2.1 h2.2
on_goal 1 => replace h2 := uniqueMul_of_twoUniqueMul ?_ h2.1 h2.2

· obtain ⟨a1, ha1, b1, hb1, hu1⟩ := h1
obtain ⟨a2, ha2, b2, hb2, hu2⟩ := h2
Expand All @@ -543,10 +547,14 @@ theorem _root_.MulEquiv.twoUniqueProds_iff (f : G ≃* H) : TwoUniqueProds G ↔
contrapose! hne; rw [Prod.mk.inj_iff] at hne ⊢
rw [← ha1.2, ← hb1.2, ← ha2.2, ← hb2.2, hne.1, hne.2]; exact ⟨rfl, rfl⟩
all_goals rcases hc with hc | hc; · exact ihA _ (hc.2 _)
· by_cases hA : A.filter (· i = p2.1) = A; rw [hA]
exacts [ihB _ (hc.2 _), ihA _ ((A.filter_subset _).ssubset_of_ne hA)]
· by_cases hA : A.filter (· i = p1.1) = A; rw [hA]
exacts [ihB _ (hc.2 _), ihA _ ((A.filter_subset _).ssubset_of_ne hA)]
· by_cases hA : A.filter (· i = p2.1) = A
· rw [hA]
exact ihB _ (hc.2 _)
· exact ihA _ ((A.filter_subset _).ssubset_of_ne hA)
· by_cases hA : A.filter (· i = p1.1) = A
· rw [hA]
exact ihB _ (hc.2 _)
· exact ihA _ ((A.filter_subset _).ssubset_of_ne hA)

open ULift in
@[to_additive] instance [TwoUniqueProds G] [TwoUniqueProds H] : TwoUniqueProds (G × H) := by
Expand Down
6 changes: 4 additions & 2 deletions Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
Original file line number Diff line number Diff line change
Expand Up @@ -468,8 +468,10 @@ variable {F G R}
δ_smul ..

lemma δ (n₀ n₁ n₂ : ℤ) (z : Cochain F G n₀) : δ n₁ n₂ (δ n₀ n₁ z) = 0 := by
by_cases h₁₂ : n₁ + 1 = n₂; swap; rw [δ_shape _ _ h₁₂]
by_cases h₀₁ : n₀ + 1 = n₁; swap; rw [δ_shape _ _ h₀₁, δ_zero]
by_cases h₁₂ : n₁ + 1 = n₂; swap
· rw [δ_shape _ _ h₁₂]
by_cases h₀₁ : n₀ + 1 = n₁; swap
· rw [δ_shape _ _ h₀₁, δ_zero]
ext p q hpq
dsimp
simp only [δ_v n₁ n₂ h₁₂ _ p q hpq _ _ rfl rfl,
Expand Down
3 changes: 2 additions & 1 deletion Mathlib/Algebra/Module/LocalizedModule.lean
Original file line number Diff line number Diff line change
Expand Up @@ -254,7 +254,8 @@ instance {A : Type*} [Semiring A] [Algebra R A] {S : Submonoid R} :
dsimp only at e₁ e₂ ⊢
rw [eq_comm]
trans (u₁ • t₁ • a₁) • u₂ • t₂ • a₂
rw [e₁, e₂]; swap; rw [eq_comm]
on_goal 1 => rw [e₁, e₂]
on_goal 2 => rw [eq_comm]
all_goals
rw [smul_smul, mul_mul_mul_comm, ← smul_eq_mul, ← smul_eq_mul A, smul_smul_smul_comm,
mul_smul, mul_smul])
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Algebra/MonoidAlgebra/Degree.lean
Original file line number Diff line number Diff line change
Expand Up @@ -187,8 +187,8 @@ theorem le_inf_support_multiset_prod (degt0 : 0 ≤ degt 0)
refine' OrderDual.ofDual_le_ofDual.mpr <|
sup_support_multiset_prod_le (OrderDual.ofDual_le_ofDual.mp _)
(fun a b => OrderDual.ofDual_le_ofDual.mp _) m
exact degt0
exact degtm _ _
· exact degt0
· exact degtm _ _
#align add_monoid_algebra.le_inf_support_multiset_prod AddMonoidAlgebra.le_inf_support_multiset_prod

theorem sup_support_finset_prod_le (degb0 : degb 00)
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Algebra/MonoidAlgebra/Ideal.lean
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ theorem MonoidAlgebra.mem_ideal_span_of_image [Monoid G] [Semiring k] {s : Set G
obtain ⟨d, hd, d2, rfl⟩ := hx _ hi
convert Ideal.mul_mem_left _ (id <| Finsupp.single d2 <| x (d2 * d) : MonoidAlgebra k G) _
pick_goal 3
refine' Ideal.subset_span ⟨_, hd, rfl⟩
· refine' Ideal.subset_span ⟨_, hd, rfl⟩
rw [id, MonoidAlgebra.of_apply, MonoidAlgebra.single_mul_single, mul_one]
#align monoid_algebra.mem_ideal_span_of_image MonoidAlgebra.mem_ideal_span_of_image

Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Algebra/MvPolynomial/Variables.lean
Original file line number Diff line number Diff line change
Expand Up @@ -259,7 +259,7 @@ theorem eval₂Hom_eq_constantCoeff_of_vars (f : R →+* S) {g : σ → S} {p :
rw [Finset.sum_eq_single (0 : σ →₀ ℕ)]
· rw [Finsupp.prod_zero_index, mul_one]
rfl
intro d hd hd0
on_goal 1 => intro d hd hd0
on_goal 3 =>
rw [constantCoeff_eq, coeff, ← Ne, ← Finsupp.mem_support_iff] at h0
intro
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Algebra/Polynomial/BigOperators.lean
Original file line number Diff line number Diff line change
Expand Up @@ -150,7 +150,7 @@ theorem leadingCoeff_multiset_prod' (h : (t.map leadingCoeff).prod ≠ 0) :
simp only [ne_eq]
apply right_ne_zero_of_mul h
· rw [ih]
exact h
· exact h
simp only [ne_eq, not_false_eq_true]
apply right_ne_zero_of_mul h
#align polynomial.leading_coeff_multiset_prod' Polynomial.leadingCoeff_multiset_prod'
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Algebra/Polynomial/Degree/Definitions.lean
Original file line number Diff line number Diff line change
Expand Up @@ -179,7 +179,7 @@ theorem le_degree_of_ne_zero (h : coeff p n ≠ 0) : (n : WithBot ℕ) ≤ degre

theorem le_natDegree_of_ne_zero (h : coeff p n ≠ 0) : n ≤ natDegree p := by
rw [← Nat.cast_le (α := WithBot ℕ), ← degree_eq_natDegree]
exact le_degree_of_ne_zero h
· exact le_degree_of_ne_zero h
· rintro rfl
exact h rfl
#align polynomial.le_nat_degree_of_ne_zero Polynomial.le_natDegree_of_ne_zero
Expand Down Expand Up @@ -777,7 +777,7 @@ lemma natDegree_eq_of_natDegree_add_lt_right (p q : R[X])

lemma natDegree_eq_of_natDegree_add_eq_zero (p q : R[X])
(H : natDegree (p + q) = 0) : natDegree p = natDegree q := by
by_cases h₁ : natDegree p = 0; by_cases h₂ : natDegree q = 0
by_cases h₁ : natDegree p = 0; on_goal 1 => by_cases h₂ : natDegree q = 0
· exact h₁.trans h₂.symm
· apply natDegree_eq_of_natDegree_add_lt_right; rwa [H, Nat.pos_iff_ne_zero]
· apply natDegree_eq_of_natDegree_add_lt_left; rwa [H, Nat.pos_iff_ne_zero]
Expand Down
8 changes: 4 additions & 4 deletions Mathlib/Algebra/Polynomial/Derivative.lean
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ theorem coeff_derivative (p : R[X]) (n : ℕ) :
rw [derivative_apply]
simp only [coeff_X_pow, coeff_sum, coeff_C_mul]
rw [sum, Finset.sum_eq_single (n + 1)]
simp only [Nat.add_succ_sub_one, add_zero, mul_one, if_true, eq_self_iff_true]; norm_cast
· simp only [Nat.add_succ_sub_one, add_zero, mul_one, if_true, eq_self_iff_true]; norm_cast
· intro b
cases b
· intros
Expand Down Expand Up @@ -320,9 +320,9 @@ theorem derivative_map [Semiring S] (p : R[X]) (f : R →+* S) :
let n := max p.natDegree (map f p).natDegree
rw [derivative_apply, derivative_apply]
rw [sum_over_range' _ _ (n + 1) ((le_max_left _ _).trans_lt (lt_add_one _))]
rw [sum_over_range' _ _ (n + 1) ((le_max_right _ _).trans_lt (lt_add_one _))]
simp only [Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_C, map_mul, coeff_map,
map_natCast, Polynomial.map_natCast, Polynomial.map_pow, map_X]
on_goal 1 => rw [sum_over_range' _ _ (n + 1) ((le_max_right _ _).trans_lt (lt_add_one _))]
· simp only [Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_C, map_mul, coeff_map,
map_natCast, Polynomial.map_natCast, Polynomial.map_pow, map_X]
all_goals intro n; rw [zero_mul, C_0, zero_mul]
#align polynomial.derivative_map Polynomial.derivative_map

Expand Down
3 changes: 2 additions & 1 deletion Mathlib/Algebra/Polynomial/Div.lean
Original file line number Diff line number Diff line change
Expand Up @@ -556,7 +556,8 @@ theorem rootMultiplicity_C (r a : R) : rootMultiplicity a (C r) = 0 := by
· rw [Subsingleton.elim (C r) 0, rootMultiplicity_zero]
classical
rw [rootMultiplicity_eq_multiplicity]
split_ifs with hr; rfl
split_ifs with hr
· rfl
have h : natDegree (C r) < natDegree (X - C a) := by simp
simp_rw [multiplicity.multiplicity_eq_zero.mpr ((monic_X_sub_C a).not_dvd_of_natDegree_lt hr h)]
rfl
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Algebra/Polynomial/FieldDivision.lean
Original file line number Diff line number Diff line change
Expand Up @@ -661,7 +661,7 @@ theorem irreducible_iff_degree_lt (p : R[X]) (hp0 : p ≠ 0) (hpu : ¬ IsUnit p)
Irreducible p ↔ ∀ q, q.degree ≤ ↑(natDegree p / 2) → q ∣ p → IsUnit q := by
rw [← irreducible_mul_leadingCoeff_inv,
(monic_mul_leadingCoeff_inv hp0).irreducible_iff_degree_lt]
simp [hp0, natDegree_mul_leadingCoeff_inv]
· simp [hp0, natDegree_mul_leadingCoeff_inv]
· contrapose! hpu
exact isUnit_of_mul_eq_one _ _ hpu

Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Algebra/Polynomial/Module/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -385,7 +385,7 @@ noncomputable def equivPolynomialSelf : PolynomialModule R R ≃ₗ[R[X]] R[X] :
single_apply, ge_iff_le, smul_eq_mul, Polynomial.coeff_mul, mul_ite, mul_zero]
split_ifs with hn
· rw [Finset.sum_eq_single (i - n, n)]
simp only [ite_true]
· simp only [ite_true]
· rintro ⟨p, q⟩ hpq1 hpq2
rw [Finset.mem_antidiagonal] at hpq1
split_ifs with H
Expand Down
3 changes: 2 additions & 1 deletion Mathlib/Algebra/Polynomial/Reverse.lean
Original file line number Diff line number Diff line change
Expand Up @@ -357,7 +357,8 @@ theorem coeff_one_reverse (f : R[X]) : coeff (reverse f) 1 = nextCoeff f := by
rw [commute_X p, reverse_mul_X]

@[simp] lemma reverse_mul_X_pow (p : R[X]) (n : ℕ) : reverse (p * X ^ n) = reverse p := by
induction' n with n ih; simp
induction' n with n ih
· simp
rw [pow_succ, ← mul_assoc, reverse_mul_X, ih]

@[simp] lemma reverse_X_pow_mul (p : R[X]) (n : ℕ) : reverse (X ^ n * p) = reverse p := by
Expand Down
Loading

0 comments on commit ce2e171

Please sign in to comment.