tracking: #30658 split into pieces

Mathlib/Algebra/AddConstMap/Basic.lean

@@ -42,7 +42,7 @@ structure AddConstMap (G H : Type*) [Add G] [Add H] (a : G) (b : H) where
   map_add_const' (x : G) : toFun (x + a) = toFun x + b
 
 @[inherit_doc]
-scoped [AddConstMap] notation:25 G " →+c[" a ", " b "] " H => AddConstMap G H a b
+scoped[AddConstMap] notation:25 G " →+c[" a ", " b "] " H => AddConstMap G H a b
 
 /-- Typeclass for maps satisfying `f (x + a) = f x + b`.
 
@@ -63,7 +63,7 @@ namespace AddConstMapClass
 In this section we prove properties like `f (x + n • a) = f x + n • b`.
 -/
 
-scoped [AddConstMapClass] attribute [simp] map_add_const
+scoped[AddConstMapClass] attribute [simp] map_add_const
 
 variable {F G H : Type*} [FunLike F G H] {a : G} {b : H}
 

Mathlib/Algebra/Algebra/Spectrum/Quasispectrum.lean

@@ -567,7 +567,7 @@ theorem of_subset_range_algebraMap (hf : f.LeftInverse (algebraMap R S))
 
 lemma of_spectrum_eq {a b : A} {f : S → R} (ha : SpectrumRestricts a f)
     (h : spectrum S a = spectrum S b) : SpectrumRestricts b f where
-  rightInvOn :=  by
+  rightInvOn := by
     rw [quasispectrum_eq_spectrum_union_zero, ← h, ← quasispectrum_eq_spectrum_union_zero]
     exact QuasispectrumRestricts.rightInvOn ha
   left_inv := ha.left_inv

Mathlib/Algebra/BrauerGroup/Defs.lean

@@ -70,10 +70,10 @@ lemma trans {A B C : CSA K} (hAB : IsBrauerEquivalent A B) (hBC : IsBrauerEquiva
   obtain ⟨n, m, hn, hm, ⟨iso1⟩⟩ := hAB
   obtain ⟨p, q, hp, hq, ⟨iso2⟩⟩ := hBC
   exact ⟨p * n, m * q, by simp_all, by simp_all,
-    ⟨reindexAlgEquiv _ _ finProdFinEquiv |>.symm.trans <| compAlgEquiv _ _ _ _|>.symm.trans <|
-    iso1.mapMatrix (m := Fin p)|>.trans <| compAlgEquiv _ _ _ _|>.trans <|
-    reindexAlgEquiv K B (.prodComm (Fin p) (Fin m))|>.trans <| compAlgEquiv _ _ _ _|>.symm.trans <|
-    iso2.mapMatrix.trans <| compAlgEquiv _ _ _ _|>.trans <| reindexAlgEquiv _ _ finProdFinEquiv⟩⟩
+    ⟨reindexAlgEquiv _ _ finProdFinEquiv |>.symm.trans <| compAlgEquiv _ _ _ _ |>.symm.trans <|
+    iso1.mapMatrix (m := Fin p)|>.trans <| compAlgEquiv _ _ _ _ |>.trans <|
+    reindexAlgEquiv K B (.prodComm (Fin p) (Fin m))|>.trans <| compAlgEquiv _ _ _ _ |>.symm.trans <|
+    iso2.mapMatrix.trans <| compAlgEquiv _ _ _ _ |>.trans <| reindexAlgEquiv _ _ finProdFinEquiv⟩⟩
 
 lemma is_eqv : Equivalence (IsBrauerEquivalent (K := K)) where
   refl := refl

Mathlib/Algebra/Category/Ring/Basic.lean

@@ -134,6 +134,7 @@ lemma hom_inv_apply {R S : SemiRingCat} (e : R ≅ S) (s : S) : e.hom (e.inv s)
 instance : Inhabited SemiRingCat :=
   ⟨of PUnit⟩
 
+set_option linter.style.commandStart false in -- TODO fix linter/pretty-printing!
 /-- This unification hint helps with problems of the form `(forget ?C).obj R =?= carrier R'`. -/
 unif_hint forget_obj_eq_coe (R R' : SemiRingCat) where
   R ≟ R' ⊢
@@ -284,6 +285,7 @@ lemma hom_inv_apply {R S : RingCat} (e : R ≅ S) (s : S) : e.hom (e.inv s) = s
 instance : Inhabited RingCat :=
   ⟨of PUnit⟩
 
+set_option linter.style.commandStart false in -- TODO investigate and fix!
 /-- This unification hint helps with problems of the form `(forget ?C).obj R =?= carrier R'`.
 
 An example where this is needed is in applying
@@ -447,6 +449,7 @@ lemma hom_inv_apply {R S : CommSemiRingCat} (e : R ≅ S) (s : S) : e.hom (e.inv
 instance : Inhabited CommSemiRingCat :=
   ⟨of PUnit⟩
 
+set_option linter.style.commandStart false in -- TODO investigate and fix!
 /-- This unification hint helps with problems of the form `(forget ?C).obj R =?= carrier R'`. -/
 unif_hint forget_obj_eq_coe (R R' : CommSemiRingCat) where
   R ≟ R' ⊢
@@ -609,6 +612,7 @@ instance : Inhabited CommRingCat :=
 
 lemma forget_obj {R : CommRingCat} : (forget CommRingCat).obj R = R := rfl
 
+set_option linter.style.commandStart false in -- TODO fix linter/pretty-printing!
 /-- This unification hint helps with problems of the form `(forget ?C).obj R =?= carrier R'`.
 
 An example where this is needed is in applying `TopCat.Presheaf.restrictOpen` to commutative rings.

Mathlib/Algebra/GroupWithZero/Range.lean

@@ -167,7 +167,7 @@ theorem mem_valueGroup_iff_of_comm {y : Bˣ} :
       obtain ⟨v, hv, b, hb⟩ := hdy
       refine ⟨u * v, by simp [hu, hv], a * b, ?_⟩
       simpa [map_mul, Units.val_mul, ← hb, ← ha] using mul_mul_mul_comm ..
-    | inv c hc hcy  =>
+    | inv c hc hcy =>
       obtain ⟨u, hu, a, ha⟩ := hcy
       exact ⟨a, by simp [← ha, hu], u, by simp [← ha]⟩
   · have hv : f x ≠ 0 := by

Mathlib/Algebra/IsPrimePow.lean

@@ -69,6 +69,7 @@ theorem isPrimePow_nat_iff (n : ℕ) : IsPrimePow n ↔ ∃ p k : ℕ, Nat.Prime
 theorem Nat.Prime.isPrimePow {p : ℕ} (hp : p.Prime) : IsPrimePow p :=
   _root_.Prime.isPrimePow (prime_iff.mp hp)
 
+set_option linter.style.commandStart false in -- TODO decide about this!
 theorem isPrimePow_nat_iff_bounded (n : ℕ) :
     IsPrimePow n ↔ ∃ p : ℕ, p ≤ n ∧ ∃ k : ℕ, k ≤ n ∧ p.Prime ∧ 0 < k ∧ p ^ k = n := by
   rw [isPrimePow_nat_iff]

Mathlib/Algebra/MonoidAlgebra/ToDirectSum.lean

@@ -271,7 +271,7 @@ theorem AddMonoidAlgebra.toDirectSum_pow [DecidableEq ι] [AddMonoid ι] [Semiri
 @[simp]
 theorem DirectSum.toAddMonoidAlgebra_pow [DecidableEq ι] [AddMonoid ι] [Semiring M]
     [∀ m : M, Decidable (m ≠ 0)] (f : ⨁ _ : ι, M) (n : ℕ):
-    (f ^ n).toAddMonoidAlgebra = toAddMonoidAlgebra f ^ n :=  by
+    (f ^ n).toAddMonoidAlgebra = toAddMonoidAlgebra f ^ n := by
   classical exact map_pow addMonoidAlgebraRingEquivDirectSum.symm f n
 
 end Equivs

Mathlib/Algebra/NoZeroSMulDivisors/Basic.lean

@@ -70,6 +70,7 @@ section SMulInjective
 variable (R)
 variable [NoZeroSMulDivisors R M]
 
+set_option linter.style.commandStart false in -- TODO decide about this!
 theorem smul_left_injective {x : M} (hx : x ≠ 0) : Function.Injective fun c : R => c • x :=
   fun c d h =>
   sub_eq_zero.mp

Mathlib/Algebra/Order/CauSeq/Basic.lean

@@ -208,6 +208,7 @@ variable (abv) in
 /-- The constant Cauchy sequence. -/
 def const (x : β) : CauSeq β abv := ⟨fun _ ↦ x, IsCauSeq.const _⟩
 
+set_option linter.style.commandStart false in -- TODO fix the linter!
 /-- The constant Cauchy sequence -/
 local notation "const" => const abv
 

Mathlib/Algebra/Order/Module/Defs.lean

@@ -536,7 +536,7 @@ lemma smul_pos_iff_of_pos_left [PosSMulStrictMono α β] [PosSMulReflectLT α β
 
 lemma smul_neg_iff_of_pos_left [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) :
     a • b < 0 ↔ b < 0 := by
-  simpa only [smul_zero]  using smul_lt_smul_iff_of_pos_left ha (b₂ := (0 : β))
+  simpa only [smul_zero] using smul_lt_smul_iff_of_pos_left ha (b₂ := (0 : β))
 
 lemma smul_nonneg [PosSMulMono α β] (ha : 0 ≤ a) (hb : 0 ≤ b₁) : 0 ≤ a • b₁ := by
   simpa only [smul_zero] using smul_le_smul_of_nonneg_left hb ha

Mathlib/Algebra/Polynomial/AlgebraMap.lean

@@ -322,7 +322,7 @@ def algEquivCMulXAddC {R : Type*} [CommRing R] (a b : R) [Invertible a] : R[X] 
     (by simp [← C_mul, ← mul_assoc]) (by simp [← C_mul, ← mul_assoc])
 
 theorem algEquivCMulXAddC_symm_eq {R : Type*} [CommRing R] (a b : R) [Invertible a] :
-    (algEquivCMulXAddC a b).symm =  algEquivCMulXAddC (⅟a) (- ⅟a * b) := by
+    (algEquivCMulXAddC a b).symm = algEquivCMulXAddC (⅟a) (- ⅟a * b) := by
   ext p : 1
   simp only [algEquivCMulXAddC_symm_apply, neg_mul, algEquivCMulXAddC_apply, map_neg, map_mul]
   congr

Mathlib/Algebra/Ring/BooleanRing.lean

@@ -160,8 +160,8 @@ def sup : Max α :=
 def inf : Min α :=
   ⟨(· * ·)⟩
 
-scoped [BooleanAlgebraOfBooleanRing] attribute [instance 100] BooleanRing.sup
-scoped [BooleanAlgebraOfBooleanRing] attribute [instance 100] BooleanRing.inf
+scoped[BooleanAlgebraOfBooleanRing] attribute [instance 100] BooleanRing.sup
+scoped[BooleanAlgebraOfBooleanRing] attribute [instance 100] BooleanRing.inf
 open BooleanAlgebraOfBooleanRing
 
 theorem sup_comm (a b : α) : a ⊔ b = b ⊔ a := by

Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean

@@ -708,7 +708,7 @@ def liftNCRingHom (f : k →+* R) (g : G →* R) (h_comm : ∀ {x y}, (f (y •
     SkewMonoidAlgebra k G →+* R where
   __ := liftNC (f : k →+ R) g
   map_one' := liftNC_one _ _
-  map_mul' _ _ :=  liftNC_mul _ _ _ _ fun {_ _} _ ↦ h_comm
+  map_mul' _ _ := liftNC_mul _ _ _ _ fun {_ _} _ ↦ h_comm
 
 end Semiring
 

Mathlib/AlgebraicGeometry/AffineSpace.lean

@@ -45,7 +45,7 @@ def AffineSpace (n : Type v) (S : Scheme.{max u v}) : Scheme.{max u v} :=
 namespace AffineSpace
 
 /-- `𝔸(n; S)` is the affine `n`-space over `S`. -/
-scoped [AlgebraicGeometry] notation "𝔸("n"; "S")" => AffineSpace n S
+scoped[AlgebraicGeometry] notation "𝔸("n"; "S")" => AffineSpace n S
 
 variable {n} in
 lemma of_mvPolynomial_int_ext {R} {f g : ℤ[n] ⟶ R} (h : ∀ i, f (.X i) = g (.X i)) : f = g := by

Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean

@@ -105,7 +105,7 @@ theorem hη :
         (N₁Γ₀ : Γ ⋙ N₁ ≅ (toKaroubiEquivalence (ChainComplex C ℕ)).functor) := by
   ext K : 3
   simp only [Compatibility.τ₀_hom_app, Compatibility.τ₁_hom_app]
-  exact (N₂Γ₂_compatible_with_N₁Γ₀ K).trans (by simp )
+  exact (N₂Γ₂_compatible_with_N₁Γ₀ K).trans (by simp)
 
 /-- The counit isomorphism induced by `N₁Γ₀` -/
 @[simps!]

Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean

@@ -143,7 +143,7 @@ private lemma factor_P_δ_σ {n : ℕ} (i : Fin (n + 1)) {x : SimplexCategoryGen
   induction n generalizing x with
   | zero => cases hf with
     | of _ h => cases h; exact factor_δ_σ _ _
-    | id  => exact ⟨_, _, _, P_σ.σ i, P_δ.id_mem _, by simp⟩
+    | id => exact ⟨_, _, _, P_σ.σ i, P_δ.id_mem _, by simp⟩
     | comp_of j f hf hg =>
       obtain ⟨k⟩ := hg
       obtain ⟨rfl, rfl⟩ | hf' := eq_or_len_le_of_P_δ hf

Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean

@@ -115,7 +115,7 @@ lemma yonedaEquiv_map {n m : SimplexCategory} (f : n ⟶ m) :
 
 /-- The (degenerate) `m`-simplex in the standard simplex concentrated in vertex `k`. -/
 def const (n : ℕ) (k : Fin (n + 1)) (m : SimplexCategoryᵒᵖ) : Δ[n].obj m :=
-  objMk (OrderHom.const _ k )
+  objMk (OrderHom.const _ k)
 
 @[simp]
 lemma const_down_toOrderHom (n : ℕ) (k : Fin (n + 1)) (m : SimplexCategoryᵒᵖ) :

Mathlib/Analysis/BoxIntegral/UnitPartition.lean

@@ -74,7 +74,7 @@ theorem BoxIntegral.le_hasIntegralVertices_of_isBounded [Finite ι] {s : Set (ι
   obtain ⟨R, hR₁, hR₂⟩ := IsBounded.subset_ball_lt h 0 0
   let C : ℕ := ⌈R⌉₊
   have hC := Nat.ceil_pos.mpr hR₁
-  let I : Box ι := Box.mk (fun _ ↦ - C) (fun _ ↦ C )
+  let I : Box ι := Box.mk (fun _ ↦ - C) (fun _ ↦ C)
     (fun _ ↦ by simp [C, neg_lt_self_iff, Nat.cast_pos, hC])
   refine ⟨I, ⟨fun _ ↦ - C, fun _ ↦ C, fun i ↦ (Int.cast_neg_natCast C).symm, fun _ ↦ rfl⟩,
     le_trans hR₂ ?_⟩

Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean

@@ -105,9 +105,9 @@ noncomputable section
 open ENat NNReal Topology Filter Set Fin Filter Function
 
 /-- Smoothness exponent for analytic functions. -/
-scoped [ContDiff] notation3 "ω" => (⊤ : WithTop ℕ∞)
+scoped[ContDiff] notation3 "ω" => (⊤ : WithTop ℕ∞)
 /-- Smoothness exponent for infinitely differentiable functions. -/
-scoped [ContDiff] notation3 "∞" => ((⊤ : ℕ∞) : WithTop ℕ∞)
+scoped[ContDiff] notation3 "∞" => ((⊤ : ℕ∞) : WithTop ℕ∞)
 
 open scoped ContDiff Pointwise
 

Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean

@@ -811,7 +811,7 @@ def compAlongOrderedFinpartitionₗ :
         ext v
         simp [applyOrderedFinpartition_update_left])
   map_add' _ _ := rfl
-  map_smul' _ _ :=  rfl
+  map_smul' _ _ := rfl
 
 variable (𝕜 E F G) in
 /-- Bundled version of `compAlongOrderedFinpartition`, depending continuously linearly on `f`

Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean

@@ -120,7 +120,7 @@ theorem ModularGroup_T_zpow_mem_verticalStrip (z : ℍ) {N : ℕ} (hn : 0 < N) :
   rw [h, add_comm]
   simp only [neg_mul, Int.cast_neg, Int.cast_mul, Int.cast_natCast]
   have hnn : (0 : ℝ) < (N : ℝ) := by norm_cast at *
-  have h2 : z.re + -(N * n) =  z.re - n * N := by ring
+  have h2 : z.re + -(N * n) = z.re - n * N := by ring
   rw [h2, abs_eq_self.2 (Int.sub_floor_div_mul_nonneg (z.re : ℝ) hnn)]
   apply (Int.sub_floor_div_mul_lt (z.re : ℝ) hnn).le
 

Mathlib/Analysis/Normed/Unbundled/SmoothingSeminorm.lean

@@ -476,7 +476,7 @@ theorem isNonarchimedean_smoothingFun (hμ1 : μ 1 ≤ 1) (hna : IsNonarchimedea
   intro ε hε
   rw [sub_le_iff_le_add]
   have h_mul : smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤
-      max (smoothingFun μ x) (smoothingFun μ y) + ε :=  by
+      max (smoothingFun μ x) (smoothingFun μ y) + ε := by
     rw [max_def]
     split_ifs with h
     · rw [add_le_add_iff_right]

Mathlib/CategoryTheory/Abelian/Projective/Resolution.lean

@@ -147,7 +147,7 @@ lemma liftHomotopyZeroSucc_comp {Y Z : C} {P : ProjectiveResolution Y} {Q : Proj
 /-- Any lift of the zero morphism is homotopic to zero. -/
 def liftHomotopyZero {Y Z : C} {P : ProjectiveResolution Y} {Q : ProjectiveResolution Z}
     (f : P.complex ⟶ Q.complex) (comm : f ≫ Q.π = 0) : Homotopy f 0 :=
-  Homotopy.mkInductive _ (liftHomotopyZeroZero f comm) (by simp )
+  Homotopy.mkInductive _ (liftHomotopyZeroZero f comm) (by simp)
     (liftHomotopyZeroOne f comm) (by simp) fun n ⟨g, g', w⟩ =>
     ⟨liftHomotopyZeroSucc f n g g' w, by simp⟩
 

Mathlib/CategoryTheory/Bicategory/Adjunction/Mate.lean

@@ -682,7 +682,7 @@ theorem mateEquiv_conjugateEquiv_vcomp
     _ = 𝟙 _ ⊗≫
           rightAdjointSquare.vcomp
             (mateEquiv adj₁ adj₂ α)
-            (mateEquiv adj₂ adj₃ ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)) ⊗≫ 𝟙 _  := by
+            (mateEquiv adj₂ adj₃ ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)) ⊗≫ 𝟙 _ := by
       dsimp only [conjugateEquiv_apply, rightAdjointSquareConjugate.vcomp,
         rightAdjointSquare.vcomp]
       bicategory

Mathlib/CategoryTheory/Bicategory/EqToHom.lean

@@ -110,7 +110,7 @@ lemma whiskerRight_congr {y z : B} {g g' : y ⟶ z} (h : g = g') {x : B}
   simp
 
 lemma leftUnitor_hom_congr {x y : B} {f f' : x ⟶ y} (h : f = f') :
-    (λ_ f).hom = 𝟙 _ ◁ (eqToHom h)  ≫ (λ_ f').hom ≫ eqToHom h.symm := by
+    (λ_ f).hom = 𝟙 _ ◁ (eqToHom h) ≫ (λ_ f').hom ≫ eqToHom h.symm := by
   subst h
   simp
 
@@ -120,7 +120,7 @@ lemma leftUnitor_inv_congr {x y : B} {f f' : x ⟶ y} (h : f = f') :
   simp
 
 lemma rightUnitor_hom_congr {x y : B} {f f' : x ⟶ y} (h : f = f') :
-    (ρ_ f).hom = (eqToHom h) ▷ 𝟙 _  ≫ (ρ_ f').hom ≫ eqToHom h.symm := by
+    (ρ_ f).hom = (eqToHom h) ▷ 𝟙 _ ≫ (ρ_ f').hom ≫ eqToHom h.symm := by
   subst h
   simp
 

Mathlib/CategoryTheory/Category/Cat/Adjunction.lean

@@ -47,7 +47,7 @@ def typeToCatObjectsAdj : typeToCat ⊣ Cat.objects :=
       naturality := fun _ _ _  ↦  Functor.hext (fun _ ↦ rfl)
         (by intro ⟨_⟩ ⟨_⟩ f
             obtain rfl := Discrete.eq_of_hom f
-            cat_disch ) } }
+            cat_disch) } }
 
 /-- The connected components functor -/
 def connectedComponents : Cat.{v, u} ⥤ Type u where

Mathlib/CategoryTheory/Category/Cat/Terminal.lean

@@ -34,7 +34,7 @@ def isTerminalOfUniqueOfIsDiscrete {T : Type u} [Category.{v} T] [Unique T] [IsD
 
 instance : HasTerminal Cat.{v, u} := by
   have : IsDiscrete (ShrinkHoms.{u} PUnit.{u + 1}) := {
-    subsingleton _ _ := { allEq _ _ :=  eq_of_comp_right_eq (congrFun rfl) }
+    subsingleton _ _ := { allEq _ _ := eq_of_comp_right_eq (congrFun rfl) }
     eq_of_hom _ := rfl
   }
   exact IsTerminal.hasTerminal (X := Cat.of (ShrinkHoms PUnit)) isTerminalOfUniqueOfIsDiscrete

Mathlib/CategoryTheory/Closed/Ideal.lean

@@ -133,7 +133,7 @@ abbrev CartesianMonoidalCategory.ofReflective [CartesianMonoidalCategory C] [Ref
         ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫ (reflectorAdjunction i).counit.app _)
       isLimit := by
         apply isLimitOfReflects i
-        apply IsLimit.equivOfNatIsoOfIso (pairComp X Y _) _ _ _|>.invFun
+        apply IsLimit.equivOfNatIsoOfIso (pairComp X Y _) _ _ _ |>.invFun
           (tensorProductIsBinaryProduct (i.obj X) (i.obj Y))
         fapply BinaryFan.ext
         · change (reflector i ⋙ i).obj (i.obj X ⊗ i.obj Y) ≅ (𝟭 C).obj (i.obj X ⊗ i.obj Y)
@@ -142,7 +142,7 @@ abbrev CartesianMonoidalCategory.ofReflective [CartesianMonoidalCategory C] [Ref
             haveI := reflective_products i
             use Limits.prod X Y
             constructor
-            apply Limits.PreservesLimitPair.iso i _ _|>.trans
+            apply Limits.PreservesLimitPair.iso i _ _ |>.trans
             refine Limits.IsLimit.conePointUniqueUpToIso (limit.isLimit (pair (i.obj X) (i.obj Y)))
               (tensorProductIsBinaryProduct _ _)
           exact asIso ((reflectorAdjunction i).unit.app (i.obj X ⊗ i.obj Y))|>.symm

Mathlib/CategoryTheory/Core.lean

@@ -122,7 +122,7 @@ variable {D : Type u₂} [Category.{v₂} D]
 @[simps!]
 def core {F G : C ⥤ D} (α : F ≅ G) : F.core ≅ G.core :=
   NatIso.ofComponents
-    (fun x ↦ Groupoid.isoEquivHom _ _|>.symm <| .mk <| α.app x.of)
+    (fun x ↦ Groupoid.isoEquivHom _ _ |>.symm <| .mk <| α.app x.of)
 
 @[simp]
 lemma coreComp {F G H : C ⥤ D} (α : F ≅ G) (β : G ≅ H) : (α ≪≫ β).core = α.core ≪≫ β.core := rfl
@@ -136,7 +136,7 @@ lemma coreWhiskerLeft {E : Type u₃} [Category.{v₃} E] (F : C ⥤ D) {G H : D
   cat_disch
 
 lemma coreWhiskerRight {E : Type u₃} [Category.{v₃} E] {F G : C ⥤ D} (η : F ≅ G) (H : D ⥤ E) :
-    (isoWhiskerRight η H ).core =
+    (isoWhiskerRight η H).core =
     F.coreComp H ≪≫ isoWhiskerRight η.core H.core ≪≫ (G.coreComp H).symm := by
   cat_disch
 

Mathlib/CategoryTheory/Enriched/FunctorCategory.lean

@@ -258,7 +258,7 @@ noncomputable abbrev precompEnrichedHom' {F₁' F₂' : K ⥤ C}
       rw [enrichedHom_condition_assoc, eHom_whisker_exchange,
         eHom_whisker_exchange, ← eHomWhiskerRight_comp_assoc,
         ← eHomWhiskerRight_comp_assoc, NatTrans.naturality]
-      dsimp )
+      dsimp)
 
 /-- If `F₁` and `F₂` are functors `J ⥤ C`, and `G : K ⥤ J`,
 then this is the induced morphism

Mathlib/CategoryTheory/EqToHom.lean

@@ -362,7 +362,7 @@ def Equivalence.induced {T : Type*} (e : T ≃ D) :
   unitIso := NatIso.ofComponents (fun _ ↦ eqToIso (by simp)) (fun {X Y} f ↦ by
     dsimp
     erw [eqToHom_trans_assoc _ (by simp), eqToHom_refl, Category.id_comp]
-    rfl )
+    rfl)
   counitIso := NatIso.ofComponents (fun _ ↦ eqToIso (by simp))
   functor_unitIso_comp X := eqToHom_trans (by simp) (by simp)
 

Mathlib/CategoryTheory/FiberedCategory/Cartesian.lean

@@ -352,7 +352,7 @@ lemma isIso_of_base_isIso (φ : a ⟶ b) [IsStronglyCartesian p f φ] [IsIso f]
   have inv_hom : φ' ≫ φ = 𝟙 b := fac p (p.map φ) φ _ (𝟙 b)
   refine ⟨?_, inv_hom⟩
   -- We will now show that `φ ≫ φ' = 𝟙 a` by showing that `(φ ≫ φ') ≫ φ = 𝟙 a ≫ φ`.
-  have h₁ : IsHomLift p (𝟙 (p.obj a)) (φ  ≫ φ') := by
+  have h₁ : IsHomLift p (𝟙 (p.obj a)) (φ ≫ φ') := by
     rw [← IsIso.hom_inv_id (p.map φ)]
     apply IsHomLift.comp
   apply IsStronglyCartesian.ext p (p.map φ) φ (𝟙 (p.obj a))

Mathlib/CategoryTheory/FiberedCategory/HomLift.lean

@@ -142,7 +142,7 @@ instance comp_lift_id_left {a b c : 𝒳} {S T : 𝒮} (f : S ⟶ T) (ψ : b ⟶
     (φ : a ⟶ b) [p.IsHomLift (𝟙 S) φ] : p.IsHomLift f (φ ≫ ψ) := by
   simpa using inferInstanceAs (p.IsHomLift (𝟙 S ≫ f) (φ ≫ ψ))
 
-/-- If `φ : a ⟶ b` lifts `𝟙 T` and `ψ : b ⟶ c` lifts `f`, then `φ  ≫ ψ` lifts `f` -/
+/-- If `φ : a ⟶ b` lifts `𝟙 T` and `ψ : b ⟶ c` lifts `f`, then `φ ≫ ψ` lifts `f` -/
 lemma comp_lift_id_left' {a b c : 𝒳} (R : 𝒮) (φ : a ⟶ b) [p.IsHomLift (𝟙 R) φ]
     {S T : 𝒮} (f : S ⟶ T) (ψ : b ⟶ c) [p.IsHomLift f ψ] : p.IsHomLift f (φ ≫ ψ) := by
   obtain rfl : R = S := by rw [← codomain_eq p (𝟙 R) φ, domain_eq p f ψ]