From c93575a3bf66341c32a357213ba963b6052aa2d5 Mon Sep 17 00:00:00 2001 From: sgouezel Date: Wed, 4 Oct 2023 14:04:29 +0000 Subject: [PATCH] chore: cleanup some spaces (#7484) Purely cosmetic PR. --- Archive/Sensitivity.lean | 2 +- Mathlib/Algebra/GradedMonoid.lean | 2 +- .../DoldKan/FunctorGamma.lean | 2 +- .../AlgebraicTopology/DoldKan/Homotopies.lean | 2 +- Mathlib/Analysis/Analytic/IsolatedZeros.lean | 4 ++-- Mathlib/Analysis/Convex/Segment.lean | 2 +- .../CategoryTheory/Abelian/RightDerived.lean | 2 +- Mathlib/CategoryTheory/Functor/Currying.lean | 2 +- Mathlib/CategoryTheory/Generator.lean | 2 +- Mathlib/CategoryTheory/Grothendieck.lean | 2 +- .../Limits/Shapes/Equalizers.lean | 2 +- .../Limits/Shapes/Pullbacks.lean | 2 +- .../Localization/Construction.lean | 2 +- .../Monoidal/Free/Coherence.lean | 2 +- Mathlib/CategoryTheory/Preadditive/Mat.lean | 2 +- Mathlib/CategoryTheory/Shift/Basic.lean | 2 +- Mathlib/CategoryTheory/Shift/Pullback.lean | 6 +++--- Mathlib/CategoryTheory/StructuredArrow.lean | 8 ++++---- Mathlib/Combinatorics/HalesJewett.lean | 2 +- .../SimpleGraph/Connectivity/Subgraph.lean | 6 +++--- Mathlib/Data/Finset/Pointwise.lean | 2 +- Mathlib/Data/List/Basic.lean | 2 +- Mathlib/Data/PNat/Factors.lean | 2 +- Mathlib/Data/Part.lean | 2 +- .../QPF/Multivariate/Constructions/Fix.lean | 2 +- Mathlib/GroupTheory/QuotientGroup.lean | 18 +++++++++--------- .../LinearAlgebra/AffineSpace/Independent.lean | 2 +- Mathlib/LinearAlgebra/Basic.lean | 2 +- Mathlib/LinearAlgebra/Dual.lean | 2 +- Mathlib/Mathport/Notation.lean | 4 ++-- Mathlib/MeasureTheory/Integral/Bochner.lean | 2 +- Mathlib/ModelTheory/Algebra/Ring/Basic.lean | 10 +++++----- Mathlib/NumberTheory/KummerDedekind.lean | 2 +- Mathlib/NumberTheory/LegendreSymbol/Basic.lean | 4 ++-- Mathlib/NumberTheory/NumberField/Units.lean | 2 +- Mathlib/RingTheory/AdjoinRoot.lean | 2 +- Mathlib/RingTheory/Discriminant.lean | 2 +- Mathlib/RingTheory/Henselian.lean | 2 +- .../RingTheory/Localization/FractionRing.lean | 2 +- Mathlib/RingTheory/Nullstellensatz.lean | 2 +- Mathlib/RingTheory/Perfection.lean | 2 +- Mathlib/RingTheory/WittVector/Basic.lean | 2 +- Mathlib/Tactic/ByContra.lean | 2 +- Mathlib/Tactic/NoncommRing.lean | 2 +- .../Topology/ContinuousFunction/Ideals.lean | 2 +- test/linarith.lean | 4 ++-- 46 files changed, 69 insertions(+), 69 deletions(-) diff --git a/Archive/Sensitivity.lean b/Archive/Sensitivity.lean index f0f668264e412..50f32a891fcdb 100644 --- a/Archive/Sensitivity.lean +++ b/Archive/Sensitivity.lean @@ -138,7 +138,7 @@ theorem adj_iff_proj_adj {p q : Q n.succ} (h₀ : p 0 = q 0) : q ∈ p.adjacent ↔ π q ∈ (π p).adjacent := by constructor · rintro ⟨i, h_eq, h_uni⟩ - have h_i : i ≠ 0 := fun h_i => absurd h₀ (by rwa [h_i] at h_eq ) + have h_i : i ≠ 0 := fun h_i => absurd h₀ (by rwa [h_i] at h_eq) use i.pred h_i, show p (Fin.succ (Fin.pred i _)) ≠ q (Fin.succ (Fin.pred i _)) by rwa [Fin.succ_pred] intro y hy diff --git a/Mathlib/Algebra/GradedMonoid.lean b/Mathlib/Algebra/GradedMonoid.lean index 1d9f84e3a5dbd..3a35d97463552 100644 --- a/Mathlib/Algebra/GradedMonoid.lean +++ b/Mathlib/Algebra/GradedMonoid.lean @@ -658,7 +658,7 @@ theorem SetLike.coe_list_dProd (A : ι → S) [SetLike.GradedMonoid A] (fι : α /-- A version of `List.coe_dProd_set_like` with `Subtype.mk`. -/ theorem SetLike.list_dProd_eq (A : ι → S) [SetLike.GradedMonoid A] (fι : α → ι) (fA : ∀ a, A (fι a)) (l : List α) : - (@List.dProd _ _ (fun i => ↥(A i)) _ _ l fι fA ) = + (@List.dProd _ _ (fun i => ↥(A i)) _ _ l fι fA) = ⟨List.prod (l.map fun a => fA a), (l.dProdIndex_eq_map_sum fι).symm ▸ list_prod_map_mem_graded l _ _ fun i _ => (fA i).prop⟩ := diff --git a/Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean b/Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean index ca89826d63bde..cb2af4b91d7e5 100644 --- a/Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean +++ b/Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean @@ -93,7 +93,7 @@ zero otherwise. -/ def mapMono (K : ChainComplex C ℕ) {Δ' Δ : SimplexCategory} (i : Δ' ⟶ Δ) [Mono i] : K.X Δ.len ⟶ K.X Δ'.len := by by_cases Δ = Δ' - · exact eqToHom (by congr ) + · exact eqToHom (by congr) · by_cases Isδ₀ i · exact K.d Δ.len Δ'.len · exact 0 diff --git a/Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean b/Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean index 49ce641c7f3e8..d19d1145e70b7 100644 --- a/Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean +++ b/Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean @@ -112,7 +112,7 @@ theorem hσ'_eq_zero {q n m : ℕ} (hnq : n < q) (hnm : c.Rel m n) : theorem hσ'_eq {q n a m : ℕ} (ha : n = a + q) (hnm : c.Rel m n) : (hσ' q n m hnm : X _[n] ⟶ X _[m]) = ((-1 : ℤ) ^ a • X.σ ⟨a, Nat.lt_succ_iff.mpr (Nat.le.intro (Eq.symm ha))⟩) ≫ - eqToHom (by congr ) := by + eqToHom (by congr) := by simp only [hσ', hσ] split_ifs · exfalso diff --git a/Mathlib/Analysis/Analytic/IsolatedZeros.lean b/Mathlib/Analysis/Analytic/IsolatedZeros.lean index 79baade6672c1..5c78763dc8394 100644 --- a/Mathlib/Analysis/Analytic/IsolatedZeros.lean +++ b/Mathlib/Analysis/Analytic/IsolatedZeros.lean @@ -120,7 +120,7 @@ theorem locally_ne_zero (hp : HasFPowerSeriesAt f p z₀) (h : p ≠ 0) : ∀ᶠ #align has_fpower_series_at.locally_ne_zero HasFPowerSeriesAt.locally_ne_zero theorem locally_zero_iff (hp : HasFPowerSeriesAt f p z₀) : (∀ᶠ z in 𝓝 z₀, f z = 0) ↔ p = 0 := - ⟨fun hf => hp.eq_zero_of_eventually hf, fun h => eventually_eq_zero (by rwa [h] at hp )⟩ + ⟨fun hf => hp.eq_zero_of_eventually hf, fun h => eventually_eq_zero (by rwa [h] at hp)⟩ #align has_fpower_series_at.locally_zero_iff HasFPowerSeriesAt.locally_zero_iff end HasFPowerSeriesAt @@ -134,7 +134,7 @@ theorem eventually_eq_zero_or_eventually_ne_zero (hf : AnalyticAt 𝕜 f z₀) : (∀ᶠ z in 𝓝 z₀, f z = 0) ∨ ∀ᶠ z in 𝓝[≠] z₀, f z ≠ 0 := by rcases hf with ⟨p, hp⟩ by_cases h : p = 0 - · exact Or.inl (HasFPowerSeriesAt.eventually_eq_zero (by rwa [h] at hp )) + · exact Or.inl (HasFPowerSeriesAt.eventually_eq_zero (by rwa [h] at hp)) · exact Or.inr (hp.locally_ne_zero h) #align analytic_at.eventually_eq_zero_or_eventually_ne_zero AnalyticAt.eventually_eq_zero_or_eventually_ne_zero diff --git a/Mathlib/Analysis/Convex/Segment.lean b/Mathlib/Analysis/Convex/Segment.lean index 5e1ba737891ce..73cdae64cf075 100644 --- a/Mathlib/Analysis/Convex/Segment.lean +++ b/Mathlib/Analysis/Convex/Segment.lean @@ -300,7 +300,7 @@ lemma segment_inter_eq_endpoint_of_linearIndependent_sub rw [Hx, Hy, smul_add, smul_add] at H have : c + q • (y - c) = c + p • (x - c) := by convert H using 1 <;> simp [sub_smul] - obtain ⟨rfl, rfl⟩ : p = 0 ∧ q = 0 := h.eq_zero_of_pair' ((add_right_inj c).1 this ).symm + obtain ⟨rfl, rfl⟩ : p = 0 ∧ q = 0 := h.eq_zero_of_pair' ((add_right_inj c).1 this).symm simp end OrderedRing diff --git a/Mathlib/CategoryTheory/Abelian/RightDerived.lean b/Mathlib/CategoryTheory/Abelian/RightDerived.lean index 96594270e5183..31f6ac000e864 100644 --- a/Mathlib/CategoryTheory/Abelian/RightDerived.lean +++ b/Mathlib/CategoryTheory/Abelian/RightDerived.lean @@ -201,7 +201,7 @@ theorem exact_of_map_injectiveResolution (P : InjectiveResolution X) [PreservesF Preadditive.exact_of_iso_of_exact' (F.map (P.ι.f 0)) (F.map (P.cocomplex.d 0 1)) _ _ (Iso.refl _) (Iso.refl _) (HomologicalComplex.xNextIso ((F.mapHomologicalComplex _).obj P.cocomplex) rfl).symm (by simp) - (by rw [Iso.refl_hom, Category.id_comp, Iso.symm_hom, HomologicalComplex.dFrom_eq] <;> congr ) + (by rw [Iso.refl_hom, Category.id_comp, Iso.symm_hom, HomologicalComplex.dFrom_eq] <;> congr) (preserves_exact_of_preservesFiniteLimits_of_mono _ P.exact₀) #align category_theory.abelian.functor.exact_of_map_injective_resolution CategoryTheory.Abelian.Functor.exact_of_map_injectiveResolution diff --git a/Mathlib/CategoryTheory/Functor/Currying.lean b/Mathlib/CategoryTheory/Functor/Currying.lean index d531fd061e633..5dddb6950b3cb 100644 --- a/Mathlib/CategoryTheory/Functor/Currying.lean +++ b/Mathlib/CategoryTheory/Functor/Currying.lean @@ -88,7 +88,7 @@ def currying : C ⥤ D ⥤ E ≌ C × D ⥤ E := (NatIso.ofComponents fun F => NatIso.ofComponents fun X => NatIso.ofComponents fun Y => Iso.refl _) (NatIso.ofComponents fun F => NatIso.ofComponents (fun X => eqToIso (by simp)) - (by intros X Y f; cases X; cases Y; cases f; dsimp at *; rw [←F.map_comp]; simp )) + (by intros X Y f; cases X; cases Y; cases f; dsimp at *; rw [←F.map_comp]; simp)) #align category_theory.currying CategoryTheory.currying /-- `F.flip` is isomorphic to uncurrying `F`, swapping the variables, and currying. -/ diff --git a/Mathlib/CategoryTheory/Generator.lean b/Mathlib/CategoryTheory/Generator.lean index 87cc9d0c11c5f..f3dc72ae46b04 100644 --- a/Mathlib/CategoryTheory/Generator.lean +++ b/Mathlib/CategoryTheory/Generator.lean @@ -291,7 +291,7 @@ theorem hasInitial_of_isCoseparating [WellPowered C] [HasLimits C] {𝒢 : Set C let t := Pi.lift (@Sigma.snd 𝒢 fun G => A ⟶ (G : C)) haveI : Mono t := (isCoseparating_iff_mono 𝒢).1 h𝒢 A exact Subobject.ofLEMk _ (pullback.fst : pullback s t ⟶ _) bot_le ≫ pullback.snd - · suffices ∀ (g : Subobject.underlying.obj ⊥ ⟶ A ), f = g by + · suffices ∀ (g : Subobject.underlying.obj ⊥ ⟶ A), f = g by apply this intro g suffices IsSplitEpi (equalizer.ι f g) by exact eq_of_epi_equalizer diff --git a/Mathlib/CategoryTheory/Grothendieck.lean b/Mathlib/CategoryTheory/Grothendieck.lean index 06aac56f15140..65e5a56d19e84 100644 --- a/Mathlib/CategoryTheory/Grothendieck.lean +++ b/Mathlib/CategoryTheory/Grothendieck.lean @@ -196,7 +196,7 @@ def grothendieckTypeToCat : Grothendieck (G ⋙ typeToCat) ≌ G.Elements where rintro ⟨_, ⟨⟩⟩ ⟨_, ⟨⟩⟩ ⟨base, ⟨⟨f⟩⟩⟩ dsimp at * simp - rfl ) + rfl) counitIso := NatIso.ofComponents (fun X => by diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean b/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean index ff692996c1668..d5f7fe6545f16 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean @@ -169,7 +169,7 @@ def walkingParallelPairOpEquiv : WalkingParallelPair ≌ WalkingParallelPairᵒ counitIso := NatIso.ofComponents (fun j => eqToIso (by induction' j with X - cases X <;> rfl )) + cases X <;> rfl)) (fun {i} {j} f => by induction' i with i induction' j with j diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean index 62a4786e2edc7..4cb70aaf5401b 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean @@ -1594,7 +1594,7 @@ open WalkingCospan noncomputable def pullbackIsPullbackOfCompMono (f : X ⟶ W) (g : Y ⟶ W) (i : W ⟶ Z) [Mono i] [HasPullback f g] : IsLimit (PullbackCone.mk pullback.fst pullback.snd (show pullback.fst ≫ f ≫ i = pullback.snd ≫ g ≫ i from by -- Porting note: used to be _ - simp only [← Category.assoc]; rw [cancel_mono]; apply pullback.condition )) := + simp only [← Category.assoc]; rw [cancel_mono]; apply pullback.condition)) := PullbackCone.isLimitOfCompMono f g i _ (limit.isLimit (cospan f g)) #align category_theory.limits.pullback_is_pullback_of_comp_mono CategoryTheory.Limits.pullbackIsPullbackOfCompMono diff --git a/Mathlib/CategoryTheory/Localization/Construction.lean b/Mathlib/CategoryTheory/Localization/Construction.lean index d69043faa1215..4e725ff43f8cf 100644 --- a/Mathlib/CategoryTheory/Localization/Construction.lean +++ b/Mathlib/CategoryTheory/Localization/Construction.lean @@ -345,7 +345,7 @@ def inverse : W.FunctorsInverting D ⥤ W.Localization ⥤ D ext X simp only [NatTrans.comp_app, eqToHom_app, eqToHom_refl, comp_id, id_comp, NatTrans.hcomp_id_app, NatTrans.id_app, Functor.map_id] - rfl ) + rfl) map_comp τ₁ τ₂ := natTrans_hcomp_injective (by diff --git a/Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean b/Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean index afba63f365e0d..94721e9ac85c5 100644 --- a/Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean +++ b/Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean @@ -308,7 +308,7 @@ def normalizeIso : tensorFunc C ≅ normalize' C := congr 2 erw [← reassoc_of% h₂] rw [← h₃, ← Category.assoc, ← id_tensor_comp_tensor_id, h₄] - rfl ) + rfl) #align category_theory.free_monoidal_category.normalize_iso CategoryTheory.FreeMonoidalCategory.normalizeIso /-- The isomorphism between an object and its normal form is natural. -/ diff --git a/Mathlib/CategoryTheory/Preadditive/Mat.lean b/Mathlib/CategoryTheory/Preadditive/Mat.lean index 5724c90d79801..50f18610473e9 100644 --- a/Mathlib/CategoryTheory/Preadditive/Mat.lean +++ b/Mathlib/CategoryTheory/Preadditive/Mat.lean @@ -252,7 +252,7 @@ instance hasFiniteBiproducts : HasFiniteBiproducts (Mat_ C) where simp · rw [dif_neg h, dif_neg (Ne.symm h)] · rw [dif_neg h, dif_neg] - tauto ) } + tauto) } set_option linter.uppercaseLean3 false in #align category_theory.Mat_.has_finite_biproducts CategoryTheory.Mat_.hasFiniteBiproducts diff --git a/Mathlib/CategoryTheory/Shift/Basic.lean b/Mathlib/CategoryTheory/Shift/Basic.lean index e3069e5650cae..d09a2d1a1cea1 100644 --- a/Mathlib/CategoryTheory/Shift/Basic.lean +++ b/Mathlib/CategoryTheory/Shift/Basic.lean @@ -749,7 +749,7 @@ def hasShiftOfFullyFaithful : congr 1 erw [(i n).hom.naturality] dsimp - simp ) + simp) add_zero_hom_app := fun n X => F.map_injective (by have := dcongr_arg (fun a => (i a).hom.app X) (add_zero n) simp [this, ← NatTrans.naturality_assoc, eqToHom_map, diff --git a/Mathlib/CategoryTheory/Shift/Pullback.lean b/Mathlib/CategoryTheory/Shift/Pullback.lean index 2138341d07a60..bfda2f780e9f3 100644 --- a/Mathlib/CategoryTheory/Shift/Pullback.lean +++ b/Mathlib/CategoryTheory/Shift/Pullback.lean @@ -75,7 +75,7 @@ lemma pullbackShiftFunctorZero_hom_app : rfl lemma pullbackShiftFunctorAdd'_inv_app : - (shiftFunctorAdd' _ a₁ a₂ a₃ h ).inv.app X = + (shiftFunctorAdd' _ a₁ a₂ a₃ h).inv.app X = (shiftFunctor (PullbackShift C φ) a₂).map ((pullbackShiftIso C φ a₁ b₁ h₁).hom.app X) ≫ (pullbackShiftIso C φ a₂ b₂ h₂).hom.app _ ≫ (shiftFunctorAdd' C b₁ b₂ b₃ (by rw [h₁, h₂, h₃, ← h, φ.map_add])).inv.app X ≫ @@ -91,12 +91,12 @@ lemma pullbackShiftFunctorAdd'_inv_app : apply eqToHom_map lemma pullbackShiftFunctorAdd'_hom_app : - (shiftFunctorAdd' _ a₁ a₂ a₃ h ).hom.app X = + (shiftFunctorAdd' _ a₁ a₂ a₃ h).hom.app X = (pullbackShiftIso C φ a₃ b₃ h₃).hom.app X ≫ (shiftFunctorAdd' C b₁ b₂ b₃ (by rw [h₁, h₂, h₃, ← h, φ.map_add])).hom.app X ≫ (pullbackShiftIso C φ a₂ b₂ h₂).inv.app _ ≫ (shiftFunctor (PullbackShift C φ) a₂).map ((pullbackShiftIso C φ a₁ b₁ h₁).inv.app X) := by - rw [← cancel_epi ((shiftFunctorAdd' _ a₁ a₂ a₃ h ).inv.app X), Iso.inv_hom_id_app, + rw [← cancel_epi ((shiftFunctorAdd' _ a₁ a₂ a₃ h).inv.app X), Iso.inv_hom_id_app, pullbackShiftFunctorAdd'_inv_app φ X a₁ a₂ a₃ h b₁ b₂ b₃ h₁ h₂ h₃, assoc, assoc, assoc, Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app_assoc, Iso.hom_inv_id_app_assoc, ← Functor.map_comp, Iso.hom_inv_id_app, Functor.map_id] diff --git a/Mathlib/CategoryTheory/StructuredArrow.lean b/Mathlib/CategoryTheory/StructuredArrow.lean index 12e60bfc576ca..a039b5ea3bc0e 100644 --- a/Mathlib/CategoryTheory/StructuredArrow.lean +++ b/Mathlib/CategoryTheory/StructuredArrow.lean @@ -832,12 +832,12 @@ def structuredArrowOpEquivalence (F : C ⥤ D) (d : D) : (fun X => (StructuredArrow.isoMk (Iso.refl _)).op) fun {X Y} f => Quiver.Hom.unop_inj <| by apply CommaMorphism.ext <;> - dsimp [StructuredArrow.isoMk, Comma.isoMk,StructuredArrow.homMk]; simp ) + dsimp [StructuredArrow.isoMk, Comma.isoMk,StructuredArrow.homMk]; simp) (NatIso.ofComponents (fun X => CostructuredArrow.isoMk (Iso.refl _)) fun {X Y} f => by apply CommaMorphism.ext <;> - dsimp [CostructuredArrow.isoMk, Comma.isoMk, CostructuredArrow.homMk]; simp ) + dsimp [CostructuredArrow.isoMk, Comma.isoMk, CostructuredArrow.homMk]; simp) #align category_theory.structured_arrow_op_equivalence CategoryTheory.structuredArrowOpEquivalence /-- For a functor `F : C ⥤ D` and an object `d : D`, the category of costructured arrows @@ -852,12 +852,12 @@ def costructuredArrowOpEquivalence (F : C ⥤ D) (d : D) : (fun X => (CostructuredArrow.isoMk (Iso.refl _)).op) fun {X Y} f => Quiver.Hom.unop_inj <| by apply CommaMorphism.ext <;> - dsimp [CostructuredArrow.isoMk, CostructuredArrow.homMk, Comma.isoMk]; simp ) + dsimp [CostructuredArrow.isoMk, CostructuredArrow.homMk, Comma.isoMk]; simp) (NatIso.ofComponents (fun X => StructuredArrow.isoMk (Iso.refl _)) fun {X Y} f => by apply CommaMorphism.ext <;> - dsimp [StructuredArrow.isoMk, StructuredArrow.homMk, Comma.isoMk]; simp ) + dsimp [StructuredArrow.isoMk, StructuredArrow.homMk, Comma.isoMk]; simp) #align category_theory.costructured_arrow_op_equivalence CategoryTheory.costructuredArrowOpEquivalence end CategoryTheory diff --git a/Mathlib/Combinatorics/HalesJewett.lean b/Mathlib/Combinatorics/HalesJewett.lean index 0a63df3032708..4f360d634c0fc 100644 --- a/Mathlib/Combinatorics/HalesJewett.lean +++ b/Mathlib/Combinatorics/HalesJewett.lean @@ -343,7 +343,7 @@ theorem exists_mono_homothetic_copy {M κ : Type*} [AddCommMonoid M] (S : Finset obtain ⟨ι, _inst, hι⟩ := Line.exists_mono_in_high_dimension S κ specialize hι fun v => C <| ∑ i, v i obtain ⟨l, c, hl⟩ := hι - set s : Finset ι := Finset.univ.filter (fun i => l.idxFun i = none ) with hs + set s : Finset ι := Finset.univ.filter (fun i => l.idxFun i = none) with hs refine' ⟨s.card, Finset.card_pos.mpr ⟨l.proper.choose, _⟩, ∑ i in sᶜ, ((l.idxFun i).map _).getD 0, c, _⟩ diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean index 34d4c80d00696..49502ecec6844 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean @@ -98,7 +98,7 @@ protected lemma Connected.mono' {H H' : G.Subgraph} exact h.mono ⟨hv.le, hle⟩ hv protected lemma Connected.sup {H K : G.Subgraph} - (hH : H.Connected) (hK : K.Connected) (hn : (H ⊓ K).verts.Nonempty ) : + (hH : H.Connected) (hK : K.Connected) (hn : (H ⊓ K).verts.Nonempty) : (H ⊔ K).Connected := by rw [Subgraph.connected_iff', connected_iff_exists_forall_reachable] obtain ⟨u, hu, hu'⟩ := hn @@ -118,7 +118,7 @@ lemma _root_.SimpleGraph.Walk.toSubgraph_connected {u v : V} (p : G.Walk u v) : lemma induce_union_connected {H : G.Subgraph} {s t : Set V} (sconn : (H.induce s).Connected) (tconn : (H.induce t).Connected) - (sintert : (s ⊓ t).Nonempty ) : + (sintert : (s ⊓ t).Nonempty) : (H.induce (s ∪ t)).Connected := by refine (sconn.sup tconn sintert).mono ?_ ?_ · apply le_induce_union @@ -161,7 +161,7 @@ lemma connected_induce_iff : (G.induce s).Connected ↔ ((⊤ : G.Subgraph).indu lemma induce_union_connected {s t : Set V} (sconn : (G.induce s).Connected) (tconn : (G.induce t).Connected) - (sintert : (s ∩ t).Nonempty ) : + (sintert : (s ∩ t).Nonempty) : (G.induce (s ∪ t)).Connected := by rw [connected_induce_iff] at sconn tconn ⊢ exact Subgraph.induce_union_connected sconn tconn sintert diff --git a/Mathlib/Data/Finset/Pointwise.lean b/Mathlib/Data/Finset/Pointwise.lean index 337bbdccc12b1..6d21ccce88665 100644 --- a/Mathlib/Data/Finset/Pointwise.lean +++ b/Mathlib/Data/Finset/Pointwise.lean @@ -623,7 +623,7 @@ theorem singleton_div (a : α) : {a} / s = s.image ((· / ·) a) := #align finset.singleton_div Finset.singleton_div #align finset.singleton_sub Finset.singleton_sub --- @[to_additive (attr := simp )] -- Porting note: simp can prove this & the additive version +-- @[to_additive (attr := simp)] -- Porting note: simp can prove this & the additive version @[to_additive] theorem singleton_div_singleton (a b : α) : ({a} : Finset α) / {b} = {a / b} := image₂_singleton diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean index 481bb983dc20b..e9a1a192e0180 100644 --- a/Mathlib/Data/List/Basic.lean +++ b/Mathlib/Data/List/Basic.lean @@ -1242,7 +1242,7 @@ theorem get?_injective {α : Type u} {xs : List α} {i j : ℕ} (h₀ : i < xs.l case succ.succ => congr; cases h₁ apply tail_ih <;> solve_by_elim [lt_of_succ_lt_succ] - all_goals ( dsimp at h₂; cases' h₁ with _ _ h h') + all_goals (dsimp at h₂; cases' h₁ with _ _ h h') · cases (h x (mem_iff_get?.mpr ⟨_, h₂.symm⟩) rfl) · cases (h x (mem_iff_get?.mpr ⟨_, h₂⟩) rfl) #align list.nth_injective List.get?_injective diff --git a/Mathlib/Data/PNat/Factors.lean b/Mathlib/Data/PNat/Factors.lean index c36cb520eec71..dba3f7dca0451 100644 --- a/Mathlib/Data/PNat/Factors.lean +++ b/Mathlib/Data/PNat/Factors.lean @@ -303,7 +303,7 @@ theorem factorMultiset_mul (n m : ℕ+) : #align pnat.factor_multiset_mul PNat.factorMultiset_mul theorem factorMultiset_pow (n : ℕ+) (m : ℕ) : - factorMultiset (Pow.pow n m ) = m • factorMultiset n := by + factorMultiset (Pow.pow n m) = m • factorMultiset n := by let u := factorMultiset n have : n = u.prod := (prod_factorMultiset n).symm rw [this, ← PrimeMultiset.prod_smul] diff --git a/Mathlib/Data/Part.lean b/Mathlib/Data/Part.lean index 41fd75471d5dd..b392acee0e1d1 100644 --- a/Mathlib/Data/Part.lean +++ b/Mathlib/Data/Part.lean @@ -387,7 +387,7 @@ theorem of_toOption (o : Part α) [Decidable o.Dom] : ofOption (toOption o) = o noncomputable def equivOption : Part α ≃ Option α := haveI := Classical.dec ⟨fun o => toOption o, ofOption, fun o => of_toOption o, fun o => - Eq.trans (by dsimp; congr ) (to_ofOption o)⟩ + Eq.trans (by dsimp; congr) (to_ofOption o)⟩ #align part.equiv_option Part.equivOption /-- We give `Part α` the order where everything is greater than `none`. -/ diff --git a/Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean b/Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean index 81b49a8af1aa1..6a80c89fd683c 100644 --- a/Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean +++ b/Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean @@ -106,7 +106,7 @@ set_option linter.uppercaseLean3 false in #align mvqpf.recF_eq_of_Wequiv MvQPF.recF_eq_of_wEquiv theorem wEquiv.abs' {α : TypeVec n} (x y : q.P.W α) - (h : MvQPF.abs (q.P.wDest' x ) = MvQPF.abs (q.P.wDest' y)) : + (h : MvQPF.abs (q.P.wDest' x) = MvQPF.abs (q.P.wDest' y)) : WEquiv x y := by revert h apply q.P.w_cases _ x diff --git a/Mathlib/GroupTheory/QuotientGroup.lean b/Mathlib/GroupTheory/QuotientGroup.lean index 75632b3d95838..427acc85cad07 100644 --- a/Mathlib/GroupTheory/QuotientGroup.lean +++ b/Mathlib/GroupTheory/QuotientGroup.lean @@ -156,37 +156,37 @@ instance Quotient.commGroup {G : Type*} [CommGroup G] (N : Subgroup G) : CommGro local notation " Q " => G ⧸ N @[to_additive (attr := simp)] -theorem mk_one : ((1 : G) : Q ) = 1 := +theorem mk_one : ((1 : G) : Q) = 1 := rfl #align quotient_group.coe_one QuotientGroup.mk_one #align quotient_add_group.coe_zero QuotientAddGroup.mk_zero @[to_additive (attr := simp)] -theorem mk_mul (a b : G) : ((a * b : G) : Q ) = a * b := +theorem mk_mul (a b : G) : ((a * b : G) : Q) = a * b := rfl #align quotient_group.coe_mul QuotientGroup.mk_mul #align quotient_add_group.coe_add QuotientAddGroup.mk_add @[to_additive (attr := simp)] -theorem mk_inv (a : G) : ((a⁻¹ : G) : Q ) = (a : Q)⁻¹ := +theorem mk_inv (a : G) : ((a⁻¹ : G) : Q) = (a : Q)⁻¹ := rfl #align quotient_group.coe_inv QuotientGroup.mk_inv #align quotient_add_group.coe_neg QuotientAddGroup.mk_neg @[to_additive (attr := simp)] -theorem mk_div (a b : G) : ((a / b : G) : Q ) = a / b := +theorem mk_div (a b : G) : ((a / b : G) : Q) = a / b := rfl #align quotient_group.coe_div QuotientGroup.mk_div #align quotient_add_group.coe_sub QuotientAddGroup.mk_sub @[to_additive (attr := simp)] -theorem mk_pow (a : G) (n : ℕ) : ((a ^ n : G) : Q ) = (a : Q) ^ n := +theorem mk_pow (a : G) (n : ℕ) : ((a ^ n : G) : Q) = (a : Q) ^ n := rfl #align quotient_group.coe_pow QuotientGroup.mk_pow #align quotient_add_group.coe_nsmul QuotientAddGroup.mk_nsmul @[to_additive (attr := simp)] -theorem mk_zpow (a : G) (n : ℤ) : ((a ^ n : G) : Q ) = (a : Q) ^ n := +theorem mk_zpow (a : G) (n : ℤ) : ((a ^ n : G) : Q) = (a : Q) ^ n := rfl #align quotient_group.coe_zpow QuotientGroup.mk_zpow #align quotient_add_group.coe_zsmul QuotientAddGroup.mk_zsmul @@ -211,13 +211,13 @@ def lift (φ : G →* M) (HN : N ≤ φ.ker) : Q →* M := #align quotient_add_group.lift QuotientAddGroup.lift @[to_additive (attr := simp)] -theorem lift_mk {φ : G →* M} (HN : N ≤ φ.ker) (g : G) : lift N φ HN (g : Q ) = φ g := +theorem lift_mk {φ : G →* M} (HN : N ≤ φ.ker) (g : G) : lift N φ HN (g : Q) = φ g := rfl #align quotient_group.lift_mk QuotientGroup.lift_mk #align quotient_add_group.lift_mk QuotientAddGroup.lift_mk @[to_additive (attr := simp)] -theorem lift_mk' {φ : G →* M} (HN : N ≤ φ.ker) (g : G) : lift N φ HN (mk g : Q ) = φ g := +theorem lift_mk' {φ : G →* M} (HN : N ≤ φ.ker) (g : G) : lift N φ HN (mk g : Q) = φ g := rfl -- TODO: replace `mk` with `mk'`) #align quotient_group.lift_mk' QuotientGroup.lift_mk' @@ -225,7 +225,7 @@ theorem lift_mk' {φ : G →* M} (HN : N ≤ φ.ker) (g : G) : lift N φ HN (mk @[to_additive (attr := simp)] theorem lift_quot_mk {φ : G →* M} (HN : N ≤ φ.ker) (g : G) : - lift N φ HN (Quot.mk _ g : Q ) = φ g := + lift N φ HN (Quot.mk _ g : Q) = φ g := rfl #align quotient_group.lift_quot_mk QuotientGroup.lift_quot_mk #align quotient_add_group.lift_quot_mk QuotientAddGroup.lift_quot_mk diff --git a/Mathlib/LinearAlgebra/AffineSpace/Independent.lean b/Mathlib/LinearAlgebra/AffineSpace/Independent.lean index cf0410409315d..7fbbf1a6fc131 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/Independent.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/Independent.lean @@ -209,7 +209,7 @@ theorem affineIndependent_iff_indicator_eq_of_affineCombination_eq (p : ι → P simp only [Set.indicator, Finset.mem_coe, ite_eq_right_iff] intro h by_contra - exact ( mt (@Set.mem_union_right _ i ↑s2 ↑s1) hi) h + exact (mt (@Set.mem_union_right _ i ↑s2 ↑s1) hi) h simp [h₁, h₂] · intro ha s w hw hs i0 hi0 let w1 : ι → k := Function.update (Function.const ι 0) i0 1 diff --git a/Mathlib/LinearAlgebra/Basic.lean b/Mathlib/LinearAlgebra/Basic.lean index 226b6f2369cab..371235e570cb1 100644 --- a/Mathlib/LinearAlgebra/Basic.lean +++ b/Mathlib/LinearAlgebra/Basic.lean @@ -298,7 +298,7 @@ instance [Nontrivial M] : Nontrivial (Module.End R M) := by @[simp, norm_cast] theorem coeFn_sum {ι : Type*} (t : Finset ι) (f : ι → M →ₛₗ[σ₁₂] M₂) : - ⇑(∑ i in t, f i ) = ∑ i in t, (f i : M → M₂) := + ⇑(∑ i in t, f i) = ∑ i in t, (f i : M → M₂) := _root_.map_sum (show AddMonoidHom (M →ₛₗ[σ₁₂] M₂) (M → M₂) from { toFun := FunLike.coe, diff --git a/Mathlib/LinearAlgebra/Dual.lean b/Mathlib/LinearAlgebra/Dual.lean index e0af723e49b9e..9ed86f36983d5 100644 --- a/Mathlib/LinearAlgebra/Dual.lean +++ b/Mathlib/LinearAlgebra/Dual.lean @@ -683,7 +683,7 @@ variable [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] open Lean.Elab.Tactic in /-- Try using `Set.to_finite` to dispatch a `Set.finite` goal. -/ def evalUseFiniteInstance : TacticM Unit := do - evalTactic (← `(tactic| intros; apply Set.toFinite )) + evalTactic (← `(tactic| intros; apply Set.toFinite)) elab "use_finite_instance" : tactic => evalUseFiniteInstance diff --git a/Mathlib/Mathport/Notation.lean b/Mathlib/Mathport/Notation.lean index 68feb8442d81f..ae24db14f4519 100644 --- a/Mathlib/Mathport/Notation.lean +++ b/Mathlib/Mathport/Notation.lean @@ -336,7 +336,7 @@ partial def matchFoldl (lit x y : Name) (smatcher : Matcher) (sinit : Matcher) : matchFoldl lit x y smatcher sinit s /-- Create a `Term` that represents a matcher for `foldl` notation. -Reminder: `( lit ","* => foldl (x y => scopedTerm) init )` -/ +Reminder: `( lit ","* => foldl (x y => scopedTerm) init)` -/ partial def mkFoldlMatcher (lit x y : Name) (scopedTerm init : Term) (boundNames : HashSet Name) : OptionT TermElabM (List Name × Term) := do -- Build the `scopedTerm` matcher with `x` and `y` as additional variables @@ -346,7 +346,7 @@ partial def mkFoldlMatcher (lit x y : Name) (scopedTerm init : Term) (boundNames return (keys ++ keys', ← ``(matchFoldl $(quote lit) $(quote x) $(quote y) $smatcher $sinit)) /-- Create a `Term` that represents a matcher for `foldr` notation. -Reminder: `( lit ","* => foldr (x y => scopedTerm) init )` -/ +Reminder: `( lit ","* => foldr (x y => scopedTerm) init)` -/ partial def mkFoldrMatcher (lit x y : Name) (scopedTerm init : Term) (boundNames : HashSet Name) : OptionT TermElabM (List Name × Term) := do -- Build the `scopedTerm` matcher with `x` and `y` as additional variables diff --git a/Mathlib/MeasureTheory/Integral/Bochner.lean b/Mathlib/MeasureTheory/Integral/Bochner.lean index ffffa70d14ad4..bda79c85dc27e 100644 --- a/Mathlib/MeasureTheory/Integral/Bochner.lean +++ b/Mathlib/MeasureTheory/Integral/Bochner.lean @@ -1379,7 +1379,7 @@ theorem norm_integral_le_integral_norm (f : α → G) : ‖∫ a, f a ∂μ‖ calc ‖∫ a, f a ∂μ‖ ≤ ENNReal.toReal (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ) := norm_integral_le_lintegral_norm _ - _ = ∫ a, ‖f a‖ ∂μ := (integral_eq_lintegral_of_nonneg_ae le_ae <| h.norm).symm ) + _ = ∫ a, ‖f a‖ ∂μ := (integral_eq_lintegral_of_nonneg_ae le_ae <| h.norm).symm) fun h : ¬AEStronglyMeasurable f μ => by rw [integral_non_aestronglyMeasurable h, norm_zero] exact integral_nonneg_of_ae le_ae diff --git a/Mathlib/ModelTheory/Algebra/Ring/Basic.lean b/Mathlib/ModelTheory/Algebra/Ring/Basic.lean index 2be5d6ffd4375..bfc225a31955a 100644 --- a/Mathlib/ModelTheory/Algebra/Ring/Basic.lean +++ b/Mathlib/ModelTheory/Algebra/Ring/Basic.lean @@ -154,19 +154,19 @@ class CompatibleRing (R : Type*) [Add R] [Mul R] [Neg R] [One R] [Zero R] extends Language.ring.Structure R where /-- Addition in the `Language.ring.Structure` is the same as the addition given by the `Add` instance -/ - ( funMap_add : ∀ x, funMap addFunc x = x 0 + x 1 ) + funMap_add : ∀ x, funMap addFunc x = x 0 + x 1 /-- Multiplication in the `Language.ring.Structure` is the same as the multiplication given by the `Mul` instance -/ - ( funMap_mul : ∀ x, funMap mulFunc x = x 0 * x 1 ) + funMap_mul : ∀ x, funMap mulFunc x = x 0 * x 1 /-- Negation in the `Language.ring.Structure` is the same as the negation given by the `Neg` instance -/ - ( funMap_neg : ∀ x, funMap negFunc x = -x 0 ) + funMap_neg : ∀ x, funMap negFunc x = -x 0 /-- The constant `0` in the `Language.ring.Structure` is the same as the constant given by the `Zero` instance -/ - ( funMap_zero : ∀ x, funMap (zeroFunc : Language.ring.Constants) x = 0 ) + funMap_zero : ∀ x, funMap (zeroFunc : Language.ring.Constants) x = 0 /-- The constant `1` in the `Language.ring.Structure` is the same as the constant given by the `One` instance -/ - ( funMap_one : ∀ x, funMap (oneFunc : Language.ring.Constants) x = 1 ) + funMap_one : ∀ x, funMap (oneFunc : Language.ring.Constants) x = 1 open CompatibleRing diff --git a/Mathlib/NumberTheory/KummerDedekind.lean b/Mathlib/NumberTheory/KummerDedekind.lean index 7a3c9ee2c208c..f3ec94c3ec3d6 100644 --- a/Mathlib/NumberTheory/KummerDedekind.lean +++ b/Mathlib/NumberTheory/KummerDedekind.lean @@ -144,7 +144,7 @@ theorem comap_map_eq_map_adjoin_of_coprime_conductor (⟨z, hz⟩ : R) ∈ I.map (algebraMap R R) by rw [← this, ← temp] obtain ⟨a, ha⟩ := (Set.mem_image _ _ _).mp (prod_mem_ideal_map_of_mem_conductor hp - (show z ∈ I.map (algebraMap R S) by rwa [Ideal.mem_comap] at hy )) + (show z ∈ I.map (algebraMap R S) by rwa [Ideal.mem_comap] at hy)) use a + algebraMap R R q * ⟨z, hz⟩ refine ⟨Ideal.add_mem (I.map (algebraMap R R)) ha.left ?_, by simp only [ha.right, map_add, AlgHom.map_mul, add_right_inj]; rfl⟩ diff --git a/Mathlib/NumberTheory/LegendreSymbol/Basic.lean b/Mathlib/NumberTheory/LegendreSymbol/Basic.lean index 7ba216590aa2a..9ba372670f357 100644 --- a/Mathlib/NumberTheory/LegendreSymbol/Basic.lean +++ b/Mathlib/NumberTheory/LegendreSymbol/Basic.lean @@ -265,7 +265,7 @@ theorem eq_zero_mod_of_eq_neg_one {p : ℕ} [Fact p.Prime] {a : ℤ} (h : legend /-- If `legendreSym p a = -1` and `p` divides `x^2 - a*y^2`, then `p` must divide `x` and `y`. -/ theorem prime_dvd_of_eq_neg_one {p : ℕ} [Fact p.Prime] {a : ℤ} (h : legendreSym p a = -1) {x y : ℤ} - (hxy : (p : ℤ) ∣ x ^ 2 - a * y ^ 2 ) : ↑p ∣ x ∧ ↑p ∣ y := by + (hxy : (p : ℤ) ∣ x ^ 2 - a * y ^ 2) : ↑p ∣ x ∧ ↑p ∣ y := by simp_rw [← ZMod.int_cast_zmod_eq_zero_iff_dvd] at hxy ⊢ push_cast at hxy exact eq_zero_mod_of_eq_neg_one h hxy @@ -311,7 +311,7 @@ theorem mod_four_ne_three_of_sq_eq_neg_sq' {x y : ZMod p} (hy : y ≠ 0) (hxy : @mod_four_ne_three_of_sq_eq_neg_one p _ (x / y) (by apply_fun fun z => z / y ^ 2 at hxy - rwa [neg_div, ← div_pow, ← div_pow, div_self hy, one_pow] at hxy ) + rwa [neg_div, ← div_pow, ← div_pow, div_self hy, one_pow] at hxy) #align zmod.mod_four_ne_three_of_sq_eq_neg_sq' ZMod.mod_four_ne_three_of_sq_eq_neg_sq' theorem mod_four_ne_three_of_sq_eq_neg_sq {x y : ZMod p} (hx : x ≠ 0) (hxy : x ^ 2 = -y ^ 2) : diff --git a/Mathlib/NumberTheory/NumberField/Units.lean b/Mathlib/NumberTheory/NumberField/Units.lean index d47ad0ab22843..7b45bb84cf7d6 100644 --- a/Mathlib/NumberTheory/NumberField/Units.lean +++ b/Mathlib/NumberTheory/NumberField/Units.lean @@ -402,7 +402,7 @@ theorem seq_norm_le (n : ℕ) : /-- Construct a unit associated to the place `w₁`. The family, for `w₁ ≠ w₀`, formed by the image by the `logEmbedding` of these units is `ℝ`-linearly independent, see `unit_lattice_span_eq_top`. -/ -theorem exists_unit (w₁ : InfinitePlace K ) : +theorem exists_unit (w₁ : InfinitePlace K) : ∃ u : (𝓞 K)ˣ, ∀ w : InfinitePlace K, w ≠ w₁ → Real.log (w u) < 0 := by obtain ⟨B, hB⟩ : ∃ B : ℕ, minkowskiBound K < (convexBodyLtFactor K) * B := by simp_rw [mul_comm] diff --git a/Mathlib/RingTheory/AdjoinRoot.lean b/Mathlib/RingTheory/AdjoinRoot.lean index 3bd0dce9bc1a3..6c6dabfca5950 100644 --- a/Mathlib/RingTheory/AdjoinRoot.lean +++ b/Mathlib/RingTheory/AdjoinRoot.lean @@ -852,7 +852,7 @@ noncomputable def quotEquivQuotMap (f : R[X]) (I : Ideal R) : rfl rw [this, quotAdjoinRootEquivQuotPolynomialQuot_mk_of, map_C] -- Porting note: the following `rfl` was not needed - rfl ) + rfl) #align adjoin_root.quot_equiv_quot_map AdjoinRoot.quotEquivQuotMap @[simp] diff --git a/Mathlib/RingTheory/Discriminant.lean b/Mathlib/RingTheory/Discriminant.lean index 821c9a319f8b4..8b97f16c6350a 100644 --- a/Mathlib/RingTheory/Discriminant.lean +++ b/Mathlib/RingTheory/Discriminant.lean @@ -251,7 +251,7 @@ theorem discr_powerBasis_eq_norm [IsSeparable K L] : ← Finset.prod_mk _ (hnodup.erase _)] rw [prod_sigma', prod_sigma'] refine' - prod_bij (fun i _ => ⟨e i.2, e i.1 pb.gen⟩) (fun i hi => _) (fun i _ => by simp ) + prod_bij (fun i _ => ⟨e i.2, e i.1 pb.gen⟩) (fun i hi => _) (fun i _ => by simp) (fun i j hi hj hij => _) fun σ hσ => _ · simp only [true_and_iff, Finset.mem_mk, mem_univ, mem_sigma] rw [Multiset.mem_erase_of_ne fun h => ?_] diff --git a/Mathlib/RingTheory/Henselian.lean b/Mathlib/RingTheory/Henselian.lean index 3c9697135ee6d..87311b18ff64f 100644 --- a/Mathlib/RingTheory/Henselian.lean +++ b/Mathlib/RingTheory/Henselian.lean @@ -122,7 +122,7 @@ theorem HenselianLocalRing.TFAE (R : Type u) [CommRing R] [LocalRing R] : TFAE [HenselianLocalRing R, ∀ (f : R[X]) (_ : f.Monic) (a₀ : ResidueField R) (_ : aeval a₀ f = 0) - (_ : aeval a₀ (derivative f )≠ 0), ∃ a : R, f.IsRoot a ∧ residue R a = a₀, + (_ : aeval a₀ (derivative f) ≠ 0), ∃ a : R, f.IsRoot a ∧ residue R a = a₀, ∀ {K : Type u} [Field K], ∀ (φ : R →+* K) (_ : Surjective φ) (f : R[X]) (_ : f.Monic) (a₀ : K) (_ : f.eval₂ φ a₀ = 0) (_ : f.derivative.eval₂ φ a₀ ≠ 0), diff --git a/Mathlib/RingTheory/Localization/FractionRing.lean b/Mathlib/RingTheory/Localization/FractionRing.lean index fc83734dbd202..fee315b83875a 100644 --- a/Mathlib/RingTheory/Localization/FractionRing.lean +++ b/Mathlib/RingTheory/Localization/FractionRing.lean @@ -324,7 +324,7 @@ theorem isScalarTower_liftAlgebra [IsDomain R] [Field K] [Algebra R K] [NoZeroSM by letI := liftAlgebra R K; exact IsScalarTower R (FractionRing R) K := by letI := liftAlgebra R K exact IsScalarTower.of_algebraMap_eq fun x => - (IsFractionRing.lift_algebraMap (NoZeroSMulDivisors.algebraMap_injective R K ) x).symm + (IsFractionRing.lift_algebraMap (NoZeroSMulDivisors.algebraMap_injective R K) x).symm /-- Given an integral domain `A` and a localization map to a field of fractions `f : A →+* K`, we get an `A`-isomorphism between the field of fractions of `A` as a quotient diff --git a/Mathlib/RingTheory/Nullstellensatz.lean b/Mathlib/RingTheory/Nullstellensatz.lean index e5de8e7ba2209..2c3e04a2f6955 100644 --- a/Mathlib/RingTheory/Nullstellensatz.lean +++ b/Mathlib/RingTheory/Nullstellensatz.lean @@ -124,7 +124,7 @@ instance vanishingIdeal_singleton_isMaximal {x : σ → k} : ⟨(Ideal.Quotient.mk (vanishingIdeal {x} : Ideal (MvPolynomial σ k))) (C z), by simp⟩⟩ obtain ⟨q, rfl⟩ := Quotient.mk_surjective p rwa [Ideal.Quotient.lift_mk, ← mem_vanishingIdeal_singleton_iff, - ← Quotient.eq_zero_iff_mem] at hp ) + ← Quotient.eq_zero_iff_mem] at hp) rw [← bot_quotient_isMaximal_iff, RingEquiv.bot_maximal_iff this] exact bot_isMaximal #align mv_polynomial.vanishing_ideal_singleton_is_maximal MvPolynomial.vanishingIdeal_singleton_isMaximal diff --git a/Mathlib/RingTheory/Perfection.lean b/Mathlib/RingTheory/Perfection.lean index 8f8ea5f76f380..f60d40e3ecdd6 100644 --- a/Mathlib/RingTheory/Perfection.lean +++ b/Mathlib/RingTheory/Perfection.lean @@ -327,7 +327,7 @@ noncomputable def lift [PerfectRing R p] (S : Type u₂) [CommSemiring S] [CharP right_inv f := by exact RingHom.ext fun x => m.equiv.injective <| (m.equiv.apply_symm_apply _).trans <| show Perfection.lift p R S (π.comp f) x = RingHom.comp (↑m.equiv) f x from - RingHom.ext_iff.1 (by rw [Equiv.apply_eq_iff_eq_symm_apply]; rfl ) _ + RingHom.ext_iff.1 (by rw [Equiv.apply_eq_iff_eq_symm_apply]; rfl) _ #align perfection_map.lift PerfectionMap.lift variable {R p} diff --git a/Mathlib/RingTheory/WittVector/Basic.lean b/Mathlib/RingTheory/WittVector/Basic.lean index 967d4430c4fc1..ccd6aed2eeaf9 100644 --- a/Mathlib/RingTheory/WittVector/Basic.lean +++ b/Mathlib/RingTheory/WittVector/Basic.lean @@ -99,7 +99,7 @@ macro "map_fun_tac" : tactic => `(tactic| ( try { cases n <;> simp <;> done } <;> -- porting note: this line solves `one` apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl <;> ext ⟨i, k⟩ <;> - fin_cases i <;> rfl )) + fin_cases i <;> rfl)) -- and until `pow`. -- We do not tag these lemmas as `@[simp]` because they will be bundled in `map` later on. diff --git a/Mathlib/Tactic/ByContra.lean b/Mathlib/Tactic/ByContra.lean index 8e0fe6dc5c3c5..f69d742c79423 100644 --- a/Mathlib/Tactic/ByContra.lean +++ b/Mathlib/Tactic/ByContra.lean @@ -42,4 +42,4 @@ macro_rules -- if the below `exact` call fails then this tactic should fail with the message -- tactic failed: and are not definitionally equal have $e:ident : $y := by { push_neg; exact h }; - clear h ) ) + clear h)) diff --git a/Mathlib/Tactic/NoncommRing.lean b/Mathlib/Tactic/NoncommRing.lean index 4495473685373..2e1e13656783b 100644 --- a/Mathlib/Tactic/NoncommRing.lean +++ b/Mathlib/Tactic/NoncommRing.lean @@ -55,6 +55,6 @@ macro_rules -- Pull out negations. neg_mul, mul_neg] | fail "`noncomm_ring` simp lemmas don't apply; try `abel` instead") <;> - first | abel1 | abel_nf )) + first | abel1 | abel_nf)) end Mathlib.Tactic.NoncommRing diff --git a/Mathlib/Topology/ContinuousFunction/Ideals.lean b/Mathlib/Topology/ContinuousFunction/Ideals.lean index 2d39b99956ba1..e274f54e7cb96 100644 --- a/Mathlib/Topology/ContinuousFunction/Ideals.lean +++ b/Mathlib/Topology/ContinuousFunction/Ideals.lean @@ -293,7 +293,7 @@ theorem idealOfSet_ofIdeal_eq_closure (I : Ideal C(X, 𝕜)) : obtain ⟨g', hI', hgt'⟩ := this obtain ⟨c, hc, hgc'⟩ : ∃ (c : _) (_ : 0 < c), ∀ y : X, y ∈ t → c ≤ g' y := t.eq_empty_or_nonempty.elim - (fun ht' => ⟨1, zero_lt_one, fun y hy => False.elim (by rwa [ht'] at hy )⟩) fun ht' => + (fun ht' => ⟨1, zero_lt_one, fun y hy => False.elim (by rwa [ht'] at hy)⟩) fun ht' => let ⟨x, hx, hx'⟩ := ht.isCompact.exists_forall_le ht' (map_continuous g').continuousOn ⟨g' x, hgt' x hx, hx'⟩ obtain ⟨g, hg, hgc⟩ := exists_mul_le_one_eqOn_ge g' hc diff --git a/test/linarith.lean b/test/linarith.lean index e86e346abefcf..59dc278f9f4f3 100644 --- a/test/linarith.lean +++ b/test/linarith.lean @@ -279,9 +279,9 @@ example (u v x y A B : ℚ) by nlinarith example (u v x y A B : ℚ) : (0 < A) → (A ≤ 1) → (1 ≤ B) -→ (x ≤ B) → ( y ≤ B) +→ (x ≤ B) → (y ≤ B) → (0 ≤ u ) → (0 ≤ v ) -→ (u < A) → ( v < A) +→ (u < A) → (v < A) → (u * y + v * x + u * v < 3 * A * B) := by intros nlinarith