From ce2e1714243ce401c1d07f30415ec25b2075754a Mon Sep 17 00:00:00 2001 From: damiano Date: Tue, 30 Apr 2024 08:22:13 +0000 Subject: [PATCH] chore: adapt to multiple goal linter 3 (#12372) A PR analogous to #12338 and #12361: reformatting proofs following the multiple goals linter of #12339. --- Mathlib/Algebra/Algebra/Spectrum.lean | 20 +-- .../Algebra/Category/ModuleCat/Images.lean | 6 +- Mathlib/Algebra/CharP/Quotient.lean | 3 +- Mathlib/Algebra/DirectLimit.lean | 37 +++-- Mathlib/Algebra/DirectSum/Internal.lean | 4 +- Mathlib/Algebra/Group/UniqueProds.lean | 28 ++-- .../Homology/HomotopyCategory/HomComplex.lean | 6 +- Mathlib/Algebra/Module/LocalizedModule.lean | 3 +- Mathlib/Algebra/MonoidAlgebra/Degree.lean | 4 +- Mathlib/Algebra/MonoidAlgebra/Ideal.lean | 2 +- Mathlib/Algebra/MvPolynomial/Variables.lean | 2 +- Mathlib/Algebra/Polynomial/BigOperators.lean | 2 +- .../Polynomial/Degree/Definitions.lean | 4 +- Mathlib/Algebra/Polynomial/Derivative.lean | 8 +- Mathlib/Algebra/Polynomial/Div.lean | 3 +- Mathlib/Algebra/Polynomial/FieldDivision.lean | 2 +- Mathlib/Algebra/Polynomial/Module/Basic.lean | 2 +- Mathlib/Algebra/Polynomial/Reverse.lean | 3 +- Mathlib/Algebra/Polynomial/RingDivision.lean | 35 ++-- Mathlib/Algebra/Quaternion.lean | 2 +- Mathlib/Analysis/BoxIntegral/Box/Basic.lean | 9 +- .../Analysis/BoxIntegral/Partition/Basic.lean | 14 +- Mathlib/Analysis/Convex/Combination.lean | 10 +- Mathlib/Analysis/Convex/Function.lean | 10 +- Mathlib/Analysis/Convex/Mul.lean | 6 +- Mathlib/Analysis/Convex/Segment.lean | 24 +-- Mathlib/Analysis/Convex/Star.lean | 12 +- Mathlib/Analysis/Normed/Field/Basic.lean | 6 +- Mathlib/Analysis/SpecificLimits/Basic.lean | 9 +- Mathlib/CategoryTheory/Abelian/Homology.lean | 8 +- Mathlib/Combinatorics/Configuration.lean | 13 +- Mathlib/Combinatorics/Hall/Basic.lean | 4 +- Mathlib/Data/Complex/Exponential.lean | 4 +- Mathlib/Data/Nat/Squarefree.lean | 8 +- Mathlib/Data/Nat/Totient.lean | 4 +- Mathlib/Data/ZMod/Basic.lean | 4 +- .../Geometry/RingedSpace/PresheafedSpace.lean | 14 +- Mathlib/GroupTheory/Complement.lean | 6 +- Mathlib/GroupTheory/Exponent.lean | 4 +- Mathlib/GroupTheory/HNNExtension.lean | 7 +- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean | 6 +- .../GroupTheory/SpecificGroups/Dihedral.lean | 12 +- .../AffineSpace/Combination.lean | 4 +- .../AffineSpace/Independent.lean | 9 +- Mathlib/LinearAlgebra/DFinsupp.lean | 2 +- .../Dimension/StrongRankCondition.lean | 2 +- Mathlib/LinearAlgebra/FreeModule/PID.lean | 78 ++++----- .../LinearAlgebra/InvariantBasisNumber.lean | 6 +- Mathlib/LinearAlgebra/Matrix/Determinant.lean | 150 +++++++++--------- Mathlib/LinearAlgebra/Matrix/DotProduct.lean | 4 +- .../LinearAlgebra/Matrix/Transvection.lean | 13 +- Mathlib/ModelTheory/DirectLimit.lean | 4 +- Mathlib/NumberTheory/FLT/Three.lean | 3 +- Mathlib/NumberTheory/Multiplicity.lean | 4 +- Mathlib/NumberTheory/PellMatiyasevic.lean | 5 +- Mathlib/RingTheory/ChainOfDivisors.lean | 6 +- Mathlib/RingTheory/Finiteness.lean | 12 +- Mathlib/RingTheory/Ideal/IsPrimary.lean | 7 +- .../RingTheory/Localization/Away/Basic.lean | 14 +- .../RingTheory/Localization/FractionRing.lean | 10 +- Mathlib/RingTheory/Localization/Ideal.lean | 8 +- .../RingTheory/Localization/Submodule.lean | 5 +- .../RingTheory/MvPolynomial/Symmetric.lean | 16 +- .../MvPolynomial/WeightedHomogeneous.lean | 10 +- Mathlib/RingTheory/Polynomial/Basic.lean | 12 +- .../RingTheory/Polynomial/Hermite/Basic.lean | 8 +- Mathlib/RingTheory/Polynomial/Nilpotent.lean | 4 +- Mathlib/RingTheory/Polynomial/Vieta.lean | 3 +- Mathlib/RingTheory/PowerSeries/WellKnown.lean | 6 +- Mathlib/RingTheory/PrincipalIdealDomain.lean | 4 +- .../RingTheory/UniqueFactorizationDomain.lean | 2 +- Mathlib/SetTheory/Surreal/Dyadic.lean | 3 +- Mathlib/Topology/Algebra/Polynomial.lean | 4 +- Mathlib/Topology/Algebra/UniformGroup.lean | 5 +- .../Topology/Algebra/UniformMulAction.lean | 2 +- .../Category/TopCat/Limits/Pullbacks.lean | 16 +- .../Topology/Category/TopCat/OpenNhds.lean | 7 +- Mathlib/Topology/Gluing.lean | 20 +-- Mathlib/Topology/Homeomorph.lean | 5 +- Mathlib/Topology/Homotopy/HSpaces.lean | 3 +- Mathlib/Topology/IndicatorConstPointwise.lean | 4 +- Mathlib/Topology/Instances/ENNReal.lean | 8 +- Mathlib/Topology/Instances/NNReal.lean | 4 +- Mathlib/Topology/LocallyConstant/Basic.lean | 9 +- Mathlib/Topology/Order/IntermediateValue.lean | 8 +- Mathlib/Topology/Order/ScottTopology.lean | 4 +- Mathlib/Topology/Sequences.lean | 4 +- Mathlib/Topology/Sheaves/Presheaf.lean | 8 +- .../Sheaves/SheafCondition/Sites.lean | 5 +- Mathlib/Topology/StoneCech.lean | 2 +- Mathlib/Topology/UniformSpace/Cauchy.lean | 4 +- .../UniformSpace/UniformEmbedding.lean | 2 +- 92 files changed, 484 insertions(+), 424 deletions(-) diff --git a/Mathlib/Algebra/Algebra/Spectrum.lean b/Mathlib/Algebra/Algebra/Spectrum.lean index 5bf6e29f329db4..26a4f066b174df 100644 --- a/Mathlib/Algebra/Algebra/Spectrum.lean +++ b/Mathlib/Algebra/Algebra/Spectrum.lean @@ -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, @@ -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 diff --git a/Mathlib/Algebra/Category/ModuleCat/Images.lean b/Mathlib/Algebra/Category/ModuleCat/Images.lean index 726c4b9d45d408..f28644eda20a97 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Images.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Images.lean @@ -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] diff --git a/Mathlib/Algebra/CharP/Quotient.lean b/Mathlib/Algebra/CharP/Quotient.lean index e72a23cec58e7f..def99a8f0a5921 100644 --- a/Mathlib/Algebra/CharP/Quotient.lean +++ b/Mathlib/Algebra/CharP/Quotient.lean @@ -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 diff --git a/Mathlib/Algebra/DirectLimit.lean b/Mathlib/Algebra/DirectLimit.lean index 58a6753519ad88..0fbfc53ab982c8 100644 --- a/Mathlib/Algebra/DirectLimit.lean +++ b/Mathlib/Algebra/DirectLimit.lean @@ -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) @@ -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⟩}, _, @@ -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)] @@ -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) @@ -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 := diff --git a/Mathlib/Algebra/DirectSum/Internal.lean b/Mathlib/Algebra/DirectSum/Internal.lean index b19948136c8aec..1d0793c36ee8af 100644 --- a/Mathlib/Algebra/DirectSum/Internal.lean +++ b/Mathlib/Algebra/DirectSum/Internal.lean @@ -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 @@ -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 diff --git a/Mathlib/Algebra/Group/UniqueProds.lean b/Mathlib/Algebra/Group/UniqueProds.lean index c944b44b80fc34..46068af5bd5c62 100644 --- a/Mathlib/Algebra/Group/UniqueProds.lean +++ b/Mathlib/Algebra/Group/UniqueProds.lean @@ -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 @@ -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' @@ -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⟩ @@ -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 @@ -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 diff --git a/Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean b/Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean index 9d0d6b94d4de1e..97181ccb7234db 100644 --- a/Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean +++ b/Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean @@ -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, diff --git a/Mathlib/Algebra/Module/LocalizedModule.lean b/Mathlib/Algebra/Module/LocalizedModule.lean index 87ad93eff069e1..23c82379dac1c1 100644 --- a/Mathlib/Algebra/Module/LocalizedModule.lean +++ b/Mathlib/Algebra/Module/LocalizedModule.lean @@ -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]) diff --git a/Mathlib/Algebra/MonoidAlgebra/Degree.lean b/Mathlib/Algebra/MonoidAlgebra/Degree.lean index 3d22467d24758d..d95bf58f57ea78 100644 --- a/Mathlib/Algebra/MonoidAlgebra/Degree.lean +++ b/Mathlib/Algebra/MonoidAlgebra/Degree.lean @@ -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 0 ≤ 0) diff --git a/Mathlib/Algebra/MonoidAlgebra/Ideal.lean b/Mathlib/Algebra/MonoidAlgebra/Ideal.lean index b4214b2a752ff8..bdadc297c33c9c 100644 --- a/Mathlib/Algebra/MonoidAlgebra/Ideal.lean +++ b/Mathlib/Algebra/MonoidAlgebra/Ideal.lean @@ -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 diff --git a/Mathlib/Algebra/MvPolynomial/Variables.lean b/Mathlib/Algebra/MvPolynomial/Variables.lean index 96c3b647590a05..3ce959fbe949b2 100644 --- a/Mathlib/Algebra/MvPolynomial/Variables.lean +++ b/Mathlib/Algebra/MvPolynomial/Variables.lean @@ -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 diff --git a/Mathlib/Algebra/Polynomial/BigOperators.lean b/Mathlib/Algebra/Polynomial/BigOperators.lean index 2bc3dd2c5f6f60..df6ccd2d4bd41d 100644 --- a/Mathlib/Algebra/Polynomial/BigOperators.lean +++ b/Mathlib/Algebra/Polynomial/BigOperators.lean @@ -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' diff --git a/Mathlib/Algebra/Polynomial/Degree/Definitions.lean b/Mathlib/Algebra/Polynomial/Degree/Definitions.lean index ad0dbfc47bfe18..247f5fe6e09a11 100644 --- a/Mathlib/Algebra/Polynomial/Degree/Definitions.lean +++ b/Mathlib/Algebra/Polynomial/Degree/Definitions.lean @@ -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 @@ -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] diff --git a/Mathlib/Algebra/Polynomial/Derivative.lean b/Mathlib/Algebra/Polynomial/Derivative.lean index 5a88f043ca6a61..4c99d8a30c8430 100644 --- a/Mathlib/Algebra/Polynomial/Derivative.lean +++ b/Mathlib/Algebra/Polynomial/Derivative.lean @@ -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 @@ -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 diff --git a/Mathlib/Algebra/Polynomial/Div.lean b/Mathlib/Algebra/Polynomial/Div.lean index 99102ca84e12c6..5e4320a2884e8f 100644 --- a/Mathlib/Algebra/Polynomial/Div.lean +++ b/Mathlib/Algebra/Polynomial/Div.lean @@ -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 diff --git a/Mathlib/Algebra/Polynomial/FieldDivision.lean b/Mathlib/Algebra/Polynomial/FieldDivision.lean index d4b0fd98811033..8c3cac3732ce40 100644 --- a/Mathlib/Algebra/Polynomial/FieldDivision.lean +++ b/Mathlib/Algebra/Polynomial/FieldDivision.lean @@ -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 diff --git a/Mathlib/Algebra/Polynomial/Module/Basic.lean b/Mathlib/Algebra/Polynomial/Module/Basic.lean index 7e4a7152ebc89f..a4b8ed745a198e 100644 --- a/Mathlib/Algebra/Polynomial/Module/Basic.lean +++ b/Mathlib/Algebra/Polynomial/Module/Basic.lean @@ -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 diff --git a/Mathlib/Algebra/Polynomial/Reverse.lean b/Mathlib/Algebra/Polynomial/Reverse.lean index f09f2df99c46d6..e9e12c30cea691 100644 --- a/Mathlib/Algebra/Polynomial/Reverse.lean +++ b/Mathlib/Algebra/Polynomial/Reverse.lean @@ -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 diff --git a/Mathlib/Algebra/Polynomial/RingDivision.lean b/Mathlib/Algebra/Polynomial/RingDivision.lean index 8de5eeccbd7969..2ddf08e3f061e4 100644 --- a/Mathlib/Algebra/Polynomial/RingDivision.lean +++ b/Mathlib/Algebra/Polynomial/RingDivision.lean @@ -338,22 +338,23 @@ theorem Monic.not_irreducible_iff_exists_add_mul_eq_coeff (hm : p.Monic) (hnd : cases subsingleton_or_nontrivial R · simp [natDegree_of_subsingleton] at hnd rw [hm.irreducible_iff_natDegree', and_iff_right, hnd] - push_neg; constructor - · rintro ⟨a, b, ha, hb, rfl, hdb⟩ - simp only [zero_lt_two, Nat.div_self, ge_iff_le, - Nat.Ioc_succ_singleton, zero_add, mem_singleton] at hdb - have hda := hnd - rw [ha.natDegree_mul hb, hdb] at hda - use a.coeff 0, b.coeff 0, mul_coeff_zero a b - simpa only [nextCoeff, hnd, add_right_cancel hda, hdb] using ha.nextCoeff_mul hb - · rintro ⟨c₁, c₂, hmul, hadd⟩ - refine - ⟨X + C c₁, X + C c₂, monic_X_add_C _, monic_X_add_C _, ?_, ?_⟩ - · rw [p.as_sum_range_C_mul_X_pow, hnd, Finset.sum_range_succ, Finset.sum_range_succ, - Finset.sum_range_one, ← hnd, hm.coeff_natDegree, hnd, hmul, hadd, C_mul, C_add, C_1] - ring - · rw [mem_Ioc, natDegree_X_add_C _] - simp + · push_neg + constructor + · rintro ⟨a, b, ha, hb, rfl, hdb⟩ + simp only [zero_lt_two, Nat.div_self, ge_iff_le, + Nat.Ioc_succ_singleton, zero_add, mem_singleton] at hdb + have hda := hnd + rw [ha.natDegree_mul hb, hdb] at hda + use a.coeff 0, b.coeff 0, mul_coeff_zero a b + simpa only [nextCoeff, hnd, add_right_cancel hda, hdb] using ha.nextCoeff_mul hb + · rintro ⟨c₁, c₂, hmul, hadd⟩ + refine + ⟨X + C c₁, X + C c₂, monic_X_add_C _, monic_X_add_C _, ?_, ?_⟩ + · rw [p.as_sum_range_C_mul_X_pow, hnd, Finset.sum_range_succ, Finset.sum_range_succ, + Finset.sum_range_one, ← hnd, hm.coeff_natDegree, hnd, hmul, hadd, C_mul, C_add, C_1] + ring + · rw [mem_Ioc, natDegree_X_add_C _] + simp · rintro rfl simp [natDegree_one] at hnd #align polynomial.monic.not_irreducible_iff_exists_add_mul_eq_coeff Polynomial.Monic.not_irreducible_iff_exists_add_mul_eq_coeff @@ -1616,7 +1617,7 @@ theorem isUnit_of_isUnit_leadingCoeff_of_isUnit_map {f : R[X]} (hf : IsUnit f.le convert hf change coeff f 0 = coeff f (natDegree f) rw [(degree_eq_iff_natDegree_eq _).1 dz] - rfl + · rfl rintro rfl simp at H · intro h diff --git a/Mathlib/Algebra/Quaternion.lean b/Mathlib/Algebra/Quaternion.lean index 54e7b303208832..b9772b0a3db1b4 100644 --- a/Mathlib/Algebra/Quaternion.lean +++ b/Mathlib/Algebra/Quaternion.lean @@ -1297,7 +1297,7 @@ variable [LinearOrderedCommRing R] {a : ℍ[R]} theorem normSq_eq_zero : normSq a = 0 ↔ a = 0 := by refine' ⟨fun h => _, fun h => h.symm ▸ normSq.map_zero⟩ rw [normSq_def', add_eq_zero_iff', add_eq_zero_iff', add_eq_zero_iff'] at h - exact ext a 0 (pow_eq_zero h.1.1.1) (pow_eq_zero h.1.1.2) (pow_eq_zero h.1.2) (pow_eq_zero h.2) + · exact ext a 0 (pow_eq_zero h.1.1.1) (pow_eq_zero h.1.1.2) (pow_eq_zero h.1.2) (pow_eq_zero h.2) all_goals apply_rules [sq_nonneg, add_nonneg] #align quaternion.norm_sq_eq_zero Quaternion.normSq_eq_zero diff --git a/Mathlib/Analysis/BoxIntegral/Box/Basic.lean b/Mathlib/Analysis/BoxIntegral/Box/Basic.lean index 16bb22e5eec43c..88df8a1d1f9173 100644 --- a/Mathlib/Analysis/BoxIntegral/Box/Basic.lean +++ b/Mathlib/Analysis/BoxIntegral/Box/Basic.lean @@ -152,12 +152,15 @@ theorem le_def : I ≤ J ↔ ∀ x ∈ I, x ∈ J := Iff.rfl theorem le_TFAE : List.TFAE [I ≤ J, (I : Set (ι → ℝ)) ⊆ J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper] := by - tfae_have 1 ↔ 2; exact Iff.rfl + tfae_have 1 ↔ 2 + · exact Iff.rfl tfae_have 2 → 3 · intro h simpa [coe_eq_pi, closure_pi_set, lower_ne_upper] using closure_mono h - tfae_have 3 ↔ 4; exact Icc_subset_Icc_iff I.lower_le_upper - tfae_have 4 → 2; exact fun h x hx i ↦ Ioc_subset_Ioc (h.1 i) (h.2 i) (hx i) + tfae_have 3 ↔ 4 + · exact Icc_subset_Icc_iff I.lower_le_upper + tfae_have 4 → 2 + · exact fun h x hx i ↦ Ioc_subset_Ioc (h.1 i) (h.2 i) (hx i) tfae_finish #align box_integral.box.le_tfae BoxIntegral.Box.le_TFAE diff --git a/Mathlib/Analysis/BoxIntegral/Partition/Basic.lean b/Mathlib/Analysis/BoxIntegral/Partition/Basic.lean index 265d261796b5fc..d1e41003a75772 100644 --- a/Mathlib/Analysis/BoxIntegral/Partition/Basic.lean +++ b/Mathlib/Analysis/BoxIntegral/Partition/Basic.lean @@ -139,8 +139,10 @@ instance partialOrder : PartialOrder (Prepartition I) where fun π₁ π₂ h₁ h₂ => injective_boxes (Subset.antisymm (this h₁ h₂) (this h₂ h₁)) intro π₁ π₂ h₁ h₂ J hJ rcases h₁ hJ with ⟨J', hJ', hle⟩; rcases h₂ hJ' with ⟨J'', hJ'', hle'⟩ - obtain rfl : J = J''; exact π₁.eq_of_le hJ hJ'' (hle.trans hle') - obtain rfl : J' = J; exact le_antisymm ‹_› ‹_› + obtain rfl : J = J'' + · exact π₁.eq_of_le hJ hJ'' (hle.trans hle') + obtain rfl : J' = J + · exact le_antisymm ‹_› ‹_› assumption instance : OrderTop (Prepartition I) where @@ -304,8 +306,8 @@ def biUnion (πi : ∀ J : Box ι, Prepartition J) : Prepartition I where rw [Function.onFun, Set.disjoint_left] rintro x hx₁ hx₂; apply Hne obtain rfl : J₁ = J₂ - exact π.eq_of_mem_of_mem hJ₁ hJ₂ ((πi J₁).le_of_mem hJ₁' hx₁) ((πi J₂).le_of_mem hJ₂' hx₂) - exact (πi J₁).eq_of_mem_of_mem hJ₁' hJ₂' hx₁ hx₂ + · exact π.eq_of_mem_of_mem hJ₁ hJ₂ ((πi J₁).le_of_mem hJ₁' hx₁) ((πi J₂).le_of_mem hJ₂' hx₂) + · exact (πi J₁).eq_of_mem_of_mem hJ₁' hJ₂' hx₁ hx₂ #align box_integral.prepartition.bUnion BoxIntegral.Prepartition.biUnion variable {πi πi₁ πi₂ : ∀ J : Box ι, Prepartition J} @@ -535,8 +537,8 @@ theorem restrict_biUnion (πi : ∀ J, Prepartition J) (hJ : J ∈ π) : · simp only [iUnion_restrict, iUnion_biUnion, Set.subset_def, Set.mem_inter_iff, Set.mem_iUnion] rintro x ⟨hxJ, J₁, h₁, hx⟩ obtain rfl : J = J₁ - exact π.eq_of_mem_of_mem hJ h₁ hxJ (iUnion_subset _ hx) - exact hx + · exact π.eq_of_mem_of_mem hJ h₁ hxJ (iUnion_subset _ hx) + · exact hx #align box_integral.prepartition.restrict_bUnion BoxIntegral.Prepartition.restrict_biUnion theorem biUnion_le_iff {πi : ∀ J, Prepartition J} {π' : Prepartition I} : diff --git a/Mathlib/Analysis/Convex/Combination.lean b/Mathlib/Analysis/Convex/Combination.lean index 587c2253140e11..2c4584ee5ac911 100644 --- a/Mathlib/Analysis/Convex/Combination.lean +++ b/Mathlib/Analysis/Convex/Combination.lean @@ -115,11 +115,11 @@ theorem Finset.centerMass_segment (s : Finset ι) (w₁ w₂ : ι → R) (z : ι theorem Finset.centerMass_ite_eq (hi : i ∈ t) : t.centerMass (fun j => if i = j then (1 : R) else 0) z = z i := by rw [Finset.centerMass_eq_of_sum_1] - trans ∑ j in t, if i = j then z i else 0 - · congr with i - split_ifs with h - exacts [h ▸ one_smul _ _, zero_smul _ _] - · rw [sum_ite_eq, if_pos hi] + · trans ∑ j in t, if i = j then z i else 0 + · congr with i + split_ifs with h + exacts [h ▸ one_smul _ _, zero_smul _ _] + · rw [sum_ite_eq, if_pos hi] · rw [sum_ite_eq, if_pos hi] #align finset.center_mass_ite_eq Finset.centerMass_ite_eq diff --git a/Mathlib/Analysis/Convex/Function.lean b/Mathlib/Analysis/Convex/Function.lean index 7e98f552c4c41d..a9214c32fc09bf 100644 --- a/Mathlib/Analysis/Convex/Function.lean +++ b/Mathlib/Analysis/Convex/Function.lean @@ -235,7 +235,10 @@ theorem ConvexOn.convex_le (hf : ConvexOn 𝕜 s f) (r : β) : Convex 𝕜 ({ x ⟨hf.1 hx.1 hy.1 ha hb hab, calc f (a • x + b • y) ≤ a • f x + b • f y := hf.2 hx.1 hy.1 ha hb hab - _ ≤ a • r + b • r := by gcongr; exact hx.2; exact hy.2 + _ ≤ a • r + b • r := by + gcongr + · exact hx.2 + · exact hy.2 _ = r := Convex.combo_self hab r ⟩ #align convex_on.convex_le ConvexOn.convex_le @@ -386,7 +389,10 @@ theorem StrictConvexOn.convex_lt (hf : StrictConvexOn 𝕜 s f) (r : β) : ⟨hf.1 hx.1 hy.1 ha.le hb.le hab, calc f (a • x + b • y) < a • f x + b • f y := hf.2 hx.1 hy.1 hxy ha hb hab - _ ≤ a • r + b • r := by gcongr; exact hx.2.le; exact hy.2.le + _ ≤ a • r + b • r := by + gcongr + · exact hx.2.le + · exact hy.2.le _ = r := Convex.combo_self hab r ⟩ #align strict_convex_on.convex_lt StrictConvexOn.convex_lt diff --git a/Mathlib/Analysis/Convex/Mul.lean b/Mathlib/Analysis/Convex/Mul.lean index fc534c5b9b17d2..8d972c4e5980d5 100644 --- a/Mathlib/Analysis/Convex/Mul.lean +++ b/Mathlib/Analysis/Convex/Mul.lean @@ -177,8 +177,8 @@ lemma convexOn_zpow : ∀ n : ℤ, ConvexOn 𝕜 (Ioi 0) fun x : 𝕜 ↦ x ^ n rintro x (hx : 0 < x) y (hy : 0 < y) a b ha hb hab field_simp rw [div_le_div_iff, ← sub_nonneg] - calc - 0 ≤ a * b * (x - y) ^ 2 := by positivity - _ = _ := by obtain rfl := eq_sub_of_add_eq hab; ring + · calc + 0 ≤ a * b * (x - y) ^ 2 := by positivity + _ = _ := by obtain rfl := eq_sub_of_add_eq hab; ring all_goals positivity #align convex_on_zpow convexOn_zpow diff --git a/Mathlib/Analysis/Convex/Segment.lean b/Mathlib/Analysis/Convex/Segment.lean index 2f738f68de9343..d3b4e756dfd9de 100644 --- a/Mathlib/Analysis/Convex/Segment.lean +++ b/Mathlib/Analysis/Convex/Segment.lean @@ -457,12 +457,12 @@ variable [OrderedAddCommMonoid E] [Module 𝕜 E] [OrderedSMul 𝕜 E] {x y : E} theorem segment_subset_Icc (h : x ≤ y) : [x -[𝕜] y] ⊆ Icc x y := by rintro z ⟨a, b, ha, hb, hab, rfl⟩ constructor - calc - x = a • x + b • x := (Convex.combo_self hab _).symm - _ ≤ a • x + b • y := by gcongr - calc - a • x + b • y ≤ a • y + b • y := by gcongr - _ = y := Convex.combo_self hab _ + · calc + x = a • x + b • x := (Convex.combo_self hab _).symm + _ ≤ a • x + b • y := by gcongr + · calc + a • x + b • y ≤ a • y + b • y := by gcongr + _ = y := Convex.combo_self hab _ #align segment_subset_Icc segment_subset_Icc end OrderedAddCommMonoid @@ -474,12 +474,12 @@ variable [OrderedCancelAddCommMonoid E] [Module 𝕜 E] [OrderedSMul 𝕜 E] {x theorem openSegment_subset_Ioo (h : x < y) : openSegment 𝕜 x y ⊆ Ioo x y := by rintro z ⟨a, b, ha, hb, hab, rfl⟩ constructor - calc - x = a • x + b • x := (Convex.combo_self hab _).symm - _ < a • x + b • y := by gcongr - calc - a • x + b • y < a • y + b • y := by gcongr - _ = y := Convex.combo_self hab _ + · calc + x = a • x + b • x := (Convex.combo_self hab _).symm + _ < a • x + b • y := by gcongr + · calc + a • x + b • y < a • y + b • y := by gcongr + _ = y := Convex.combo_self hab _ #align open_segment_subset_Ioo openSegment_subset_Ioo end OrderedCancelAddCommMonoid diff --git a/Mathlib/Analysis/Convex/Star.lean b/Mathlib/Analysis/Convex/Star.lean index c66b24df7017b6..9da3cf9b761838 100644 --- a/Mathlib/Analysis/Convex/Star.lean +++ b/Mathlib/Analysis/Convex/Star.lean @@ -450,16 +450,16 @@ theorem Set.OrdConnected.starConvex [OrderedSemiring 𝕜] [OrderedAddCommMonoid intro y hy a b ha hb hab obtain hxy | hyx := h _ hy · refine' hs.out hx hy (mem_Icc.2 ⟨_, _⟩) - calc - x = a • x + b • x := (Convex.combo_self hab _).symm - _ ≤ a • x + b • y := by gcongr + · calc + x = a • x + b • x := (Convex.combo_self hab _).symm + _ ≤ a • x + b • y := by gcongr calc a • x + b • y ≤ a • y + b • y := by gcongr _ = y := Convex.combo_self hab _ · refine' hs.out hy hx (mem_Icc.2 ⟨_, _⟩) - calc - y = a • y + b • y := (Convex.combo_self hab _).symm - _ ≤ a • x + b • y := by gcongr + · calc + y = a • y + b • y := (Convex.combo_self hab _).symm + _ ≤ a • x + b • y := by gcongr calc a • x + b • y ≤ a • x + b • x := by gcongr _ = x := Convex.combo_self hab _ diff --git a/Mathlib/Analysis/Normed/Field/Basic.lean b/Mathlib/Analysis/Normed/Field/Basic.lean index 036af71371068d..d1c57875270bd6 100644 --- a/Mathlib/Analysis/Normed/Field/Basic.lean +++ b/Mathlib/Analysis/Normed/Field/Basic.lean @@ -663,9 +663,9 @@ instance (priority := 100) semi_normed_ring_top_monoid [NonUnitalSeminormedRing (((continuous_fst.tendsto x).sub tendsto_const_nhds).norm.mul _) -- Porting note: `show` used to select a goal to work on rotate_right - show Tendsto _ _ _ - exact tendsto_const_nhds - simp⟩ + · show Tendsto _ _ _ + exact tendsto_const_nhds + · simp⟩ #align semi_normed_ring_top_monoid semi_normed_ring_top_monoid -- see Note [lower instance priority] diff --git a/Mathlib/Analysis/SpecificLimits/Basic.lean b/Mathlib/Analysis/SpecificLimits/Basic.lean index 50df1409ebdf79..4dee81cbdf1ba0 100644 --- a/Mathlib/Analysis/SpecificLimits/Basic.lean +++ b/Mathlib/Analysis/SpecificLimits/Basic.lean @@ -155,10 +155,11 @@ alias tendsto_pow_atTop_nhds_0_of_lt_1 := tendsto_pow_atTop_nhds_zero_of_lt_one simp only [hr.symm, one_pow] at h exact zero_ne_one <| tendsto_nhds_unique h tendsto_const_nhds · apply @not_tendsto_nhds_of_tendsto_atTop 𝕜 ℕ _ _ _ _ atTop _ (fun n ↦ |r| ^ n) _ 0 _ - refine (pow_right_strictMono <| lt_of_le_of_ne (le_of_not_lt hr_le) - hr).monotone.tendsto_atTop_atTop (fun b ↦ ?_) - obtain ⟨n, hn⟩ := (pow_unbounded_of_one_lt b (lt_of_le_of_ne (le_of_not_lt hr_le) hr)) - exacts [⟨n, le_of_lt hn⟩, by simpa only [← abs_pow]] + · refine (pow_right_strictMono <| lt_of_le_of_ne (le_of_not_lt hr_le) + hr).monotone.tendsto_atTop_atTop (fun b ↦ ?_) + obtain ⟨n, hn⟩ := (pow_unbounded_of_one_lt b (lt_of_le_of_ne (le_of_not_lt hr_le) hr)) + exact ⟨n, le_of_lt hn⟩ + · simpa only [← abs_pow] · simpa only [← abs_pow] using (tendsto_pow_atTop_nhds_zero_of_lt_one (abs_nonneg r)) h @[deprecated] alias tendsto_pow_atTop_nhds_0_iff := tendsto_pow_atTop_nhds_zero_iff -- 2024-01-31 diff --git a/Mathlib/CategoryTheory/Abelian/Homology.lean b/Mathlib/CategoryTheory/Abelian/Homology.lean index 67d27d5f143c66..62bb2137928c2a 100644 --- a/Mathlib/CategoryTheory/Abelian/Homology.lean +++ b/Mathlib/CategoryTheory/Abelian/Homology.lean @@ -361,10 +361,10 @@ noncomputable def homology'FunctorIso (i : ι) : F.mapHomologicalComplex_map_f, F.map_comp] dsimp [HomologicalComplex.dFrom, HomologicalComplex.Hom.next] rw [kernel_map_comp_preserves_kernel_iso_inv_assoc] - conv_lhs => erw [← F.map_comp_assoc] - rotate_right; simp - rw [← kernel_map_comp_kernelSubobjectIso_inv] - any_goals simp) + · conv_lhs => erw [← F.map_comp_assoc] + rw [← kernel_map_comp_kernelSubobjectIso_inv] + · simp + · simp) #align category_theory.functor.homology_functor_iso CategoryTheory.Functor.homology'FunctorIso end CategoryTheory.Functor diff --git a/Mathlib/Combinatorics/Configuration.lean b/Mathlib/Combinatorics/Configuration.lean index 7f69688d1a0c31..ad2f7cdd37c7fe 100644 --- a/Mathlib/Combinatorics/Configuration.lean +++ b/Mathlib/Combinatorics/Configuration.lean @@ -275,11 +275,12 @@ theorem HasLines.lineCount_eq_pointCount [HasLines P L] [Fintype P] [Fintype L] simp_rw [Finset.sum_const, Finset.card_univ, hPL, sum_lineCount_eq_sum_pointCount] have step2 : ∑ i in s, lineCount L i.1 = ∑ i in s, pointCount P i.2 := by rw [s.sum_finset_product Finset.univ fun p => Set.toFinset { l | p ∈ l }] - rw [s.sum_finset_product_right Finset.univ fun l => Set.toFinset { p | p ∈ l }, eq_comm] - refine sum_bijective _ hf1 (by simp) fun l _ ↦ ?_ - simp_rw [hf2, sum_const, Set.toFinset_card, ← Nat.card_eq_fintype_card] - change pointCount P l • _ = lineCount L (f l) • _ - rw [hf2] + on_goal 1 => + rw [s.sum_finset_product_right Finset.univ fun l => Set.toFinset { p | p ∈ l }, eq_comm] + · refine sum_bijective _ hf1 (by simp) fun l _ ↦ ?_ + simp_rw [hf2, sum_const, Set.toFinset_card, ← Nat.card_eq_fintype_card] + change pointCount P l • _ = lineCount L (f l) • _ + rw [hf2] all_goals simp_rw [s, Finset.mem_univ, true_and_iff, Set.mem_toFinset]; exact fun p => Iff.rfl have step3 : ∑ i in sᶜ, lineCount L i.1 = ∑ i in sᶜ, pointCount P i.2 := by rwa [← s.sum_add_sum_compl, ← s.sum_add_sum_compl, step2, add_left_cancel_iff] at step1 @@ -312,7 +313,7 @@ noncomputable def HasLines.hasPoints [HasLines P L] [Fintype P] [Fintype L] have h₂ : ∀ l : L, 0 < pointCount P l := fun l => (congr_arg _ (hf2 l)).mpr (h₁ (f l)) obtain ⟨p, hl₁⟩ := Fintype.card_pos_iff.mp ((congr_arg _ Nat.card_eq_fintype_card).mp (h₂ l₁)) by_cases hl₂ : p ∈ l₂ - exact ⟨p, hl₁, hl₂⟩ + · exact ⟨p, hl₁, hl₂⟩ have key' : Fintype.card { q : P // q ∈ l₂ } = Fintype.card { l : L // p ∈ l } := ((HasLines.lineCount_eq_pointCount h hl₂).trans Nat.card_eq_fintype_card).symm.trans Nat.card_eq_fintype_card diff --git a/Mathlib/Combinatorics/Hall/Basic.lean b/Mathlib/Combinatorics/Hall/Basic.lean index 8800354655ea5d..74dbd44608e368 100644 --- a/Mathlib/Combinatorics/Hall/Basic.lean +++ b/Mathlib/Combinatorics/Hall/Basic.lean @@ -82,8 +82,8 @@ theorem hallMatchingsOn.nonempty {ι : Type u} {α : Type v} [DecidableEq α] (t apply (all_card_le_biUnion_card_iff_existsInjective' fun i : ι' => t i).mp intro s' convert h (s'.image (↑)) using 1 - simp only [card_image_of_injective s' Subtype.coe_injective] - rw [image_biUnion] + · simp only [card_image_of_injective s' Subtype.coe_injective] + · rw [image_biUnion] #align hall_matchings_on.nonempty hallMatchingsOn.nonempty /-- This is the `hallMatchingsOn` sets assembled into a directed system. diff --git a/Mathlib/Data/Complex/Exponential.lean b/Mathlib/Data/Complex/Exponential.lean index 7b717f43b690d9..9e7255b773e5ab 100644 --- a/Mathlib/Data/Complex/Exponential.lean +++ b/Mathlib/Data/Complex/Exponential.lean @@ -1459,8 +1459,8 @@ theorem exp_approx_end (n m : ℕ) (x : ℝ) (e₁ : n + 1 = m) (h : |x| ≤ 1) |exp x - expNear m x 0| ≤ |x| ^ m / m.factorial * ((m + 1) / m) := by simp only [expNear, mul_zero, add_zero] convert exp_bound (n := m) h ?_ using 1 - field_simp [mul_comm] - omega + · field_simp [mul_comm] + · omega #align real.exp_approx_end Real.exp_approx_end theorem exp_approx_succ {n} {x a₁ b₁ : ℝ} (m : ℕ) (e₁ : n + 1 = m) (a₂ b₂ : ℝ) diff --git a/Mathlib/Data/Nat/Squarefree.lean b/Mathlib/Data/Nat/Squarefree.lean index b700e1d4925d84..55a24f3a569a72 100644 --- a/Mathlib/Data/Nat/Squarefree.lean +++ b/Mathlib/Data/Nat/Squarefree.lean @@ -309,12 +309,12 @@ theorem divisors_filter_squarefree {n : ℕ} (h0 : n ≠ 0) : apply UniqueFactorizationMonoid.factors_unique _ _ (associated_iff_eq.2 h) · intro z hz apply irreducible_of_normalized_factor z - rw [← Multiset.mem_toFinset] - apply hx hz + · rw [← Multiset.mem_toFinset] + apply hx hz · intro z hz apply irreducible_of_normalized_factor z - rw [← Multiset.mem_toFinset] - apply hy hz + · rw [← Multiset.mem_toFinset] + apply hy hz #align nat.divisors_filter_squarefree Nat.divisors_filter_squarefree open BigOperators diff --git a/Mathlib/Data/Nat/Totient.lean b/Mathlib/Data/Nat/Totient.lean index b4ecd330c42c0d..48244634bb8e92 100644 --- a/Mathlib/Data/Nat/Totient.lean +++ b/Mathlib/Data/Nat/Totient.lean @@ -100,8 +100,8 @@ theorem Ico_filter_coprime_le {a : ℕ} (k n : ℕ) (a_pos : 0 < a) : (Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a))).card := by congr rw [Ico_union_Ico_eq_Ico] - rw [add_assoc] - exact le_self_add + · rw [add_assoc] + exact le_self_add exact le_self_add _ ≤ (filter a.Coprime (Ico k (k + n % a + a * i))).card + a.totient := by rw [filter_union, ← filter_coprime_Ico_eq_totient a (k + n % a + a * i)] diff --git a/Mathlib/Data/ZMod/Basic.lean b/Mathlib/Data/ZMod/Basic.lean index 8fe8bb4a8a9945..9122193558702a 100644 --- a/Mathlib/Data/ZMod/Basic.lean +++ b/Mathlib/Data/ZMod/Basic.lean @@ -115,8 +115,8 @@ where `a ≠ 0` is `addOrderOf_coe'`. -/ @[simp] theorem addOrderOf_coe (a : ℕ) {n : ℕ} (n0 : n ≠ 0) : addOrderOf (a : ZMod n) = n / n.gcd a := by cases' a with a - simp only [Nat.zero_eq, Nat.cast_zero, addOrderOf_zero, Nat.gcd_zero_right, Nat.pos_of_ne_zero n0, - Nat.div_self] + · simp only [Nat.zero_eq, Nat.cast_zero, addOrderOf_zero, Nat.gcd_zero_right, + Nat.pos_of_ne_zero n0, Nat.div_self] rw [← Nat.smul_one_eq_coe, addOrderOf_nsmul' _ a.succ_ne_zero, ZMod.addOrderOf_one] #align zmod.add_order_of_coe ZMod.addOrderOf_coe diff --git a/Mathlib/Geometry/RingedSpace/PresheafedSpace.lean b/Mathlib/Geometry/RingedSpace/PresheafedSpace.lean index 78e4b5cf678c67..c250ef910b796c 100644 --- a/Mathlib/Geometry/RingedSpace/PresheafedSpace.lean +++ b/Mathlib/Geometry/RingedSpace/PresheafedSpace.lean @@ -286,7 +286,7 @@ def isoOfComponents (H : X.1 ≅ Y.1) (α : H.hom _* X.2 ≅ Y.2) : X ≅ Y wher c := Presheaf.toPushforwardOfIso H α.hom } hom_inv_id := by ext - simp only [comp_base, Iso.hom_inv_id, FunctorToTypes.map_id_apply, id_base] + · simp only [comp_base, Iso.hom_inv_id, FunctorToTypes.map_id_apply, id_base] rw [NatTrans.comp_app] simp only [id_base, comp_obj, op_obj, comp_base, Presheaf.pushforwardObj_obj, Opens.map_comp_obj, comp_c_app, unop_op, Presheaf.toPushforwardOfIso_app, assoc, @@ -294,8 +294,8 @@ def isoOfComponents (H : X.1 ≅ Y.1) (α : H.hom _* X.2 ≅ Y.2) : X ≅ Y wher ← Functor.map_comp, eqToHom_trans, eqToHom_refl] inv_hom_id := by ext - dsimp - rw [H.inv_hom_id] + · dsimp + rw [H.inv_hom_id] dsimp simp only [Presheaf.pushforwardObj_obj, op_obj, Opens.map_comp_obj, comp_obj, comp_c_app, unop_op, Presheaf.toPushforwardOfIso_app, whiskerRight_app, eqToHom_app, @@ -516,12 +516,12 @@ def mapPresheaf (F : C ⥤ D) : PresheafedSpace C ⥤ PresheafedSpace D where -- Porting note: these proofs were automatic in mathlib3 map_id X := by ext U - rfl - simp + · rfl + · simp map_comp f g := by ext U - rfl - simp + · rfl + · simp #align category_theory.functor.map_presheaf CategoryTheory.Functor.mapPresheaf @[simp] diff --git a/Mathlib/GroupTheory/Complement.lean b/Mathlib/GroupTheory/Complement.lean index cc760d7e6bd404..ed3254219c79f6 100644 --- a/Mathlib/GroupTheory/Complement.lean +++ b/Mathlib/GroupTheory/Complement.lean @@ -480,9 +480,9 @@ theorem equiv_mul_right_of_mem {g k : G} (h : k ∈ K) : theorem equiv_mul_left (h : H) (g : G) : hHT.equiv (h * g) = (h * (hHT.equiv g).fst, (hHT.equiv g).snd) := by have : (hHT.equiv (h * g)).2 = (hHT.equiv g).2 := hHT.equiv_snd_eq_iff_rightCosetEquivalence.2 ?_ - ext - · rw [coe_mul, equiv_fst_eq_mul_inv, this, equiv_fst_eq_mul_inv, mul_assoc] - · rw [this] + · ext + · rw [coe_mul, equiv_fst_eq_mul_inv, this, equiv_fst_eq_mul_inv, mul_assoc] + · rw [this] · simp [RightCosetEquivalence, ← smul_smul] theorem equiv_mul_left_of_mem {h g : G} (hh : h ∈ H) : diff --git a/Mathlib/GroupTheory/Exponent.lean b/Mathlib/GroupTheory/Exponent.lean index 9b4096b68e67ce..7fb264aae4e0ef 100644 --- a/Mathlib/GroupTheory/Exponent.lean +++ b/Mathlib/GroupTheory/Exponent.lean @@ -495,8 +495,8 @@ theorem exists_orderOf_eq_exponent (hG : ExponentExists G) : ∃ g : G, orderOf rw [(Commute.all _ g).orderOf_mul_eq_mul_orderOf_of_coprime hcoprime, hpk', hg, ha, hk, pow_add, pow_add, pow_one, ← mul_assoc, ← mul_assoc, Nat.div_mul_cancel, mul_assoc, lt_mul_iff_one_lt_right <| hG.orderOf_pos t, ← pow_succ] - exact one_lt_pow hp.one_lt a.succ_ne_zero - exact hpk + · exact one_lt_pow hp.one_lt a.succ_ne_zero + · exact hpk @[to_additive] theorem exponent_eq_iSup_orderOf (h : ∀ g : G, 0 < orderOf g) : diff --git a/Mathlib/GroupTheory/HNNExtension.lean b/Mathlib/GroupTheory/HNNExtension.lean index c4af9564ddb236..8bd6caa360e8d2 100644 --- a/Mathlib/GroupTheory/HNNExtension.lean +++ b/Mathlib/GroupTheory/HNNExtension.lean @@ -472,9 +472,10 @@ theorem unitsSMul_one_group_smul (g : A) (w : NormalWord d) : -- This used to be the end of the proof before leanprover/lean4#2644 dsimp congr 1 - conv_lhs => erw [IsComplement.equiv_mul_left] - simp? says - simp only [toSubgroup_one, SetLike.coe_sort_coe, map_mul, Submonoid.coe_mul, coe_toSubmonoid] + · conv_lhs => erw [IsComplement.equiv_mul_left] + simp? says + simp only [toSubgroup_one, SetLike.coe_sort_coe, map_mul, Submonoid.coe_mul, + coe_toSubmonoid] conv_lhs => erw [IsComplement.equiv_mul_left] noncomputable instance : MulAction (HNNExtension G A B φ) (NormalWord d) := diff --git a/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean b/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean index eeb6bd83f8b8f2..78ef46bb816293 100644 --- a/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean +++ b/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean @@ -65,7 +65,7 @@ theorem formPerm_disjoint_iff (hl : Nodup l) (hl' : Nodup l') (hn : 2 ≤ l.leng omega · intro h x by_cases hx : x ∈ l - by_cases hx' : x ∈ l' + on_goal 1 => by_cases hx' : x ∈ l' · exact (h hx hx').elim all_goals have := formPerm_eq_self_of_not_mem _ _ ‹_›; tauto #align list.form_perm_disjoint_iff List.formPerm_disjoint_iff @@ -135,8 +135,8 @@ where each element in the list is permuted to the next one, defined as `formPerm def formPerm : ∀ s : Cycle α, Nodup s → Equiv.Perm α := fun s => Quotient.hrecOn s (fun l _ => List.formPerm l) fun l₁ l₂ (h : l₁ ~r l₂) => by apply Function.hfunext - ext - · exact h.nodup_iff + · ext + exact h.nodup_iff · intro h₁ h₂ _ exact heq_of_eq (formPerm_eq_of_isRotated h₁ h) #align cycle.form_perm Cycle.formPerm diff --git a/Mathlib/GroupTheory/SpecificGroups/Dihedral.lean b/Mathlib/GroupTheory/SpecificGroups/Dihedral.lean index 5684e76e3255aa..648376557bdd38 100644 --- a/Mathlib/GroupTheory/SpecificGroups/Dihedral.lean +++ b/Mathlib/GroupTheory/SpecificGroups/Dihedral.lean @@ -63,17 +63,17 @@ instance : Group (DihedralGroup n) where one := one one_mul := by rintro (a | a) - exact congr_arg r (zero_add a) - exact congr_arg sr (sub_zero a) + · exact congr_arg r (zero_add a) + · exact congr_arg sr (sub_zero a) mul_one := by rintro (a | a) - exact congr_arg r (add_zero a) - exact congr_arg sr (add_zero a) + · exact congr_arg r (add_zero a) + · exact congr_arg sr (add_zero a) inv := inv mul_left_inv := by rintro (a | a) - exact congr_arg r (neg_add_self a) - exact congr_arg r (sub_self a) + · exact congr_arg r (neg_add_self a) + · exact congr_arg r (sub_self a) @[simp] theorem r_mul_r (i j : ZMod n) : r i * r j = r (i + j) := diff --git a/Mathlib/LinearAlgebra/AffineSpace/Combination.lean b/Mathlib/LinearAlgebra/AffineSpace/Combination.lean index 0d5e081e5a816a..ed85c3594ad6ae 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/Combination.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/Combination.lean @@ -441,8 +441,8 @@ theorem attach_affineCombination_of_injective [DecidableEq P] (s : Finset P) (w ext simp rw [hgf, sum_image] - simp only [Function.comp_apply] - exact fun _ _ _ _ hxy => hf hxy + · simp only [Function.comp_apply] + · exact fun _ _ _ _ hxy => hf hxy #align finset.attach_affine_combination_of_injective Finset.attach_affineCombination_of_injective theorem attach_affineCombination_coe (s : Finset P) (w : P → k) : diff --git a/Mathlib/LinearAlgebra/AffineSpace/Independent.lean b/Mathlib/LinearAlgebra/AffineSpace/Independent.lean index 89d53893fff71c..6be6567c9131f6 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/Independent.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/Independent.lean @@ -473,10 +473,11 @@ theorem exists_nontrivial_relation_sum_zero_of_not_affine_ind {t : Finset V} vsub_eq_sub, Finset.weightedVSubOfPoint_apply, sub_zero] at hwt let f : ∀ x : V, x ∈ t → k := fun x hx => w ⟨x, hx⟩ refine' ⟨fun x => if hx : x ∈ t then f x hx else (0 : k), _, _, by use i; simp [hi]⟩ - suffices (∑ e : V in t, dite (e ∈ t) (fun hx => f e hx • e) fun _ => 0) = 0 by - convert this - rename V => x - by_cases hx : x ∈ t <;> simp [hx] + on_goal 1 => + suffices (∑ e : V in t, dite (e ∈ t) (fun hx => f e hx • e) fun _ => 0) = 0 by + convert this + rename V => x + by_cases hx : x ∈ t <;> simp [hx] all_goals simp only [Finset.sum_dite_of_true fun _ h => h, Finset.mk_coe, hwt, hw] #align exists_nontrivial_relation_sum_zero_of_not_affine_ind exists_nontrivial_relation_sum_zero_of_not_affine_ind diff --git a/Mathlib/LinearAlgebra/DFinsupp.lean b/Mathlib/LinearAlgebra/DFinsupp.lean index e886a42eb4c910..24709fe424d956 100644 --- a/Mathlib/LinearAlgebra/DFinsupp.lean +++ b/Mathlib/LinearAlgebra/DFinsupp.lean @@ -407,7 +407,7 @@ theorem mem_iSup_finset_iff_exists_sum {s : Finset ι} (p : ι → Submodule R N · exact hi simp only [DFinsupp.sum] rw [Finset.sum_subset support_mk_subset, ← hμ] - exact Finset.sum_congr rfl fun x hx => congr_arg Subtype.val <| mk_of_mem hx + · exact Finset.sum_congr rfl fun x hx => congr_arg Subtype.val <| mk_of_mem hx · intro x _ hx rw [mem_support_iff, not_ne_iff] at hx rw [hx] diff --git a/Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean b/Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean index c19bf1f17b483e..801f2f20082fa7 100644 --- a/Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean +++ b/Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean @@ -113,7 +113,7 @@ theorem Basis.le_span'' {ι : Type*} [Fintype ι] (b : Basis ι R M) {w : Set M} fapply card_le_of_surjective' R · exact b.repr.toLinearMap.comp (Finsupp.total w M R (↑)) · apply Surjective.comp (g := b.repr.toLinearMap) - apply LinearEquiv.surjective + · apply LinearEquiv.surjective rw [← LinearMap.range_eq_top, Finsupp.range_total] simpa using s #align basis.le_span'' Basis.le_span'' diff --git a/Mathlib/LinearAlgebra/FreeModule/PID.lean b/Mathlib/LinearAlgebra/FreeModule/PID.lean index 0f9ea0974c5ae6..0145db1699fd51 100644 --- a/Mathlib/LinearAlgebra/FreeModule/PID.lean +++ b/Mathlib/LinearAlgebra/FreeModule/PID.lean @@ -124,23 +124,23 @@ theorem generator_maximal_submoduleImage_dvd {N O : Submodule R M} (hNO : N ≤ refine' dvd_trans _ d_dvd_right rw [dvd_generator_iff, Ideal.span, ← span_singleton_generator (Submodule.span R {a, ψ ⟨y, hNO yN⟩})] - obtain ⟨r₁, r₂, d_eq⟩ : ∃ r₁ r₂ : R, d = r₁ * a + r₂ * ψ ⟨y, hNO yN⟩ := by - obtain ⟨r₁, r₂', hr₂', hr₁⟩ := - mem_span_insert.mp (IsPrincipal.generator_mem (Submodule.span R {a, ψ ⟨y, hNO yN⟩})) - obtain ⟨r₂, rfl⟩ := mem_span_singleton.mp hr₂' - exact ⟨r₁, r₂, hr₁⟩ - let ψ' : O →ₗ[R] R := r₁ • ϕ + r₂ • ψ - have : span R {d} ≤ ψ'.submoduleImage N := by - rw [span_le, singleton_subset_iff, SetLike.mem_coe, LinearMap.mem_submoduleImage_of_le hNO] - refine' ⟨y, yN, _⟩ - change r₁ * ϕ ⟨y, hNO yN⟩ + r₂ * ψ ⟨y, hNO yN⟩ = d - rw [d_eq, ϕy_eq] - refine' - le_antisymm (this.trans (le_of_eq _)) (Ideal.span_singleton_le_span_singleton.mpr d_dvd_left) - rw [span_singleton_generator] - apply (le_trans _ this).eq_of_not_gt (hϕ ψ') - rw [← span_singleton_generator (ϕ.submoduleImage N)] - exact Ideal.span_singleton_le_span_singleton.mpr d_dvd_left + · obtain ⟨r₁, r₂, d_eq⟩ : ∃ r₁ r₂ : R, d = r₁ * a + r₂ * ψ ⟨y, hNO yN⟩ := by + obtain ⟨r₁, r₂', hr₂', hr₁⟩ := + mem_span_insert.mp (IsPrincipal.generator_mem (Submodule.span R {a, ψ ⟨y, hNO yN⟩})) + obtain ⟨r₂, rfl⟩ := mem_span_singleton.mp hr₂' + exact ⟨r₁, r₂, hr₁⟩ + let ψ' : O →ₗ[R] R := r₁ • ϕ + r₂ • ψ + have : span R {d} ≤ ψ'.submoduleImage N := by + rw [span_le, singleton_subset_iff, SetLike.mem_coe, LinearMap.mem_submoduleImage_of_le hNO] + refine' ⟨y, yN, _⟩ + change r₁ * ϕ ⟨y, hNO yN⟩ + r₂ * ψ ⟨y, hNO yN⟩ = d + rw [d_eq, ϕy_eq] + refine' + le_antisymm (this.trans (le_of_eq _)) (Ideal.span_singleton_le_span_singleton.mpr d_dvd_left) + rw [span_singleton_generator] + apply (le_trans _ this).eq_of_not_gt (hϕ ψ') + rw [← span_singleton_generator (ϕ.submoduleImage N)] + exact Ideal.span_singleton_le_span_singleton.mpr d_dvd_left · exact subset_span (mem_insert _ _) #align generator_maximal_submodule_image_dvd generator_maximal_submoduleImage_dvd @@ -291,15 +291,15 @@ theorem Submodule.nonempty_basis_of_pid {ι : Type*} [Finite ι] (b : Basis ι R cases nonempty_fintype ι induction' N using inductionOnRank with N ih · exact b - let b' := (b.reindex (Fintype.equivFin ι)).map (LinearEquiv.ofTop _ rfl).symm - by_cases N_bot : N = ⊥ - · subst N_bot - exact ⟨0, ⟨Basis.empty _⟩⟩ - obtain ⟨y, -, a, hay, M', -, N', N'_le_N, -, -, ay_ortho, h'⟩ := - Submodule.basis_of_pid_aux ⊤ N b' N_bot le_top - obtain ⟨n', ⟨bN'⟩⟩ := ih N' N'_le_N _ hay ay_ortho - obtain ⟨bN, _hbN⟩ := h' n' bN' - exact ⟨n' + 1, ⟨bN⟩⟩ + · let b' := (b.reindex (Fintype.equivFin ι)).map (LinearEquiv.ofTop _ rfl).symm + by_cases N_bot : N = ⊥ + · subst N_bot + exact ⟨0, ⟨Basis.empty _⟩⟩ + obtain ⟨y, -, a, hay, M', -, N', N'_le_N, -, -, ay_ortho, h'⟩ := + Submodule.basis_of_pid_aux ⊤ N b' N_bot le_top + obtain ⟨n', ⟨bN'⟩⟩ := ih N' N'_le_N _ hay ay_ortho + obtain ⟨bN, _hbN⟩ := h' n' bN' + exact ⟨n' + 1, ⟨bN⟩⟩ infer_instance #align submodule.nonempty_basis_of_pid Submodule.nonempty_basis_of_pid @@ -513,19 +513,19 @@ theorem Submodule.exists_smith_normal_form_of_le [Finite ι] (b : Basis ι R M) revert N induction' O using inductionOnRank with M0 ih · exact b - intro N N_le_M0 - obtain ⟨m, b'M⟩ := M0.basisOfPid b - by_cases N_bot : N = ⊥ - · subst N_bot - exact ⟨0, m, Nat.zero_le _, b'M, Basis.empty _, finZeroElim, finZeroElim⟩ - obtain ⟨y, hy, a, _, M', M'_le_M, N', _, N'_le_M', y_ortho, _, h⟩ := - Submodule.basis_of_pid_aux M0 N b'M N_bot N_le_M0 - - obtain ⟨n', m', hn'm', bM', bN', as', has'⟩ := ih M' M'_le_M y hy y_ortho N' N'_le_M' - obtain ⟨bN, h'⟩ := h n' bN' - obtain ⟨hmn, bM, h''⟩ := h' m' hn'm' bM' - obtain ⟨as, has⟩ := h'' as' has' - exact ⟨_, _, hmn, bM, bN, as, has⟩ + · intro N N_le_M0 + obtain ⟨m, b'M⟩ := M0.basisOfPid b + by_cases N_bot : N = ⊥ + · subst N_bot + exact ⟨0, m, Nat.zero_le _, b'M, Basis.empty _, finZeroElim, finZeroElim⟩ + obtain ⟨y, hy, a, _, M', M'_le_M, N', _, N'_le_M', y_ortho, _, h⟩ := + Submodule.basis_of_pid_aux M0 N b'M N_bot N_le_M0 + + obtain ⟨n', m', hn'm', bM', bN', as', has'⟩ := ih M' M'_le_M y hy y_ortho N' N'_le_M' + obtain ⟨bN, h'⟩ := h n' bN' + obtain ⟨hmn, bM, h''⟩ := h' m' hn'm' bM' + obtain ⟨as, has⟩ := h'' as' has' + exact ⟨_, _, hmn, bM, bN, as, has⟩ -- Porting note: Lean generates a goal Fintype ι for some reason infer_instance #align submodule.exists_smith_normal_form_of_le Submodule.exists_smith_normal_form_of_le diff --git a/Mathlib/LinearAlgebra/InvariantBasisNumber.lean b/Mathlib/LinearAlgebra/InvariantBasisNumber.lean index 47e493a9f27256..553c177e0fb346 100644 --- a/Mathlib/LinearAlgebra/InvariantBasisNumber.lean +++ b/Mathlib/LinearAlgebra/InvariantBasisNumber.lean @@ -286,9 +286,9 @@ private def induced_equiv [Fintype ι'] (I : Ideal R) (e : (ι → R) ≃ₗ[R] -- Porting note: the next 4 lines were necessary because Lean couldn't correctly infer `(I.pi ι)` -- and `(I.pi ι')` on its own. pick_goal 3 - convert_to Ideal.Quotient.mk (I.pi ι) _ = Ideal.Quotient.mk (I.pi ι) _ - congr - simp only [LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply] + · convert_to Ideal.Quotient.mk (I.pi ι) _ = Ideal.Quotient.mk (I.pi ι) _ + congr + simp only [LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply] all_goals convert_to Ideal.Quotient.mk (I.pi ι') _ = Ideal.Quotient.mk (I.pi ι') _ congr diff --git a/Mathlib/LinearAlgebra/Matrix/Determinant.lean b/Mathlib/LinearAlgebra/Matrix/Determinant.lean index b723eb257c49d8..210cf2d1e63689 100644 --- a/Mathlib/LinearAlgebra/Matrix/Determinant.lean +++ b/Mathlib/LinearAlgebra/Matrix/Determinant.lean @@ -589,50 +589,50 @@ theorem det_blockDiagonal {o : Type*} [Fintype o] [DecidableEq o] (M : o → Mat Finset.mem_filter.trans ⟨fun h => h.2, fun h => ⟨Finset.mem_univ _, h⟩⟩ rw [← Finset.sum_subset (Finset.subset_univ preserving_snd) _] -- And that these are in bijection with `o → Equiv.Perm m`. - refine (Finset.sum_bij (fun σ _ => prodCongrLeft fun k ↦ σ k (mem_univ k)) ?_ ?_ ?_ ?_).symm - · intro σ _ - rw [mem_preserving_snd] - rintro ⟨-, x⟩ - simp only [prodCongrLeft_apply] - · intro σ _ σ' _ eq - ext x hx k - simp only at eq - have : - ∀ k x, - prodCongrLeft (fun k => σ k (Finset.mem_univ _)) (k, x) = - prodCongrLeft (fun k => σ' k (Finset.mem_univ _)) (k, x) := - fun k x => by rw [eq] - simp only [prodCongrLeft_apply, Prod.mk.inj_iff] at this - exact (this k x).1 - · intro σ hσ - rw [mem_preserving_snd] at hσ - have hσ' : ∀ x, (σ⁻¹ x).snd = x.snd := by - intro x - conv_rhs => rw [← Perm.apply_inv_self σ x, hσ] - have mk_apply_eq : ∀ k x, ((σ (x, k)).fst, k) = σ (x, k) := by - intro k x - ext - · simp only - · simp only [hσ] - have mk_inv_apply_eq : ∀ k x, ((σ⁻¹ (x, k)).fst, k) = σ⁻¹ (x, k) := by - intro k x - conv_lhs => rw [← Perm.apply_inv_self σ (x, k)] - ext - · simp only [apply_inv_self] - · simp only [hσ'] - refine' ⟨fun k _ => ⟨fun x => (σ (x, k)).fst, fun x => (σ⁻¹ (x, k)).fst, _, _⟩, _, _⟩ - · intro x - simp only [mk_apply_eq, inv_apply_self] - · intro x - simp only [mk_inv_apply_eq, apply_inv_self] - · apply Finset.mem_univ - · ext ⟨k, x⟩ - · simp only [coe_fn_mk, prodCongrLeft_apply] - · simp only [prodCongrLeft_apply, hσ] - · intro σ _ - rw [Finset.prod_mul_distrib, ← Finset.univ_product_univ, Finset.prod_product_right] - simp only [sign_prodCongrLeft, Units.coe_prod, Int.cast_prod, blockDiagonal_apply_eq, - prodCongrLeft_apply] + · refine (Finset.sum_bij (fun σ _ => prodCongrLeft fun k ↦ σ k (mem_univ k)) ?_ ?_ ?_ ?_).symm + · intro σ _ + rw [mem_preserving_snd] + rintro ⟨-, x⟩ + simp only [prodCongrLeft_apply] + · intro σ _ σ' _ eq + ext x hx k + simp only at eq + have : + ∀ k x, + prodCongrLeft (fun k => σ k (Finset.mem_univ _)) (k, x) = + prodCongrLeft (fun k => σ' k (Finset.mem_univ _)) (k, x) := + fun k x => by rw [eq] + simp only [prodCongrLeft_apply, Prod.mk.inj_iff] at this + exact (this k x).1 + · intro σ hσ + rw [mem_preserving_snd] at hσ + have hσ' : ∀ x, (σ⁻¹ x).snd = x.snd := by + intro x + conv_rhs => rw [← Perm.apply_inv_self σ x, hσ] + have mk_apply_eq : ∀ k x, ((σ (x, k)).fst, k) = σ (x, k) := by + intro k x + ext + · simp only + · simp only [hσ] + have mk_inv_apply_eq : ∀ k x, ((σ⁻¹ (x, k)).fst, k) = σ⁻¹ (x, k) := by + intro k x + conv_lhs => rw [← Perm.apply_inv_self σ (x, k)] + ext + · simp only [apply_inv_self] + · simp only [hσ'] + refine' ⟨fun k _ => ⟨fun x => (σ (x, k)).fst, fun x => (σ⁻¹ (x, k)).fst, _, _⟩, _, _⟩ + · intro x + simp only [mk_apply_eq, inv_apply_self] + · intro x + simp only [mk_inv_apply_eq, apply_inv_self] + · apply Finset.mem_univ + · ext ⟨k, x⟩ + · simp only [coe_fn_mk, prodCongrLeft_apply] + · simp only [prodCongrLeft_apply, hσ] + · intro σ _ + rw [Finset.prod_mul_distrib, ← Finset.univ_product_univ, Finset.prod_product_right] + simp only [sign_prodCongrLeft, Units.coe_prod, Int.cast_prod, blockDiagonal_apply_eq, + prodCongrLeft_apply] · intro σ _ hσ rw [mem_preserving_snd] at hσ obtain ⟨⟨k, x⟩, hkx⟩ := not_forall.mp hσ @@ -651,37 +651,37 @@ theorem det_fromBlocks_zero₂₁ (A : Matrix m m R) (B : Matrix m n R) (D : Mat simp_rw [det_apply'] convert Eq.symm <| sum_subset (β := R) (subset_univ ((sumCongrHom m n).range : Set (Perm (Sum m n))).toFinset) ?_ - simp_rw [sum_mul_sum, ← sum_product', univ_product_univ] - refine sum_nbij (fun σ ↦ σ.fst.sumCongr σ.snd) ?_ ?_ ?_ ?_ - · intro σ₁₂ _ - simp only - erw [Set.mem_toFinset, MonoidHom.mem_range] - use σ₁₂ - simp only [sumCongrHom_apply] - · intro σ₁ _ σ₂ _ - dsimp only - intro h - have h2 : ∀ x, Perm.sumCongr σ₁.fst σ₁.snd x = Perm.sumCongr σ₂.fst σ₂.snd x := - DFunLike.congr_fun h - simp only [Sum.map_inr, Sum.map_inl, Perm.sumCongr_apply, Sum.forall, Sum.inl.injEq, - Sum.inr.injEq] at h2 - ext x - · exact h2.left x - · exact h2.right x - · intro σ hσ - erw [Set.mem_toFinset, MonoidHom.mem_range] at hσ - obtain ⟨σ₁₂, hσ₁₂⟩ := hσ - use σ₁₂ - rw [← hσ₁₂] - simp - · simp only [forall_prop_of_true, Prod.forall, mem_univ] - intro σ₁ σ₂ - rw [Fintype.prod_sum_type] - simp_rw [Equiv.sumCongr_apply, Sum.map_inr, Sum.map_inl, fromBlocks_apply₁₁, - fromBlocks_apply₂₂] - rw [mul_mul_mul_comm] - congr - rw [sign_sumCongr, Units.val_mul, Int.cast_mul] + · simp_rw [sum_mul_sum, ← sum_product', univ_product_univ] + refine sum_nbij (fun σ ↦ σ.fst.sumCongr σ.snd) ?_ ?_ ?_ ?_ + · intro σ₁₂ _ + simp only + erw [Set.mem_toFinset, MonoidHom.mem_range] + use σ₁₂ + simp only [sumCongrHom_apply] + · intro σ₁ _ σ₂ _ + dsimp only + intro h + have h2 : ∀ x, Perm.sumCongr σ₁.fst σ₁.snd x = Perm.sumCongr σ₂.fst σ₂.snd x := + DFunLike.congr_fun h + simp only [Sum.map_inr, Sum.map_inl, Perm.sumCongr_apply, Sum.forall, Sum.inl.injEq, + Sum.inr.injEq] at h2 + ext x + · exact h2.left x + · exact h2.right x + · intro σ hσ + erw [Set.mem_toFinset, MonoidHom.mem_range] at hσ + obtain ⟨σ₁₂, hσ₁₂⟩ := hσ + use σ₁₂ + rw [← hσ₁₂] + simp + · simp only [forall_prop_of_true, Prod.forall, mem_univ] + intro σ₁ σ₂ + rw [Fintype.prod_sum_type] + simp_rw [Equiv.sumCongr_apply, Sum.map_inr, Sum.map_inl, fromBlocks_apply₁₁, + fromBlocks_apply₂₂] + rw [mul_mul_mul_comm] + congr + rw [sign_sumCongr, Units.val_mul, Int.cast_mul] · rintro σ - hσn have h1 : ¬∀ x, ∃ y, Sum.inl y = σ (Sum.inl x) := by rw [Set.mem_toFinset] at hσn diff --git a/Mathlib/LinearAlgebra/Matrix/DotProduct.lean b/Mathlib/LinearAlgebra/Matrix/DotProduct.lean index 7275fb4142eeba..ca23ba5f8b684e 100644 --- a/Mathlib/LinearAlgebra/Matrix/DotProduct.lean +++ b/Mathlib/LinearAlgebra/Matrix/DotProduct.lean @@ -41,8 +41,8 @@ variable [Semiring R] [Fintype n] theorem dotProduct_stdBasis_eq_mul [DecidableEq n] (v : n → R) (c : R) (i : n) : dotProduct v (LinearMap.stdBasis R (fun _ => R) i c) = v i * c := by rw [dotProduct, Finset.sum_eq_single i, LinearMap.stdBasis_same] - exact fun _ _ hb => by rw [LinearMap.stdBasis_ne _ _ _ _ hb, mul_zero] - exact fun hi => False.elim (hi <| Finset.mem_univ _) + · exact fun _ _ hb => by rw [LinearMap.stdBasis_ne _ _ _ _ hb, mul_zero] + · exact fun hi => False.elim (hi <| Finset.mem_univ _) #align matrix.dot_product_std_basis_eq_mul Matrix.dotProduct_stdBasis_eq_mul -- @[simp] -- Porting note (#10618): simp can prove this diff --git a/Mathlib/LinearAlgebra/Matrix/Transvection.lean b/Mathlib/LinearAlgebra/Matrix/Transvection.lean index 5e21f5180826ae..d42eba2c553cbb 100644 --- a/Mathlib/LinearAlgebra/Matrix/Transvection.lean +++ b/Mathlib/LinearAlgebra/Matrix/Transvection.lean @@ -96,12 +96,13 @@ theorem updateRow_eq_transvection [Finite n] (c : R) : transvection i j c := by cases nonempty_fintype n ext a b - by_cases ha : i = a; by_cases hb : j = b - · simp only [updateRow_self, transvection, ha, hb, Pi.add_apply, StdBasisMatrix.apply_same, - one_apply_eq, Pi.smul_apply, mul_one, Algebra.id.smul_eq_mul, add_apply] - · simp only [updateRow_self, transvection, ha, hb, StdBasisMatrix.apply_of_ne, Pi.add_apply, - Ne, not_false_iff, Pi.smul_apply, and_false_iff, one_apply_ne, Algebra.id.smul_eq_mul, - mul_zero, add_apply] + by_cases ha : i = a + · by_cases hb : j = b + · simp only [updateRow_self, transvection, ha, hb, Pi.add_apply, StdBasisMatrix.apply_same, + one_apply_eq, Pi.smul_apply, mul_one, Algebra.id.smul_eq_mul, add_apply] + · simp only [updateRow_self, transvection, ha, hb, StdBasisMatrix.apply_of_ne, Pi.add_apply, + Ne, not_false_iff, Pi.smul_apply, and_false_iff, one_apply_ne, Algebra.id.smul_eq_mul, + mul_zero, add_apply] · simp only [updateRow_ne, transvection, ha, Ne.symm ha, StdBasisMatrix.apply_of_ne, add_zero, Algebra.id.smul_eq_mul, Ne, not_false_iff, DMatrix.add_apply, Pi.smul_apply, mul_zero, false_and_iff, add_apply] diff --git a/Mathlib/ModelTheory/DirectLimit.lean b/Mathlib/ModelTheory/DirectLimit.lean index ca2c4571c20acd..877b4c78cd6bcb 100644 --- a/Mathlib/ModelTheory/DirectLimit.lean +++ b/Mathlib/ModelTheory/DirectLimit.lean @@ -142,8 +142,8 @@ def setoid [DirectedSystem G fun i j h => f i j h] [IsDirected ι (· ≤ ·)] : obtain ⟨ijk, hijijk, hjkijk⟩ := directed_of (· ≤ ·) ij jk refine' ⟨ijk, le_trans hiij hijijk, le_trans hkjk hjkijk, _⟩ rw [← DirectedSystem.map_map, hij, DirectedSystem.map_map] - symm - rw [← DirectedSystem.map_map, ← hjk, DirectedSystem.map_map] <;> assumption⟩ + · symm + rw [← DirectedSystem.map_map, ← hjk, DirectedSystem.map_map] <;> assumption⟩ #align first_order.language.direct_limit.setoid FirstOrder.Language.DirectLimit.setoid /-- The structure on the `Σ`-type which becomes the structure on the direct limit after quotienting. diff --git a/Mathlib/NumberTheory/FLT/Three.lean b/Mathlib/NumberTheory/FLT/Three.lean index 560af0f38dd94e..60d4369ab1751e 100644 --- a/Mathlib/NumberTheory/FLT/Three.lean +++ b/Mathlib/NumberTheory/FLT/Three.lean @@ -97,7 +97,8 @@ theorem fermatLastTheoremThree_of_three_dvd_only_c rw [fermatLastTheoremFor_iff_int] refine fermatLastTheoremWith_of_fermatLastTheoremWith_coprime (fun a b c ha hb hc Hgcd hF ↦?_) by_cases h1 : 3 ∣ a * b * c - swap; exact fermatLastTheoremThree_case_1 h1 hF + swap + · exact fermatLastTheoremThree_case_1 h1 hF rw [(prime_three).dvd_mul, (prime_three).dvd_mul] at h1 rw [← sub_eq_zero, sub_eq_add_neg, ← (show Odd 3 by decide).neg_pow] at hF rcases h1 with ((h3a | h3b) | h3c) diff --git a/Mathlib/NumberTheory/Multiplicity.lean b/Mathlib/NumberTheory/Multiplicity.lean index 75a27c88535b74..b7c02996c3c41e 100644 --- a/Mathlib/NumberTheory/Multiplicity.lean +++ b/Mathlib/NumberTheory/Multiplicity.lean @@ -345,8 +345,8 @@ theorem Int.two_pow_sub_pow {x y : ℤ} {n : ℕ} (hxy : 2 ∣ x - y) (hx : ¬2 · simp only [Int.odd_iff_not_even, even_iff_two_dvd, hx, not_false_iff] rw [Int.two_pow_sub_pow' d hxy4 _, sq_sub_sq, ← Int.ofNat_mul_out, multiplicity.mul Int.prime_two, multiplicity.mul Int.prime_two] - suffices multiplicity (2 : ℤ) ↑(2 : ℕ) = 1 by rw [this, add_comm (1 : PartENat), ← add_assoc] - · norm_cast + · suffices multiplicity (2 : ℤ) ↑(2 : ℕ) = 1 by rw [this, add_comm (1 : PartENat), ← add_assoc] + norm_cast rw [multiplicity.multiplicity_self _ _] · apply Prime.not_unit simp only [← Nat.prime_iff, Nat.prime_two] diff --git a/Mathlib/NumberTheory/PellMatiyasevic.lean b/Mathlib/NumberTheory/PellMatiyasevic.lean index bc0406be870aff..92197a1065b321 100644 --- a/Mathlib/NumberTheory/PellMatiyasevic.lean +++ b/Mathlib/NumberTheory/PellMatiyasevic.lean @@ -675,7 +675,8 @@ theorem eq_of_xn_modEq_lem3 {i n} (npos : 0 < n) : lt_of_add_lt_add_right <| show 2 * n - k + k < n + k by rw [tsub_add_cancel_of_le] - rw [two_mul]; exact add_lt_add_left kn n + · rw [two_mul] + exact add_lt_add_left kn n exact k2n have xle : xn a1 (2 * n - k) ≤ xn a1 n := le_of_lt <| strictMono_x a1 k2nl suffices xn a1 k % xn a1 n = xn a1 n - xn a1 (2 * n - k) by rw [this, Int.ofNat_sub xle] @@ -754,7 +755,7 @@ theorem eq_of_xn_modEq_le {i j n} (ij : i ≤ j) (j2n : j ≤ 2 * n) rw [Nat.mod_eq_of_lt (strictMono_x a1 (Nat.pos_of_ne_zero npos))] exact Nat.succ_pos _ cases' i with i - exact x0 + · exact x0 rw [jn] at ij' exact x0.trans diff --git a/Mathlib/RingTheory/ChainOfDivisors.lean b/Mathlib/RingTheory/ChainOfDivisors.lean index 9914fc74a0ec17..4ba8b899629c99 100644 --- a/Mathlib/RingTheory/ChainOfDivisors.lean +++ b/Mathlib/RingTheory/ChainOfDivisors.lean @@ -202,9 +202,9 @@ theorem eq_pow_second_of_chain_of_has_chain {q : Associates M} {n : ℕ} (hn : n have := h₂.2 ⟨j, rfl⟩ rw [hi'] at this have h := (dvd_prime_pow (show Prime (c 1) from ?_) i).1 this - rcases h with ⟨u, hu, hu'⟩ - refine' Finset.mem_image.mpr ⟨u, Finset.mem_univ _, _⟩ - · rw [associated_iff_eq] at hu' + · rcases h with ⟨u, hu, hu'⟩ + refine' Finset.mem_image.mpr ⟨u, Finset.mem_univ _, _⟩ + rw [associated_iff_eq] at hu' rw [Fin.val_cast_of_lt (Nat.lt_succ_of_le hu), hu'] · rw [← irreducible_iff_prime] exact second_of_chain_is_irreducible hn h₁ (@h₂) hq diff --git a/Mathlib/RingTheory/Finiteness.lean b/Mathlib/RingTheory/Finiteness.lean index a0f0a8d8f8f075..6ab73c04f554cd 100644 --- a/Mathlib/RingTheory/Finiteness.lean +++ b/Mathlib/RingTheory/Finiteness.lean @@ -319,18 +319,18 @@ theorem fg_of_fg_map_of_fg_inf_ker {R M P : Type*} [Ring R] [AddCommGroup M] [Mo constructor · apply s.sub_mem hx rw [Finsupp.total_apply, Finsupp.lmapDomain_apply, Finsupp.sum_mapDomain_index] - refine' s.sum_mem _ - · intro y hy + · refine' s.sum_mem _ + intro y hy exact s.smul_mem _ (hg y (hl1 hy)).1 · exact zero_smul _ · exact fun _ _ _ => add_smul _ _ _ · rw [LinearMap.mem_ker, f.map_sub, ← hl2] rw [Finsupp.total_apply, Finsupp.total_apply, Finsupp.lmapDomain_apply] rw [Finsupp.sum_mapDomain_index, Finsupp.sum, Finsupp.sum, map_sum] - rw [sub_eq_zero] - refine' Finset.sum_congr rfl fun y hy => _ - unfold id - rw [f.map_smul, (hg y (hl1 hy)).2] + · rw [sub_eq_zero] + refine' Finset.sum_congr rfl fun y hy => _ + unfold id + rw [f.map_smul, (hg y (hl1 hy)).2] · exact zero_smul _ · exact fun _ _ _ => add_smul _ _ _ #align submodule.fg_of_fg_map_of_fg_inf_ker Submodule.fg_of_fg_map_of_fg_inf_ker diff --git a/Mathlib/RingTheory/Ideal/IsPrimary.lean b/Mathlib/RingTheory/Ideal/IsPrimary.lean index 37e106d592c271..9f933c79d4df90 100644 --- a/Mathlib/RingTheory/Ideal/IsPrimary.lean +++ b/Mathlib/RingTheory/Ideal/IsPrimary.lean @@ -49,9 +49,10 @@ theorem isPrimary_inf {I J : Ideal R} (hi : IsPrimary I) (hj : IsPrimary J) ⟨ne_of_lt <| lt_of_le_of_lt inf_le_left (lt_top_iff_ne_top.2 hi.1), fun {x y} ⟨hxyi, hxyj⟩ => by rw [radical_inf, hij, inf_idem] - cases' hi.2 hxyi with hxi hyi; cases' hj.2 hxyj with hxj hyj - · exact Or.inl ⟨hxi, hxj⟩ - · exact Or.inr hyj + cases' hi.2 hxyi with hxi hyi + · cases' hj.2 hxyj with hxj hyj + · exact Or.inl ⟨hxi, hxj⟩ + · exact Or.inr hyj · rw [hij] at hyi exact Or.inr hyi⟩ #align ideal.is_primary_inf Ideal.isPrimary_inf diff --git a/Mathlib/RingTheory/Localization/Away/Basic.lean b/Mathlib/RingTheory/Localization/Away/Basic.lean index dd663bc3e3b31e..fbb808974c06ee 100644 --- a/Mathlib/RingTheory/Localization/Away/Basic.lean +++ b/Mathlib/RingTheory/Localization/Away/Basic.lean @@ -295,13 +295,13 @@ theorem exists_reduced_fraction' {b : B} (hb : b ≠ 0) (hx : Irreducible x) : (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero) simp only [map_zero, ← hy, map_pow] at H apply ((injective_iff_map_eq_zero' (algebraMap R B)).mp _ a₀).mpr.mt - rw [← H] - apply mul_ne_zero hb (pow_ne_zero _ _) - exact - IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors B - (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero) - (mem_nonZeroDivisors_iff_ne_zero.mpr hx.ne_zero) - exact IsLocalization.injective B (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero) + · rw [← H] + apply mul_ne_zero hb (pow_ne_zero _ _) + exact + IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors B + (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero) + (mem_nonZeroDivisors_iff_ne_zero.mpr hx.ne_zero) + · exact IsLocalization.injective B (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero) simp only [← hy] at H obtain ⟨m, a, hyp1, hyp2⟩ := WfDvdMonoid.max_power_factor ha₀ hx refine' ⟨a, m - d, _⟩ diff --git a/Mathlib/RingTheory/Localization/FractionRing.lean b/Mathlib/RingTheory/Localization/FractionRing.lean index 480facc4e222bf..50155d623274af 100644 --- a/Mathlib/RingTheory/Localization/FractionRing.lean +++ b/Mathlib/RingTheory/Localization/FractionRing.lean @@ -269,11 +269,11 @@ theorem isFractionRing_iff_of_base_ringEquiv (h : R ≃+* P) : protected theorem nontrivial (R S : Type*) [CommRing R] [Nontrivial R] [CommRing S] [Algebra R S] [IsFractionRing R S] : Nontrivial S := by apply nontrivial_of_ne - intro h - apply @zero_ne_one R - exact - IsLocalization.injective S (le_of_eq rfl) - (((algebraMap R S).map_zero.trans h).trans (algebraMap R S).map_one.symm) + · intro h + apply @zero_ne_one R + exact + IsLocalization.injective S (le_of_eq rfl) + (((algebraMap R S).map_zero.trans h).trans (algebraMap R S).map_one.symm) #align is_fraction_ring.nontrivial IsFractionRing.nontrivial end IsFractionRing diff --git a/Mathlib/RingTheory/Localization/Ideal.lean b/Mathlib/RingTheory/Localization/Ideal.lean index 46e40ff754ae8a..fb6fdf43499c6a 100644 --- a/Mathlib/RingTheory/Localization/Ideal.lean +++ b/Mathlib/RingTheory/Localization/Ideal.lean @@ -97,8 +97,8 @@ def orderEmbedding : Ideal S ↪o Ideal R where map_rel_iff' := by rintro J₁ J₂ constructor - exact fun hJ => (map_comap M S) J₁ ▸ (map_comap M S) J₂ ▸ Ideal.map_mono hJ - exact fun hJ => Ideal.comap_mono hJ + · exact fun hJ => (map_comap M S) J₁ ▸ (map_comap M S) J₂ ▸ Ideal.map_mono hJ + · exact fun hJ => Ideal.comap_mono hJ #align is_localization.order_embedding IsLocalization.orderEmbedding /-- If `R` is a ring, then prime ideals in the localization at `M` @@ -153,8 +153,8 @@ def orderIsoOfPrime : map_rel_iff' := by rintro I I' constructor - exact (fun h => show I.val ≤ I'.val from map_comap M S I.val ▸ - map_comap M S I'.val ▸ Ideal.map_mono h) + · exact (fun h => show I.val ≤ I'.val from map_comap M S I.val ▸ + map_comap M S I'.val ▸ Ideal.map_mono h) exact fun h x hx => h hx #align is_localization.order_iso_of_prime IsLocalization.orderIsoOfPrime diff --git a/Mathlib/RingTheory/Localization/Submodule.lean b/Mathlib/RingTheory/Localization/Submodule.lean index 37851fcc4c19ba..80bc92e956defb 100644 --- a/Mathlib/RingTheory/Localization/Submodule.lean +++ b/Mathlib/RingTheory/Localization/Submodule.lean @@ -138,8 +138,9 @@ variable {S} (M) theorem mem_span_iff {N : Type*} [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N] {x : N} {a : Set N} : x ∈ Submodule.span S a ↔ ∃ y ∈ Submodule.span R a, ∃ z : M, x = mk' S 1 z • y := by - constructor; intro h - · refine' Submodule.span_induction h _ _ _ _ + constructor + · intro h + refine' Submodule.span_induction h _ _ _ _ · rintro x hx exact ⟨x, Submodule.subset_span hx, 1, by rw [mk'_one, _root_.map_one, one_smul]⟩ · exact ⟨0, Submodule.zero_mem _, 1, by rw [mk'_one, _root_.map_one, one_smul]⟩ diff --git a/Mathlib/RingTheory/MvPolynomial/Symmetric.lean b/Mathlib/RingTheory/MvPolynomial/Symmetric.lean index a699ca2ec9d9ef..b811d87e3eb30e 100644 --- a/Mathlib/RingTheory/MvPolynomial/Symmetric.lean +++ b/Mathlib/RingTheory/MvPolynomial/Symmetric.lean @@ -251,14 +251,14 @@ theorem support_esymm'' (n : ℕ) [DecidableEq σ] [Nontrivial R] : rintro a h rfl have := congr_arg Finsupp.support h rw [Finsupp.support_sum_eq_biUnion, Finsupp.support_sum_eq_biUnion] at this - have hsingle : ∀ s : Finset σ, ∀ x : σ, x ∈ s → (Finsupp.single x 1).support = {x} := by - intros _ x _ - rw [Finsupp.support_single_ne_zero x one_ne_zero] - have hs := biUnion_congr (of_eq_true (eq_self s)) (hsingle s) - have ht := biUnion_congr (of_eq_true (eq_self t)) (hsingle t) - rw [hs, ht] at this - · simp only [biUnion_singleton_eq_self] at this - exact absurd this hst.symm + · have hsingle : ∀ s : Finset σ, ∀ x : σ, x ∈ s → (Finsupp.single x 1).support = {x} := by + intros _ x _ + rw [Finsupp.support_single_ne_zero x one_ne_zero] + have hs := biUnion_congr (of_eq_true (eq_self s)) (hsingle s) + have ht := biUnion_congr (of_eq_true (eq_self t)) (hsingle t) + rw [hs, ht] at this + · simp only [biUnion_singleton_eq_self] at this + exact absurd this hst.symm all_goals intro x y; simp [Finsupp.support_single_disjoint] #align mv_polynomial.support_esymm'' MvPolynomial.support_esymm'' diff --git a/Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean b/Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean index f50c3160f30b9b..5194c5359b1254 100644 --- a/Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean +++ b/Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean @@ -443,7 +443,8 @@ theorem IsWeightedHomogeneous.weightedHomogeneousComponent_same {m : M} {p : MvP rw [coeff_weightedHomogeneousComponent] by_cases zero_coeff : coeff x p = 0 · split_ifs - rfl; rw [zero_coeff] + · rfl + rw [zero_coeff] · rw [hp zero_coeff, if_pos]; rfl theorem IsWeightedHomogeneous.weightedHomogeneousComponent_ne {m : M} (n : M) @@ -455,8 +456,11 @@ theorem IsWeightedHomogeneous.weightedHomogeneousComponent_ne {m : M} (n : M) rw [coeff_weightedHomogeneousComponent] by_cases zero_coeff : coeff x p = 0 · split_ifs - rw [zero_coeff]; rw [coeff_zero]; rw [coeff_zero] - · rw [if_neg]; rw [coeff_zero]; rw [hp zero_coeff]; exact Ne.symm hn + · rw [zero_coeff]; rw [coeff_zero] + · rw [coeff_zero] + · rw [if_neg] + · rw [coeff_zero] + · rw [hp zero_coeff]; exact Ne.symm hn /-- The weighted homogeneous components of a weighted homogeneous polynomial. -/ theorem weightedHomogeneousComponent_weighted_homogeneous_polynomial [DecidableEq M] (m n : M) diff --git a/Mathlib/RingTheory/Polynomial/Basic.lean b/Mathlib/RingTheory/Polynomial/Basic.lean index ac0f0fc632a310..8c03b571c0464a 100644 --- a/Mathlib/RingTheory/Polynomial/Basic.lean +++ b/Mathlib/RingTheory/Polynomial/Basic.lean @@ -101,7 +101,7 @@ theorem mem_degreeLT {n : ℕ} {f : R[X]} : f ∈ degreeLT R n ↔ degree f < n rw [degree, Finset.max_eq_sup_coe] rw [Finset.sup_lt_iff ?_] rotate_left - apply WithBot.bot_lt_coe + · apply WithBot.bot_lt_coe conv_rhs => simp only [mem_support_iff] intro b @@ -673,8 +673,8 @@ theorem leadingCoeffNth_mono {m n : ℕ} (H : m ≤ n) : I.leadingCoeffNth m ≤ theorem mem_leadingCoeff (x) : x ∈ I.leadingCoeff ↔ ∃ p ∈ I, Polynomial.leadingCoeff p = x := by rw [leadingCoeff, Submodule.mem_iSup_of_directed] - simp only [mem_leadingCoeffNth] - · constructor + · simp only [mem_leadingCoeffNth] + constructor · rintro ⟨i, p, hpI, _, rfl⟩ exact ⟨p, hpI, rfl⟩ rintro ⟨p, hpI, rfl⟩ @@ -998,9 +998,9 @@ protected theorem Polynomial.isNoetherianRing [inst : IsNoetherianRing R] : IsNo exact hp0 H have h1 : p.degree = (q * Polynomial.X ^ (k - q.natDegree)).degree := by rw [Polynomial.degree_mul', Polynomial.degree_X_pow] - rw [Polynomial.degree_eq_natDegree hp0, Polynomial.degree_eq_natDegree hq0] - rw [← Nat.cast_add, add_tsub_cancel_of_le, hn] - · refine' le_trans (Polynomial.natDegree_le_of_degree_le hdq) (le_of_lt h) + · rw [Polynomial.degree_eq_natDegree hp0, Polynomial.degree_eq_natDegree hq0] + rw [← Nat.cast_add, add_tsub_cancel_of_le, hn] + · refine' le_trans (Polynomial.natDegree_le_of_degree_le hdq) (le_of_lt h) rw [Polynomial.leadingCoeff_X_pow, mul_one] exact mt Polynomial.leadingCoeff_eq_zero.1 hq0 have h2 : p.leadingCoeff = (q * Polynomial.X ^ (k - q.natDegree)).leadingCoeff := by diff --git a/Mathlib/RingTheory/Polynomial/Hermite/Basic.lean b/Mathlib/RingTheory/Polynomial/Hermite/Basic.lean index 2a2df4aa2fee24..994a906c284d5f 100644 --- a/Mathlib/RingTheory/Polynomial/Hermite/Basic.lean +++ b/Mathlib/RingTheory/Polynomial/Hermite/Basic.lean @@ -110,8 +110,8 @@ theorem coeff_hermite_self (n : ℕ) : coeff (hermite n) n = 1 := by @[simp] theorem degree_hermite (n : ℕ) : (hermite n).degree = n := by rw [degree_eq_of_le_of_coeff_ne_zero] - simp_rw [degree_le_iff_coeff_zero, Nat.cast_lt] - · rintro m hnm + · simp_rw [degree_le_iff_coeff_zero, Nat.cast_lt] + rintro m hnm exact coeff_hermite_of_lt hnm · simp [coeff_hermite_self n] #align polynomial.degree_hermite Polynomial.degree_hermite @@ -210,8 +210,8 @@ theorem coeff_hermite (n k : ℕ) : coeff (hermite n) k = if Even (n + k) then (-1 : ℤ) ^ ((n - k) / 2) * (n - k - 1)‼ * Nat.choose n k else 0 := by split_ifs with h - exact coeff_hermite_of_even_add h - exact coeff_hermite_of_odd_add (Nat.odd_iff_not_even.mpr h) + · exact coeff_hermite_of_even_add h + · exact coeff_hermite_of_odd_add (Nat.odd_iff_not_even.mpr h) #align polynomial.coeff_hermite Polynomial.coeff_hermite end CoeffExplicit diff --git a/Mathlib/RingTheory/Polynomial/Nilpotent.lean b/Mathlib/RingTheory/Polynomial/Nilpotent.lean index 7c388936fb558e..c4d1e17c888980 100644 --- a/Mathlib/RingTheory/Polynomial/Nilpotent.lean +++ b/Mathlib/RingTheory/Polynomial/Nilpotent.lean @@ -121,8 +121,8 @@ theorem isUnit_of_coeff_isUnit_isNilpotent (hunit : IsUnit (P.coeff 0)) · simp_rw [← h, hdeg₂] · simp_rw [eraseLead_coeff_of_ne _ (Ne.symm hdeg), hunit] · by_cases H : i ≤ P₁.natDegree - simp_rw [eraseLead_coeff_of_ne _ (ne_of_lt (lt_of_le_of_lt H hdeg₂)), hnil i hi] - simp_rw [coeff_eq_zero_of_natDegree_lt (lt_of_not_ge H), IsNilpotent.zero] + · simp_rw [eraseLead_coeff_of_ne _ (ne_of_lt (lt_of_le_of_lt H hdeg₂)), hnil i hi] + · simp_rw [coeff_eq_zero_of_natDegree_lt (lt_of_not_ge H), IsNilpotent.zero] /-- Let `P` be a polynomial over `R`. If `P` is a unit, then all its coefficients are nilpotent, except its constant term which is a unit. diff --git a/Mathlib/RingTheory/Polynomial/Vieta.lean b/Mathlib/RingTheory/Polynomial/Vieta.lean index 78ebb933de22a1..c41e6bda67d0da 100644 --- a/Mathlib/RingTheory/Polynomial/Vieta.lean +++ b/Mathlib/RingTheory/Polynomial/Vieta.lean @@ -97,7 +97,8 @@ theorem esymm_neg (s : Multiset R) (k : ℕ) : (map Neg.neg s).esymm k = (-1) ^ intro x hx rw [(mem_powersetCard.mp hx).right.symm, ← prod_replicate, ← Multiset.map_const] nth_rw 3 [← map_id' x] - rw [← prod_map_mul, map_congr (Eq.refl _)];rfl + rw [← prod_map_mul, map_congr (Eq.refl _)] + · rfl exact fun z _ => neg_one_mul z #align multiset.esymm_neg Multiset.esymm_neg diff --git a/Mathlib/RingTheory/PowerSeries/WellKnown.lean b/Mathlib/RingTheory/PowerSeries/WellKnown.lean index a987f006c2f511..2fc1d7cbe3b573 100644 --- a/Mathlib/RingTheory/PowerSeries/WellKnown.lean +++ b/Mathlib/RingTheory/PowerSeries/WellKnown.lean @@ -171,9 +171,9 @@ theorem exp_mul_exp_eq_exp_add [Algebra ℚ A] (a b : A) : rw [mul_one_div (↑(n.choose x) : ℚ), one_div_mul_one_div] symm rw [div_eq_iff, div_mul_eq_mul_div, one_mul, choose_eq_factorial_div_factorial] - norm_cast - rw [cast_div_charZero] - · apply factorial_mul_factorial_dvd_factorial (mem_range_succ_iff.1 hx) + · norm_cast + rw [cast_div_charZero] + apply factorial_mul_factorial_dvd_factorial (mem_range_succ_iff.1 hx) · apply mem_range_succ_iff.1 hx · rintro h apply factorial_ne_zero n diff --git a/Mathlib/RingTheory/PrincipalIdealDomain.lean b/Mathlib/RingTheory/PrincipalIdealDomain.lean index d867dc9f9fa2b1..b160dc80618d99 100644 --- a/Mathlib/RingTheory/PrincipalIdealDomain.lean +++ b/Mathlib/RingTheory/PrincipalIdealDomain.lean @@ -71,8 +71,8 @@ instance (priority := 100) DivisionRing.isPrincipalIdealRing (K : Type u) [Divis IsPrincipalIdealRing K where principal S := by rcases Ideal.eq_bot_or_top S with (rfl | rfl) - apply bot_isPrincipal - apply top_isPrincipal + · apply bot_isPrincipal + · apply top_isPrincipal #align division_ring.is_principal_ideal_ring DivisionRing.isPrincipalIdealRing end diff --git a/Mathlib/RingTheory/UniqueFactorizationDomain.lean b/Mathlib/RingTheory/UniqueFactorizationDomain.lean index 5eb4818c42f0ca..e44cf987c74c01 100644 --- a/Mathlib/RingTheory/UniqueFactorizationDomain.lean +++ b/Mathlib/RingTheory/UniqueFactorizationDomain.lean @@ -1194,7 +1194,7 @@ theorem multiplicative_of_coprime (f : α → β) (a b : α) (h0 : f 0 = 0) Finset.prod_subset (Finset.subset_union_left _ (normalizedFactors b).toFinset), Finset.prod_subset (Finset.subset_union_right _ (normalizedFactors b).toFinset), ← Finset.prod_mul_distrib] - simp_rw [id, ← pow_add, this] + · simp_rw [id, ← pow_add, this] all_goals simp only [Multiset.mem_toFinset] · intro p _ hpb simp [hpb] diff --git a/Mathlib/SetTheory/Surreal/Dyadic.lean b/Mathlib/SetTheory/Surreal/Dyadic.lean index 6e119f74aa4ab5..ddb9c9b3ec89ac 100644 --- a/Mathlib/SetTheory/Surreal/Dyadic.lean +++ b/Mathlib/SetTheory/Surreal/Dyadic.lean @@ -134,7 +134,8 @@ theorem add_powHalf_succ_self_eq_powHalf (n) : powHalf (n + 1) + powHalf (n + 1) · rintro ⟨⟩ rintro ⟨⟩ apply lf_of_moveRight_le - swap; exact Sum.inl default + swap + · exact Sum.inl default calc powHalf n.succ + powHalf (n.succ + 1) ≤ powHalf n.succ + powHalf n.succ := add_le_add_left (powHalf_succ_le_powHalf _) _ diff --git a/Mathlib/Topology/Algebra/Polynomial.lean b/Mathlib/Topology/Algebra/Polynomial.lean index da4612f82ad758..722e44817348d2 100644 --- a/Mathlib/Topology/Algebra/Polynomial.lean +++ b/Mathlib/Topology/Algebra/Polynomial.lean @@ -203,7 +203,9 @@ theorem coeff_bdd_of_roots_le {B : ℝ} {d : ℕ} (f : F →+* K) {p : F[X]} (h1 calc _ ≤ max B 1 ^ (p.natDegree - i) * p.natDegree.choose i := by gcongr; apply le_max_left _ ≤ max B 1 ^ d * p.natDegree.choose i := by - gcongr; apply le_max_right; exact le_trans (Nat.sub_le _ _) h3 + gcongr + · apply le_max_right + · exact le_trans (Nat.sub_le _ _) h3 _ ≤ max B 1 ^ d * d.choose (d / 2) := by gcongr; exact (i.choose_mono h3).trans (i.choose_le_middle d) · rw [eq_one_of_roots_le hB h1 h2 h4, Polynomial.map_one, coeff_one] diff --git a/Mathlib/Topology/Algebra/UniformGroup.lean b/Mathlib/Topology/Algebra/UniformGroup.lean index b3f11ee83ea88c..aeb1fcf9d8936d 100644 --- a/Mathlib/Topology/Algebra/UniformGroup.lean +++ b/Mathlib/Topology/Algebra/UniformGroup.lean @@ -186,8 +186,7 @@ theorem uniformity_translate_mul (a : α) : ((𝓤 α).map fun x : α × α => ( @[to_additive] theorem uniformEmbedding_translate_mul (a : α) : UniformEmbedding fun x : α => x * a := { comap_uniformity := by - nth_rewrite 1 [← uniformity_translate_mul a, comap_map] - rfl + nth_rw 1 [← uniformity_translate_mul a, comap_map] rintro ⟨p₁, p₂⟩ ⟨q₁, q₂⟩ simp only [Prod.mk.injEq, mul_left_inj, imp_self] inj := mul_left_injective a } @@ -593,7 +592,7 @@ variable {G} instance Subgroup.isClosed_of_discrete [T2Space G] {H : Subgroup G} [DiscreteTopology H] : IsClosed (H : Set G) := by obtain ⟨V, V_in, VH⟩ : ∃ (V : Set G), V ∈ 𝓝 (1 : G) ∧ V ∩ (H : Set G) = {1} - exact nhds_inter_eq_singleton_of_mem_discrete H.one_mem + · exact nhds_inter_eq_singleton_of_mem_discrete H.one_mem have : (fun p : G × G => p.2 / p.1) ⁻¹' V ∈ 𝓤 G := preimage_mem_comap V_in apply isClosed_of_spaced_out this intro h h_in h' h'_in diff --git a/Mathlib/Topology/Algebra/UniformMulAction.lean b/Mathlib/Topology/Algebra/UniformMulAction.lean index a5599bda7e3e13..062f883b4c9d5b 100644 --- a/Mathlib/Topology/Algebra/UniformMulAction.lean +++ b/Mathlib/Topology/Algebra/UniformMulAction.lean @@ -175,7 +175,7 @@ instance [SMul N X] [SMulCommClass M N X] [UniformContinuousConstSMul M X] have hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x := rfl have hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x := rfl rw [hmn, hnm, map_comp, map_comp] - exact congr_arg (fun f => Completion.map f x) (funext (smul_comm _ _)) + · exact congr_arg (fun f => Completion.map f x) (funext (smul_comm _ _)) repeat' exact uniformContinuous_const_smul _⟩ @[to_additive] diff --git a/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean b/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean index ef8e66372a25ac..614ba0611d2a6d 100644 --- a/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean +++ b/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean @@ -67,14 +67,14 @@ def pullbackConeIsLimit (f : X ⟶ Z) (g : Y ⟶ Z) : IsLimit (pullbackCone f g) (by intro S constructor; swap - exact - { toFun := fun x => - ⟨⟨S.fst x, S.snd x⟩, by simpa using ConcreteCategory.congr_hom S.condition x⟩ - continuous_toFun := by - apply Continuous.subtype_mk <| Continuous.prod_mk ?_ ?_ - · exact (PullbackCone.fst S)|>.continuous_toFun - · exact (PullbackCone.snd S)|>.continuous_toFun - } + · exact + { toFun := fun x => + ⟨⟨S.fst x, S.snd x⟩, by simpa using ConcreteCategory.congr_hom S.condition x⟩ + continuous_toFun := by + apply Continuous.subtype_mk <| Continuous.prod_mk ?_ ?_ + · exact (PullbackCone.fst S)|>.continuous_toFun + · exact (PullbackCone.snd S)|>.continuous_toFun + } refine' ⟨_, _, _⟩ · delta pullbackCone ext a diff --git a/Mathlib/Topology/Category/TopCat/OpenNhds.lean b/Mathlib/Topology/Category/TopCat/OpenNhds.lean index af8bf8d7dc9281..a262ecfedc724b 100644 --- a/Mathlib/Topology/Category/TopCat/OpenNhds.lean +++ b/Mathlib/Topology/Category/TopCat/OpenNhds.lean @@ -132,7 +132,12 @@ theorem op_map_id_obj (x : X) (U : (OpenNhds x)ᵒᵖ) : (map (𝟙 X) x).op.obj /-- `Opens.map f` and `OpenNhds.map f` form a commuting square (up to natural isomorphism) with the inclusion functors into `Opens X`. -/ def inclusionMapIso (x : X) : inclusion (f x) ⋙ Opens.map f ≅ map f x ⋙ inclusion x := - NatIso.ofComponents fun U => by constructor; rfl; rfl; exact 𝟙 _; exact 𝟙 _ + NatIso.ofComponents fun U => by + constructor + · rfl + · rfl + · exact 𝟙 _ + · exact 𝟙 _ #align topological_space.open_nhds.inclusion_map_iso TopologicalSpace.OpenNhds.inclusionMapIso @[simp] diff --git a/Mathlib/Topology/Gluing.lean b/Mathlib/Topology/Gluing.lean index 0826d1b1a38971..363990e5e98034 100644 --- a/Mathlib/Topology/Gluing.lean +++ b/Mathlib/Topology/Gluing.lean @@ -132,8 +132,10 @@ theorem rel_equiv : Equivalence D.Rel := ⟨fun x => Or.inl (refl x), by rintro a b (⟨⟨⟩⟩ | ⟨x, e₁, e₂⟩) exacts [Or.inl rfl, Or.inr ⟨D.t _ _ x, by simp [e₁, e₂]⟩], by - rintro ⟨i, a⟩ ⟨j, b⟩ ⟨k, c⟩ (⟨⟨⟩⟩ | ⟨x, e₁, e₂⟩); exact id - rintro (⟨⟨⟩⟩ | ⟨y, e₃, e₄⟩); exact Or.inr ⟨x, e₁, e₂⟩ + rintro ⟨i, a⟩ ⟨j, b⟩ ⟨k, c⟩ (⟨⟨⟩⟩ | ⟨x, e₁, e₂⟩) + · exact id + rintro (⟨⟨⟩⟩ | ⟨y, e₃, e₄⟩) + · exact Or.inr ⟨x, e₁, e₂⟩ let z := (pullbackIsoProdSubtype (D.f j i) (D.f j k)).inv ⟨⟨_, _⟩, e₂.trans e₃.symm⟩ have eq₁ : (D.t j i) ((pullback.fst : _ /-(D.f j k)-/ ⟶ D.V (j, i)) z) = x := by simp [z] have eq₂ : (pullback.snd : _ ⟶ D.V _) z = y := pullbackIsoProdSubtype_inv_snd_apply _ _ _ @@ -219,7 +221,7 @@ theorem ι_eq_iff_rel (i j : D.J) (x : D.U i) (y : D.U j) : erw [sigmaIsoSigma_hom_ι_apply, sigmaIsoSigma_hom_ι_apply] exact Or.inr ⟨y, ⟨rfl, rfl⟩⟩ · rintro (⟨⟨⟩⟩ | ⟨z, e₁, e₂⟩) - rfl + · rfl dsimp only at * -- Porting note: there were `subst e₁` and `subst e₂`, instead of the `rw` rw [← e₁, ← e₂] at * @@ -297,8 +299,8 @@ theorem preimage_image_eq_image' (i j : D.J) (U : Set (𝖣.U i)) : -- Porting note: `congr 1` was here, instead of `congr_arg`, however, it did nothing. refine congr_arg ?_ ?_ rw [← Set.eq_preimage_iff_image_eq, Set.preimage_preimage] - change _ = (D.t i j ≫ D.t j i ≫ _) ⁻¹' _ - rw [𝖣.t_inv_assoc] + · change _ = (D.t i j ≫ D.t j i ≫ _) ⁻¹' _ + rw [𝖣.t_inv_assoc] rw [← isIso_iff_bijective] apply (forget TopCat).map_isIso set_option linter.uppercaseLean3 false in @@ -353,10 +355,10 @@ set_option linter.uppercaseLean3 false in theorem MkCore.t_inv (h : MkCore) (i j : h.J) (x : h.V j i) : h.t i j ((h.t j i) x) = x := by have := h.cocycle j i j x ?_ - rw [h.t_id] at this - convert Subtype.eq this - rw [h.V_id] - trivial + · rw [h.t_id] at this + · convert Subtype.eq this + rw [h.V_id] + trivial set_option linter.uppercaseLean3 false in #align Top.glue_data.mk_core.t_inv TopCat.GlueData.MkCore.t_inv diff --git a/Mathlib/Topology/Homeomorph.lean b/Mathlib/Topology/Homeomorph.lean index 478fad383fddfd..a5bcd50b44707d 100644 --- a/Mathlib/Topology/Homeomorph.lean +++ b/Mathlib/Topology/Homeomorph.lean @@ -793,8 +793,9 @@ def piSplitAt (Y : ι → Type*) [∀ j, TopologicalSpace (Y j)] : continuous_pi fun j => by dsimp only [Equiv.piSplitAt] split_ifs with h - subst h - exacts [continuous_fst, (continuous_apply _).comp continuous_snd] + · subst h + exact continuous_fst + · exact (continuous_apply _).comp continuous_snd #align homeomorph.pi_split_at Homeomorph.piSplitAt variable (Y) diff --git a/Mathlib/Topology/Homotopy/HSpaces.lean b/Mathlib/Topology/Homotopy/HSpaces.lean index d4635bfd1817fa..6207845d616a27 100644 --- a/Mathlib/Topology/Homotopy/HSpaces.lean +++ b/Mathlib/Topology/Homotopy/HSpaces.lean @@ -237,7 +237,8 @@ theorem delayReflRight_zero (γ : Path x y) : delayReflRight 0 γ = γ.trans (Pa ext t simp only [delayReflRight, trans_apply, refl_extend, Path.coe_mk_mk, Function.comp_apply, refl_apply] - split_ifs with h; swap; conv_rhs => rw [← γ.target] + split_ifs with h; swap + on_goal 1 => conv_rhs => rw [← γ.target] all_goals apply congr_arg γ; ext1; rw [qRight_zero_right] exacts [if_neg h, if_pos h] #align path.delay_refl_right_zero Path.delayReflRight_zero diff --git a/Mathlib/Topology/IndicatorConstPointwise.lean b/Mathlib/Topology/IndicatorConstPointwise.lean index 18df1ff3674dae..8838e3adede591 100644 --- a/Mathlib/Topology/IndicatorConstPointwise.lean +++ b/Mathlib/Topology/IndicatorConstPointwise.lean @@ -73,8 +73,8 @@ lemma tendsto_indicator_const_apply_iff_eventually' (b : β) classical have heart := @tendsto_ite ι L β (fun i ↦ x ∈ As i) _ (x ∈ A) _ b 0 (𝓝 b) (𝓝 (0 : β)) nhd_o nhd_b ?_ ?_ - convert heart - · by_cases hxA : x ∈ A <;> simp [hxA] + · convert heart + by_cases hxA : x ∈ A <;> simp [hxA] · simp only [principal_singleton, le_def, mem_pure] exact fun s s_nhd ↦ mem_of_mem_nhds s_nhd · simp only [principal_singleton, le_def, mem_pure] diff --git a/Mathlib/Topology/Instances/ENNReal.lean b/Mathlib/Topology/Instances/ENNReal.lean index 85cbf97b780a62..127b7af5b4cd89 100644 --- a/Mathlib/Topology/Instances/ENNReal.lean +++ b/Mathlib/Topology/Instances/ENNReal.lean @@ -648,8 +648,8 @@ theorem finset_sum_iSup_nat {α} {ι} [SemilatticeSup ι] {s : Finset α} {f : theorem mul_iSup {ι : Sort*} {f : ι → ℝ≥0∞} {a : ℝ≥0∞} : a * iSup f = ⨆ i, a * f i := by by_cases hf : ∀ i, f i = 0 · obtain rfl : f = fun _ => 0 - exact funext hf - simp only [iSup_zero_eq_zero, mul_zero] + · exact funext hf + · simp only [iSup_zero_eq_zero, mul_zero] · refine' (monotone_id.const_mul' _).map_iSup_of_continuousAt _ (mul_zero a) refine' ENNReal.Tendsto.const_mul tendsto_id (Or.inl _) exact mt iSup_eq_zero.1 hf @@ -1203,8 +1203,8 @@ theorem indicator_summable {f : α → ℝ≥0} (hf : Summable f) (s : Set α) : Summable (s.indicator f) := by refine' NNReal.summable_of_le (fun a => le_trans (le_of_eq (s.indicator_apply f a)) _) hf split_ifs - exact le_refl (f a) - exact zero_le_coe + · exact le_refl (f a) + · exact zero_le_coe #align nnreal.indicator_summable NNReal.indicator_summable theorem tsum_indicator_ne_zero {f : α → ℝ≥0} (hf : Summable f) {s : Set α} (h : ∃ a ∈ s, f a ≠ 0) : diff --git a/Mathlib/Topology/Instances/NNReal.lean b/Mathlib/Topology/Instances/NNReal.lean index e35b749d2b6603..e4a5fab834f984 100644 --- a/Mathlib/Topology/Instances/NNReal.lean +++ b/Mathlib/Topology/Instances/NNReal.lean @@ -176,8 +176,8 @@ theorem hasSum_real_toNNReal_of_nonneg {f : α → ℝ} (hf_nonneg : ∀ n, 0 @[norm_cast] theorem summable_coe {f : α → ℝ≥0} : (Summable fun a => (f a : ℝ)) ↔ Summable f := by constructor - exact fun ⟨a, ha⟩ => ⟨⟨a, ha.nonneg fun x => (f x).2⟩, hasSum_coe.1 ha⟩ - exact fun ⟨a, ha⟩ => ⟨a.1, hasSum_coe.2 ha⟩ + · exact fun ⟨a, ha⟩ => ⟨⟨a, ha.nonneg fun x => (f x).2⟩, hasSum_coe.1 ha⟩ + · exact fun ⟨a, ha⟩ => ⟨a.1, hasSum_coe.2 ha⟩ #align nnreal.summable_coe NNReal.summable_coe theorem summable_mk {f : α → ℝ} (hf : ∀ n, 0 ≤ f n) : diff --git a/Mathlib/Topology/LocallyConstant/Basic.lean b/Mathlib/Topology/LocallyConstant/Basic.lean index a25c8b31c2f86c..cb1f9655fb1287 100644 --- a/Mathlib/Topology/LocallyConstant/Basic.lean +++ b/Mathlib/Topology/LocallyConstant/Basic.lean @@ -45,9 +45,12 @@ protected theorem tfae (f : X → Y) : ∀ x, IsOpen { x' | f x' = f x }, ∀ y, IsOpen (f ⁻¹' {y}), ∀ x, ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x] := by - tfae_have 1 → 4; exact fun h y => h {y} - tfae_have 4 → 3; exact fun h x => h (f x) - tfae_have 3 → 2; exact fun h x => IsOpen.mem_nhds (h x) rfl + tfae_have 1 → 4 + · exact fun h y => h {y} + tfae_have 4 → 3 + · exact fun h x => h (f x) + tfae_have 3 → 2 + · exact fun h x => IsOpen.mem_nhds (h x) rfl tfae_have 2 → 5 · intro h x rcases mem_nhds_iff.1 (h x) with ⟨U, eq, hU, hx⟩ diff --git a/Mathlib/Topology/Order/IntermediateValue.lean b/Mathlib/Topology/Order/IntermediateValue.lean index 4883e0ddf9d62e..2e940f8a0be37e 100644 --- a/Mathlib/Topology/Order/IntermediateValue.lean +++ b/Mathlib/Topology/Order/IntermediateValue.lean @@ -70,9 +70,9 @@ on a preconnected space and `f a ≤ g a` and `g b ≤ f b`, then for some `x` w theorem intermediate_value_univ₂ [PreconnectedSpace X] {a b : X} {f g : X → α} (hf : Continuous f) (hg : Continuous g) (ha : f a ≤ g a) (hb : g b ≤ f b) : ∃ x, f x = g x := by obtain ⟨x, _, hfg, hgf⟩ : (univ ∩ { x | f x ≤ g x ∧ g x ≤ f x }).Nonempty - exact - isPreconnected_closed_iff.1 PreconnectedSpace.isPreconnected_univ _ _ (isClosed_le hf hg) - (isClosed_le hg hf) (fun _ _ => le_total _ _) ⟨a, trivial, ha⟩ ⟨b, trivial, hb⟩ + · exact + isPreconnected_closed_iff.1 PreconnectedSpace.isPreconnected_univ _ _ (isClosed_le hf hg) + (isClosed_le hg hf) (fun _ _ => le_total _ _) ⟨a, trivial, ha⟩ ⟨b, trivial, hb⟩ exact ⟨x, le_antisymm hfg hgf⟩ #align intermediate_value_univ₂ intermediate_value_univ₂ @@ -352,7 +352,7 @@ theorem IsClosed.mem_of_ge_of_forall_exists_gt {a b : α} {s : Set α} (hs : IsC have c_mem : c ∈ S := hs.csSup_mem ⟨_, ha⟩ Sbd have c_le : c ≤ b := csSup_le ⟨_, ha⟩ fun x hx => hx.2.2 cases' eq_or_lt_of_le c_le with hc hc - exact hc ▸ c_mem.1 + · exact hc ▸ c_mem.1 exfalso rcases hgt c ⟨c_mem.1, c_mem.2.1, hc⟩ with ⟨x, xs, cx, xb⟩ exact not_lt_of_le (le_csSup Sbd ⟨xs, le_trans (le_csSup Sbd ha) (le_of_lt cx), xb⟩) cx diff --git a/Mathlib/Topology/Order/ScottTopology.lean b/Mathlib/Topology/Order/ScottTopology.lean index 3af4e260a9e4aa..96b2dbca096855 100644 --- a/Mathlib/Topology/Order/ScottTopology.lean +++ b/Mathlib/Topology/Order/ScottTopology.lean @@ -238,8 +238,8 @@ lemma isLowerSet_of_isClosed : IsClosed s → IsLowerSet s := fun h ↦ lemma lowerClosure_subset_closure : ↑(lowerClosure s) ⊆ closure s := by convert closure.mono (@upperSet_le_scott α _) - rw [@IsUpperSet.closure_eq_lowerClosure α _ (upperSet α) ?_ s] - · exact instIsUpperSetUpperSet + · rw [@IsUpperSet.closure_eq_lowerClosure α _ (upperSet α) ?_ s] + exact instIsUpperSetUpperSet · exact topology_eq α lemma isClosed_Iic : IsClosed (Iic a) := diff --git a/Mathlib/Topology/Sequences.lean b/Mathlib/Topology/Sequences.lean index 223997f55a7718..c6460590019eec 100644 --- a/Mathlib/Topology/Sequences.lean +++ b/Mathlib/Topology/Sequences.lean @@ -292,8 +292,8 @@ protected theorem IsSeqCompact.totallyBounded (h : IsSeqCompact s) : TotallyBoun simpa only [forall_and, forall_mem_image, not_and] using seq_of_forall_finite_exists h refine' ⟨u, u_in, fun x _ φ hφ huφ => _⟩ obtain ⟨N, hN⟩ : ∃ N, ∀ p q, p ≥ N → q ≥ N → (u (φ p), u (φ q)) ∈ V - exact huφ.cauchySeq.mem_entourage V_in - exact hu (φ <| N + 1) (φ N) (hφ <| lt_add_one N) (hN (N + 1) N N.le_succ le_rfl) + · exact huφ.cauchySeq.mem_entourage V_in + · exact hu (φ <| N + 1) (φ N) (hφ <| lt_add_one N) (hN (N + 1) N N.le_succ le_rfl) #align is_seq_compact.totally_bounded IsSeqCompact.totallyBounded variable [IsCountablyGenerated (𝓤 X)] diff --git a/Mathlib/Topology/Sheaves/Presheaf.lean b/Mathlib/Topology/Sheaves/Presheaf.lean index 03e89d3f9b7073..0f62f78e0bcf46 100644 --- a/Mathlib/Topology/Sheaves/Presheaf.lean +++ b/Mathlib/Topology/Sheaves/Presheaf.lean @@ -346,8 +346,8 @@ def pullbackObjObjOfImageOpen {X Y : TopCat.{v}} (f : X ⟶ Y) (ℱ : Y.Presheaf have hx : IsTerminal x := { lift := fun s ↦ by fapply CostructuredArrow.homMk - change op (unop _) ⟶ op (⟨_, H⟩ : Opens _) - · refine' (homOfLE _).op + · change op (unop _) ⟶ op (⟨_, H⟩ : Opens _) + refine' (homOfLE _).op apply (Set.image_subset f s.pt.hom.unop.le).trans exact Set.image_preimage.l_u_le (SetLike.coe s.pt.left.unop) · simp [autoParam, eq_iff_true_of_subsingleton] @@ -419,8 +419,8 @@ theorem id_pushforward {X : TopCat.{w}} : pushforward C (𝟙 X) = 𝟭 (X.Presh · intros a b f ext U · erw [NatTrans.congr f (Opens.op_map_id_obj (op U))] - simp only [Functor.op_obj, eqToHom_refl, CategoryTheory.Functor.map_id, - Category.comp_id, Category.id_comp, Functor.id_obj, Functor.id_map] + · simp only [Functor.op_obj, eqToHom_refl, CategoryTheory.Functor.map_id, + Category.comp_id, Category.id_comp, Functor.id_obj, Functor.id_map] apply Pushforward.id_eq set_option linter.uppercaseLean3 false in #align Top.presheaf.id_pushforward TopCat.Presheaf.id_pushforward diff --git a/Mathlib/Topology/Sheaves/SheafCondition/Sites.lean b/Mathlib/Topology/Sheaves/SheafCondition/Sites.lean index 424e26819e33df..32095569152eed 100644 --- a/Mathlib/Topology/Sheaves/SheafCondition/Sites.lean +++ b/Mathlib/Topology/Sheaves/SheafCondition/Sites.lean @@ -137,8 +137,9 @@ variable {X : TopCat} {ι : Type*} theorem coverDense_iff_isBasis [Category ι] (B : ι ⥤ Opens X) : B.IsCoverDense (Opens.grothendieckTopology X) ↔ Opens.IsBasis (Set.range B.obj) := by rw [Opens.isBasis_iff_nbhd] - constructor; intro hd U x hx; rcases hd.1 U x hx with ⟨V, f, ⟨i, f₁, f₂, _⟩, hV⟩ - exact ⟨B.obj i, ⟨i, rfl⟩, f₁.le hV, f₂.le⟩ + constructor + · intro hd U x hx; rcases hd.1 U x hx with ⟨V, f, ⟨i, f₁, f₂, _⟩, hV⟩ + exact ⟨B.obj i, ⟨i, rfl⟩, f₁.le hV, f₂.le⟩ intro hb; constructor; intro U x hx; rcases hb hx with ⟨_, ⟨i, rfl⟩, hx, hi⟩ exact ⟨B.obj i, ⟨⟨hi⟩⟩, ⟨⟨i, 𝟙 _, ⟨⟨hi⟩⟩, rfl⟩⟩, hx⟩ #align Top.opens.cover_dense_iff_is_basis TopCat.Opens.coverDense_iff_isBasis diff --git a/Mathlib/Topology/StoneCech.lean b/Mathlib/Topology/StoneCech.lean index 482de4f79072cf..5715a3f2d98b54 100644 --- a/Mathlib/Topology/StoneCech.lean +++ b/Mathlib/Topology/StoneCech.lean @@ -295,7 +295,7 @@ end Extension theorem convergent_eqv_pure {u : Ultrafilter α} {x : α} (ux : ↑u ≤ 𝓝 x) : u ≈ pure x := fun γ tγ h₁ h₂ f hf => by - trans f x; swap; symm + trans f x; swap; on_goal 1 => symm all_goals refine' ultrafilter_extend_eq_iff.mpr (le_trans (map_mono _) (hf.tendsto _)) · apply pure_le_nhds · exact ux diff --git a/Mathlib/Topology/UniformSpace/Cauchy.lean b/Mathlib/Topology/UniformSpace/Cauchy.lean index c657f579a20438..c858aa1568337c 100644 --- a/Mathlib/Topology/UniformSpace/Cauchy.lean +++ b/Mathlib/Topology/UniformSpace/Cauchy.lean @@ -722,8 +722,8 @@ theorem setSeq_sub_aux (n : ℕ) : setSeq hf U_mem n ⊆ setSeqAux hf U_mem n := theorem setSeq_prod_subset {N m n} (hm : N ≤ m) (hn : N ≤ n) : setSeq hf U_mem m ×ˢ setSeq hf U_mem n ⊆ U N := fun p hp => by refine' (setSeqAux hf U_mem N).2.2 ⟨_, _⟩ <;> apply setSeq_sub_aux - exact setSeq_mono hf U_mem hm hp.1 - exact setSeq_mono hf U_mem hn hp.2 + · exact setSeq_mono hf U_mem hm hp.1 + · exact setSeq_mono hf U_mem hn hp.2 #align sequentially_complete.set_seq_prod_subset SequentiallyComplete.setSeq_prod_subset /-- A sequence of points such that `seq n ∈ setSeq n`. Here `setSeq` is an antitone diff --git a/Mathlib/Topology/UniformSpace/UniformEmbedding.lean b/Mathlib/Topology/UniformSpace/UniformEmbedding.lean index 6677f2ff55706e..e27a9806326cb0 100644 --- a/Mathlib/Topology/UniformSpace/UniformEmbedding.lean +++ b/Mathlib/Topology/UniformSpace/UniformEmbedding.lean @@ -286,7 +286,7 @@ theorem isComplete_of_complete_image {m : α → β} {s : Set α} (hm : UniformI intro f hf hfs rw [le_principal_iff] at hfs obtain ⟨_, ⟨x, hx, rfl⟩, hyf⟩ : ∃ y ∈ m '' s, map m f ≤ 𝓝 y - exact hs (f.map m) (hf.map hm.uniformContinuous) (le_principal_iff.2 (image_mem_map hfs)) + · exact hs (f.map m) (hf.map hm.uniformContinuous) (le_principal_iff.2 (image_mem_map hfs)) rw [map_le_iff_le_comap, ← nhds_induced, ← hm.inducing.induced] at hyf exact ⟨x, hx, hyf⟩ #align is_complete_of_complete_image isComplete_of_complete_image