chore: cleanup some spaces (#7484)

Purely cosmetic PR.

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

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⟩ :=

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

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

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
 

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

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
 

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. -/

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

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

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

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
 

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

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. -/

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
 

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,

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]

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

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, _⟩

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

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

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

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]

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`. -/

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

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,21 +211,21 @@ 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'
 #align quotient_add_group.lift_mk' QuotientAddGroup.lift_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

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

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,

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