Skip to content

Commit

Permalink
chore: adapt to multiple goal linter 5 (#12560)
Browse files Browse the repository at this point in the history
Splits off the alphabetically first half of #12381 in a separate PR to help reviewing.
  • Loading branch information
adomani authored and apnelson1 committed May 12, 2024
1 parent 7694b0b commit f93d4d6
Show file tree
Hide file tree
Showing 69 changed files with 357 additions and 335 deletions.
4 changes: 2 additions & 2 deletions Mathlib/Algebra/Category/GroupCat/Colimits.lean
Original file line number Diff line number Diff line change
Expand Up @@ -296,8 +296,8 @@ noncomputable def cokernelIsoQuotient {G H : AddCommGroupCat.{u}} (f : G ⟶ H)
apply Quotient.sound
apply leftRel_apply.mpr
fconstructor
exact -x
simp only [add_zero, AddMonoidHom.map_neg]
· exact -x
· simp only [add_zero, AddMonoidHom.map_neg]
inv :=
QuotientAddGroup.lift _ (cokernel.π f) <| by
rintro _ ⟨x, rfl⟩
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Algebra/Homology/Exact.lean
Original file line number Diff line number Diff line change
Expand Up @@ -190,8 +190,8 @@ theorem exact_comp_hom_inv_comp_iff (i : B ≅ D) : Exact (f ≫ i.hom) (i.inv
theorem exact_epi_comp (hgh : Exact g h) [Epi f] : Exact (f ≫ g) h := by
refine' ⟨by simp [hgh.w], _⟩
rw [imageToKernel_comp_left]
haveI := hgh.epi
infer_instance
· haveI := hgh.epi
infer_instance
#align category_theory.exact_epi_comp CategoryTheory.exact_epi_comp

@[simp]
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Algebra/Homology/LocalCohomology.lean
Original file line number Diff line number Diff line change
Expand Up @@ -250,8 +250,8 @@ instance ideal_powers_initial [hR : IsNoetherian R R] :
-- The inclusions `J^n1 ≤ J'` and `J^n2 ≤ J'` always form a triangle, based on
-- which exponent is larger.
rcases le_total (unop j1.left) (unop j2.left) with h | h
right; exact ⟨CostructuredArrow.homMk (homOfLE h).op (AsTrue.get trivial)⟩
left; exact ⟨CostructuredArrow.homMk (homOfLE h).op (AsTrue.get trivial)⟩
· right; exact ⟨CostructuredArrow.homMk (homOfLE h).op (AsTrue.get trivial)⟩
· left; exact ⟨CostructuredArrow.homMk (homOfLE h).op (AsTrue.get trivial)⟩
#align local_cohomology.ideal_powers_initial localCohomology.ideal_powers_initial

example : HasColimitsOfSize.{0, 0, u, u + 1} (ModuleCat.{u, u} R) := inferInstance
Expand Down
6 changes: 4 additions & 2 deletions Mathlib/Algebra/Lie/Nilpotent.lean
Original file line number Diff line number Diff line change
Expand Up @@ -175,7 +175,8 @@ theorem iterate_toEndomorphism_mem_lowerCentralSeries (x : L) (m : M) (k : ℕ)
theorem iterate_toEndomorphism_mem_lowerCentralSeries₂ (x y : L) (m : M) (k : ℕ) :
(toEndomorphism R L M x ∘ₗ toEndomorphism R L M y)^[k] m ∈
lowerCentralSeries R L M (2 * k) := by
induction' k with k ih; simp
induction' k with k ih
· simp
have hk : 2 * k.succ = (2 * k + 1) + 1 := rfl
simp only [lowerCentralSeries_succ, Function.comp_apply, Function.iterate_succ', hk,
toEndomorphism_apply_apply, LinearMap.coe_comp, toEndomorphism_apply_apply]
Expand Down Expand Up @@ -860,7 +861,8 @@ variable (R A L M : Type*) [CommRing R] [LieRing L] [LieAlgebra R L]
lemma LieSubmodule.lowerCentralSeries_tensor_eq_baseChange (k : ℕ) :
lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) k =
(lowerCentralSeries R L M k).baseChange A := by
induction' k with k ih; simp
induction' k with k ih
· simp
simp only [lowerCentralSeries_succ, ih, ← baseChange_top, lie_baseChange]

instance LieModule.instIsNilpotentTensor [IsNilpotent R L M] :
Expand Down
31 changes: 16 additions & 15 deletions Mathlib/Algebra/Module/PID.lean
Original file line number Diff line number Diff line change
Expand Up @@ -93,7 +93,7 @@ theorem Submodule.exists_isInternal_prime_power_torsion_of_pid [Module.Finite R
∃ (ι : Type u) (_ : Fintype ι) (_ : DecidableEq ι) (p : ι → R) (_ : ∀ i, Irreducible <| p i)
(e : ι → ℕ), DirectSum.IsInternal fun i => torsionBy R M <| p i ^ e i := by
refine' ⟨_, _, _, _, _, _, Submodule.isInternal_prime_power_torsion_of_pid hM⟩
exact Finset.fintypeCoeSort _
· exact Finset.fintypeCoeSort _
· rintro ⟨p, hp⟩
have hP := prime_of_factor p (Multiset.mem_toFinset.mp hp)
haveI := Ideal.isPrime_of_prime hP
Expand Down Expand Up @@ -131,17 +131,18 @@ theorem p_pow_smul_lift {x y : M} {k : ℕ} (hM' : Module.IsTorsionBy R M (p ^ p
· let f :=
((R ∙ p ^ (pOrder hM y - k) * p ^ k).quotEquivOfEq _ ?_).trans
(quotTorsionOfEquivSpanSingleton R M y)
have : f.symm ⟨p ^ k • x, h⟩ ∈
R ∙ Ideal.Quotient.mk (R ∙ p ^ (pOrder hM y - k) * p ^ k) (p ^ k) := by
rw [← Quotient.torsionBy_eq_span_singleton, mem_torsionBy_iff, ← f.symm.map_smul]
convert f.symm.map_zero; ext
rw [coe_smul_of_tower, coe_mk, coe_zero, smul_smul, ← pow_add, Nat.sub_add_cancel hk, @hM' x]
· exact mem_nonZeroDivisors_of_ne_zero (pow_ne_zero _ hp.ne_zero)
rw [Submodule.mem_span_singleton] at this; obtain ⟨a, ha⟩ := this; use a
rw [f.eq_symm_apply, ← Ideal.Quotient.mk_eq_mk, ← Quotient.mk_smul] at ha
dsimp only [smul_eq_mul, LinearEquiv.trans_apply, Submodule.quotEquivOfEq_mk,
quotTorsionOfEquivSpanSingleton_apply_mk] at ha
rw [smul_smul, mul_comm]; exact congr_arg ((↑) : _ → M) ha.symm
· have : f.symm ⟨p ^ k • x, h⟩ ∈
R ∙ Ideal.Quotient.mk (R ∙ p ^ (pOrder hM y - k) * p ^ k) (p ^ k) := by
rw [← Quotient.torsionBy_eq_span_singleton, mem_torsionBy_iff, ← f.symm.map_smul]
· convert f.symm.map_zero; ext
rw [coe_smul_of_tower, coe_mk, coe_zero, smul_smul, ← pow_add, Nat.sub_add_cancel hk,
@hM' x]
· exact mem_nonZeroDivisors_of_ne_zero (pow_ne_zero _ hp.ne_zero)
rw [Submodule.mem_span_singleton] at this; obtain ⟨a, ha⟩ := this; use a
rw [f.eq_symm_apply, ← Ideal.Quotient.mk_eq_mk, ← Quotient.mk_smul] at ha
dsimp only [smul_eq_mul, LinearEquiv.trans_apply, Submodule.quotEquivOfEq_mk,
quotTorsionOfEquivSpanSingleton_apply_mk] at ha
rw [smul_smul, mul_comm]; exact congr_arg ((↑) : _ → M) ha.symm
· symm; convert Ideal.torsionOf_eq_span_pow_pOrder hp hM y
rw [← pow_add, Nat.sub_add_cancel hk]
· use 0
Expand Down Expand Up @@ -188,9 +189,9 @@ theorem torsion_by_prime_power_decomposition (hN : Module.IsTorsion' N (Submonoi
-- Porting note(https://github.com/leanprover-community/mathlib4/issues/5732):
-- `obtain` doesn't work with placeholders.
have := IH ?_ s' ?_
obtain ⟨k, ⟨f⟩⟩ := this
clear IH
· have : ∀ i : Fin d,
· obtain ⟨k, ⟨f⟩⟩ := this
clear IH
have : ∀ i : Fin d,
∃ x : N, p ^ k i • x = 0 ∧ f (Submodule.Quotient.mk x) = DirectSum.lof R _ _ i 1 := by
intro i
let fi := f.symm.toLinearMap.comp (DirectSum.lof _ _ _ i)
Expand Down
10 changes: 5 additions & 5 deletions Mathlib/Algebra/Module/Torsion.lean
Original file line number Diff line number Diff line change
Expand Up @@ -442,11 +442,11 @@ theorem iSup_torsionBy_eq_torsionBy_prod :
rw [← torsionBySet_span_singleton_eq, Ideal.submodule_span_eq, ←
Ideal.finset_inf_span_singleton _ _ hq, Finset.inf_eq_iInf, ←
iSup_torsionBySet_ideal_eq_torsionBySet_iInf]
congr
ext : 1
congr
ext : 1
exact (torsionBySet_span_singleton_eq _).symm
· congr
ext : 1
congr
ext : 1
exact (torsionBySet_span_singleton_eq _).symm
exact fun i hi j hj ij => (Ideal.sup_eq_top_iff_isCoprime _ _).mpr (hq hi hj ij)
#align submodule.supr_torsion_by_eq_torsion_by_prod Submodule.iSup_torsionBy_eq_torsionBy_prod

Expand Down
8 changes: 4 additions & 4 deletions Mathlib/Algebra/Order/Archimedean.lean
Original file line number Diff line number Diff line change
Expand Up @@ -291,10 +291,10 @@ theorem exists_rat_btwn {x y : α} (h : x < y) : ∃ q : ℚ, x < q ∧ (q : α)
have n0' := (inv_pos.2 (sub_pos.2 h)).trans nh
have n0 := Nat.cast_pos.1 n0'
rw [Rat.cast_div_of_ne_zero, Rat.cast_natCast, Rat.cast_intCast, div_lt_iff n0']
refine' ⟨(lt_div_iff n0').2 <| (lt_iff_lt_of_le_iff_le (zh _)).1 (lt_add_one _), _⟩
rw [Int.cast_add, Int.cast_one]
refine' lt_of_le_of_lt (add_le_add_right ((zh _).1 le_rfl) _) _
rwa [← lt_sub_iff_add_lt', ← sub_mul, ← div_lt_iff' (sub_pos.2 h), one_div]
· refine' ⟨(lt_div_iff n0').2 <| (lt_iff_lt_of_le_iff_le (zh _)).1 (lt_add_one _), _⟩
rw [Int.cast_add, Int.cast_one]
refine' lt_of_le_of_lt (add_le_add_right ((zh _).1 le_rfl) _) _
rwa [← lt_sub_iff_add_lt', ← sub_mul, ← div_lt_iff' (sub_pos.2 h), one_div]
· rw [Rat.den_intCast, Nat.cast_one]
exact one_ne_zero
· intro H
Expand Down
7 changes: 4 additions & 3 deletions Mathlib/AlgebraicGeometry/StructureSheaf.lean
Original file line number Diff line number Diff line change
Expand Up @@ -762,12 +762,13 @@ theorem normalize_finite_fraction_representation (U : Opens (PrimeSpectrum.Top R
simp only []
-- Here, both sides of the equation are equal to a restriction of `s`
trans
convert congr_arg ((structureSheaf R).1.map iDj.op) (hs j).symm using 1
convert congr_arg ((structureSheaf R).1.map iDi.op) (hs i) using 1; swap
on_goal 1 =>
convert congr_arg ((structureSheaf R).1.map iDj.op) (hs j).symm using 1
convert congr_arg ((structureSheaf R).1.map iDi.op) (hs i) using 1
all_goals rw [res_const]; apply const_ext; ring
-- The remaining two goals were generated during the rewrite of `res_const`
-- These can be solved immediately
exacts [PrimeSpectrum.basicOpen_mul_le_right _ _, PrimeSpectrum.basicOpen_mul_le_left _ _]
exacts [PrimeSpectrum.basicOpen_mul_le_left _ _, PrimeSpectrum.basicOpen_mul_le_right _ _]
-- From the equality in the localization, we obtain for each `(i,j)` some power `(h i * h j) ^ n`
-- which equalizes `a i * h j` and `h i * a j`
have exists_power :
Expand Down
32 changes: 16 additions & 16 deletions Mathlib/Analysis/Analytic/Composition.lean
Original file line number Diff line number Diff line change
Expand Up @@ -391,18 +391,18 @@ theorem comp_id (p : FormalMultilinearSeries 𝕜 E F) : p.comp (id 𝕜 E) = p
ext1 n
dsimp [FormalMultilinearSeries.comp]
rw [Finset.sum_eq_single (Composition.ones n)]
show compAlongComposition p (id 𝕜 E) (Composition.ones n) = p n
· ext v
· show compAlongComposition p (id 𝕜 E) (Composition.ones n) = p n
ext v
rw [compAlongComposition_apply]
apply p.congr (Composition.ones_length n)
intros
rw [applyComposition_ones]
refine' congr_arg v _
rw [Fin.ext_iff, Fin.coe_castLE, Fin.val_mk]
show
· show
∀ b : Composition n,
b ∈ Finset.univ → b ≠ Composition.ones n → compAlongComposition p (id 𝕜 E) b = 0
· intro b _ hb
intro b _ hb
obtain ⟨k, hk, lt_k⟩ : ∃ (k : ℕ), k ∈ Composition.blocks b ∧ 1 < k :=
Composition.ne_ones_iff.1 hb
obtain ⟨i, hi⟩ : ∃ (i : Fin b.blocks.length), b.blocks.get i = k :=
Expand Down Expand Up @@ -430,16 +430,16 @@ theorem id_comp (p : FormalMultilinearSeries 𝕜 E F) (h : p 0 = 0) : (id 𝕜
· dsimp [FormalMultilinearSeries.comp]
have n_pos : 0 < n := bot_lt_iff_ne_bot.mpr hn
rw [Finset.sum_eq_single (Composition.single n n_pos)]
show compAlongComposition (id 𝕜 F) p (Composition.single n n_pos) = p n
· ext v
· show compAlongComposition (id 𝕜 F) p (Composition.single n n_pos) = p n
ext v
rw [compAlongComposition_apply, id_apply_one' _ _ (Composition.single_length n_pos)]
dsimp [applyComposition]
refine' p.congr rfl fun i him hin => congr_arg v <| _
ext; simp
show
· show
∀ b : Composition n,
b ∈ Finset.univ → b ≠ Composition.single n n_pos → compAlongComposition (id 𝕜 F) p b = 0
· intro b _ hb
intro b _ hb
have A : b.length ≠ 1 := by simpa [Composition.eq_single_iff_length] using hb
ext v
rw [compAlongComposition_apply, id_apply_ne_one _ _ A]
Expand Down Expand Up @@ -1144,14 +1144,14 @@ def sigmaEquivSigmaPi (n : ℕ) :
simp only [map_ofFn]
rfl
· rw [Fin.heq_fun_iff]
intro i
dsimp [Composition.sigmaCompositionAux]
rw [get_of_eq (splitWrtComposition_join _ _ _)]
· simp only [get_ofFn]
rfl
· simp only [map_ofFn]
rfl
· congr
· intro i
dsimp [Composition.sigmaCompositionAux]
rw [get_of_eq (splitWrtComposition_join _ _ _)]
· simp only [get_ofFn]
rfl
· simp only [map_ofFn]
rfl
· congr
#align composition.sigma_equiv_sigma_pi Composition.sigmaEquivSigmaPi

end Composition
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Analysis/Calculus/Deriv/Slope.lean
Original file line number Diff line number Diff line change
Expand Up @@ -129,7 +129,7 @@ theorem range_derivWithin_subset_closure_span_image
suffices A : f x ∈ closure (f '' (s ∩ t)) from
closure_mono (image_subset _ (inter_subset_right _ _)) A
apply ContinuousWithinAt.mem_closure_image
apply H'.continuousWithinAt.mono (inter_subset_left _ _)
· apply H'.continuousWithinAt.mono (inter_subset_left _ _)
rw [mem_closure_iff_nhdsWithin_neBot]
exact I.mono (nhdsWithin_mono _ (diff_subset _ _))

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -236,7 +236,10 @@ theorem surjOn_closedBall_of_nonlinearRightInverse (hf : ApproximatesLinearOn f
_ ≤ f'symm.nnnorm * dist (f (u n)) y + dist (u n) b := add_le_add (A _) le_rfl
_ ≤ f'symm.nnnorm * (((c : ℝ) * f'symm.nnnorm) ^ n * dist (f b) y) +
f'symm.nnnorm * (1 - ((c : ℝ) * f'symm.nnnorm) ^ n) / (1 - c * f'symm.nnnorm) *
dist (f b) y := by gcongr; exact IH.1; exact IH.2
dist (f b) y := by
gcongr
· exact IH.1
· exact IH.2
_ = f'symm.nnnorm * (1 - ((c : ℝ) * f'symm.nnnorm) ^ n.succ) /
(1 - (c : ℝ) * f'symm.nnnorm) * dist (f b) y := by
field_simp [Jcf', pow_succ]; ring
Expand Down
8 changes: 4 additions & 4 deletions Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -88,12 +88,12 @@ theorem mem_posTangentConeAt_of_segment_subset {s : Set E} {x y : E} (h : segmen
let c := fun n : ℕ => (2 : ℝ) ^ n
let d := fun n : ℕ => (c n)⁻¹ • (y - x)
refine' ⟨c, d, Filter.univ_mem' fun n => h _, tendsto_pow_atTop_atTop_of_one_lt one_lt_two, _⟩
show x + d n ∈ segment ℝ x y
· rw [segment_eq_image']
· show x + d n ∈ segment ℝ x y
rw [segment_eq_image']
refine' ⟨(c n)⁻¹, ⟨_, _⟩, rfl⟩
exacts [inv_nonneg.2 (pow_nonneg zero_le_two _), inv_le_one (one_le_pow_of_one_le one_le_two _)]
show Tendsto (fun n => c n • d n) atTop (𝓝 (y - x))
· exact tendsto_const_nhds.congr fun n ↦ (smul_inv_smul₀ (pow_ne_zero _ two_ne_zero) _).symm
· show Tendsto (fun n => c n • d n) atTop (𝓝 (y - x))
exact tendsto_const_nhds.congr fun n ↦ (smul_inv_smul₀ (pow_ne_zero _ two_ne_zero) _).symm
#align mem_pos_tangent_cone_at_of_segment_subset mem_posTangentConeAt_of_segment_subset

theorem mem_posTangentConeAt_of_segment_subset' {s : Set E} {x y : E}
Expand Down
8 changes: 4 additions & 4 deletions Mathlib/Analysis/Calculus/TangentCone.lean
Original file line number Diff line number Diff line change
Expand Up @@ -150,8 +150,8 @@ theorem subset_tangentCone_prod_left {t : Set F} {y : F} (ht : y ∈ closure t)
exact ⟨z - y, by simpa using hzt, by simpa using hz⟩
choose d' hd' using this
refine' ⟨c, fun n => (d n, d' n), _, hc, _⟩
show ∀ᶠ n in atTop, (x, y) + (d n, d' n) ∈ s ×ˢ t
· filter_upwards [hd] with n hn
· show ∀ᶠ n in atTop, (x, y) + (d n, d' n) ∈ s ×ˢ t
filter_upwards [hd] with n hn
simp [hn, (hd' n).1]
· apply Tendsto.prod_mk_nhds hy _
refine' squeeze_zero_norm (fun n => (hd' n).2.le) _
Expand All @@ -170,8 +170,8 @@ theorem subset_tangentCone_prod_right {t : Set F} {y : F} (hs : x ∈ closure s)
exact ⟨z - x, by simpa using hzs, by simpa using hz⟩
choose d' hd' using this
refine' ⟨c, fun n => (d' n, d n), _, hc, _⟩
show ∀ᶠ n in atTop, (x, y) + (d' n, d n) ∈ s ×ˢ t
· filter_upwards [hd] with n hn
· show ∀ᶠ n in atTop, (x, y) + (d' n, d n) ∈ s ×ˢ t
filter_upwards [hd] with n hn
simp [hn, (hd' n).1]
· apply Tendsto.prod_mk_nhds _ hy
refine' squeeze_zero_norm (fun n => (hd' n).2.le) _
Expand Down
3 changes: 2 additions & 1 deletion Mathlib/Analysis/InnerProductSpace/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -1590,7 +1590,8 @@ theorem norm_inner_eq_norm_tfae (x y : E) :
sub_eq_zero] at h
rw [div_eq_inv_mul, mul_smul, h, inv_smul_smul₀]
rwa [inner_self_ne_zero]
tfae_have 23; exact fun h => h.imp_right fun h' => ⟨_, h'⟩
tfae_have 23
· exact fun h => h.imp_right fun h' => ⟨_, h'⟩
tfae_have 31
· rintro (rfl | ⟨r, rfl⟩) <;>
simp [inner_smul_right, norm_smul, inner_self_eq_norm_sq_to_K, inner_self_eq_norm_mul_norm,
Expand Down
Loading

0 comments on commit f93d4d6

Please sign in to comment.