Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - chore: adapt to multiple goal linter 5 #12560

Closed
wants to merge 6 commits into from
Closed
Show file tree
Hide file tree
Changes from 2 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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 @@ -189,8 +189,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 @@ -189,9 +190,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 @@ -447,11 +447,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 @@ -393,18 +393,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 @@ -432,16 +432,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 @@ -1146,14 +1146,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 2 → 3; exact fun h => h.imp_right fun h' => ⟨_, h'⟩
tfae_have 2 → 3
· exact fun h => h.imp_right fun h' => ⟨_, h'⟩
tfae_have 3 → 1
· 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
Loading