chore: exactly 4 spaces in subsequent lines for def (#7321)

Co-authored-by: Moritz Firsching <firsching@google.com>

Author: mo271

Mathlib/Algebra/Category/MonCat/Basic.lean

@@ -370,7 +370,7 @@ end CategoryTheory.Iso
 in `MonCat` -/
 @[to_additive addEquivIsoAddMonCatIso]
 def mulEquivIsoMonCatIso {X Y : Type u} [Monoid X] [Monoid Y] :
-  X ≃* Y ≅ MonCat.of X ≅ MonCat.of Y where
+    X ≃* Y ≅ MonCat.of X ≅ MonCat.of Y where
   hom e := e.toMonCatIso
   inv i := i.monCatIsoToMulEquiv
 set_option linter.uppercaseLean3 false in

Mathlib/Algebra/Hom/Equiv/Basic.lean

@@ -622,7 +622,7 @@ where the equivalence between the targets is multiplicative.
 @[to_additive (attr := simps apply) "An additive analogue of `Equiv.arrowCongr`,
   where the equivalence between the targets is additive."]
 def arrowCongr {M N P Q : Type*} [Mul P] [Mul Q] (f : M ≃ N) (g : P ≃* Q) :
-  (M → P) ≃* (N → Q) where
+    (M → P) ≃* (N → Q) where
   toFun h n := g (h (f.symm n))
   invFun k m := g.symm (k (f m))
   left_inv h := by ext; simp

Mathlib/Algebra/Hom/Group/Defs.lean

@@ -814,7 +814,7 @@ equalities. -/
   "Copy of a `ZeroHom` with a new `toFun` equal to the old one. Useful to fix
   definitional equalities."]
 protected def OneHom.copy [One M] [One N] (f : OneHom M N) (f' : M → N) (h : f' = f) :
-  OneHom M N where
+    OneHom M N where
   toFun := f'
   map_one' := h.symm ▸ f.map_one'
 #align one_hom.copy OneHom.copy
@@ -840,7 +840,7 @@ equalities. -/
   "Copy of an `AddHom` with a new `toFun` equal to the old one. Useful to fix
   definitional equalities."]
 protected def MulHom.copy [Mul M] [Mul N] (f : M →ₙ* N) (f' : M → N) (h : f' = f) :
-  M →ₙ* N where
+    M →ₙ* N where
   toFun := f'
   map_mul' := h.symm ▸ f.map_mul'
 #align mul_hom.copy MulHom.copy
@@ -1045,7 +1045,7 @@ def MulHom.comp [Mul M] [Mul N] [Mul P] (hnp : N →ₙ* P) (hmn : M →ₙ* N)
 /-- Composition of monoid morphisms as a monoid morphism. -/
 @[to_additive]
 def MonoidHom.comp [MulOneClass M] [MulOneClass N] [MulOneClass P] (hnp : N →* P) (hmn : M →* N) :
-  M →* P where
+    M →* P where
   toFun := hnp ∘ hmn
   map_one' := by simp
   map_mul' := by simp

Mathlib/Algebra/Homology/HomologicalComplex.lean

@@ -93,8 +93,8 @@ theorem ext {C₁ C₂ : HomologicalComplex V c} (h_X : C₁.X = C₂.X)
 #align homological_complex.ext HomologicalComplex.ext
 
 /-- The obvious isomorphism `K.X p ≅ K.X q` when `p = q`. -/
-def XIsoOfEq (K : HomologicalComplex V c) {p q : ι} (h : p = q) :
-  K.X p ≅ K.X q := eqToIso (by rw [h])
+def XIsoOfEq (K : HomologicalComplex V c) {p q : ι} (h : p = q) : K.X p ≅ K.X q :=
+  eqToIso (by rw [h])
 
 @[simp]
 lemma XIsoOfEq_rfl (K : HomologicalComplex V c) (p : ι) :

Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean

@@ -81,7 +81,7 @@ def mk (v : ∀ (p q : ℤ) (_ : p + n = q), F.X p ⟶ G.X q) : Cochain F G n :=
 /-- The value of a cochain on a triplet `⟨p, q, hpq⟩`. -/
 @[pp_dot]
 def v (γ : Cochain F G n) (p q : ℤ) (hpq : p + n = q) :
-  F.X p ⟶ G.X q := γ ⟨p, q, hpq⟩
+    F.X p ⟶ G.X q := γ ⟨p, q, hpq⟩
 
 @[simp]
 lemma mk_v (v : ∀ (p q : ℤ) (_ : p + n = q), F.X p ⟶ G.X q) (p q : ℤ) (hpq : p + n = q) :

Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean

@@ -144,7 +144,7 @@ variable (S)
 by any limit kernel fork of `S.g` -/
 @[simps]
 def ofIsLimitKernelFork (hf : S.f = 0) (c : KernelFork S.g) (hc : IsLimit c) :
-  S.RightHomologyData where
+    S.RightHomologyData where
   Q := S.X₂
   H := c.pt
   p := 𝟙 _
@@ -169,7 +169,7 @@ ofIsLimitKernelFork S hf _ (kernelIsKernel _)
 by any colimit cokernel cofork of `S.g` -/
 @[simps]
 def ofIsColimitCokernelCofork (hg : S.g = 0) (c : CokernelCofork S.f) (hc : IsColimit c) :
-  S.RightHomologyData where
+    S.RightHomologyData where
   Q := c.pt
   H := c.pt
   p := c.π
@@ -363,7 +363,7 @@ attribute [nolint simpNF] mk.injEq
 /-- The right homology map data associated to the zero morphism between two short complexes. -/
 @[simps]
 def zero (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
-  RightHomologyMapData 0 h₁ h₂ where
+    RightHomologyMapData 0 h₁ h₂ where
   φQ := 0
   φH := 0
 
@@ -410,7 +410,7 @@ lemma congr_φQ {γ₁ γ₂ : RightHomologyMapData φ h₁ h₂} (eq : γ₁ =
 morphism `φ : S₁ ⟶ S₂` is given by the action `φ.τ₂` on the middle objects. -/
 @[simps]
 def ofZeros (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) (hg₂ : S₂.g = 0) :
-  RightHomologyMapData φ (RightHomologyData.ofZeros S₁ hf₁ hg₁)
+    RightHomologyMapData φ (RightHomologyData.ofZeros S₁ hf₁ hg₁)
     (RightHomologyData.ofZeros S₂ hf₂ hg₂) where
   φQ := φ.τ₂
   φH := φ.τ₂

Mathlib/Algebra/Ring/Equiv.lean

@@ -120,8 +120,8 @@ instance (priority := 100) toNonUnitalRingHomClass [NonUnitalNonAssocSemiring R]
 `RingEquiv`. This is declared as the default coercion from `F` to `α ≃+* β`. -/
 @[coe]
 def toRingEquiv [Mul α] [Add α] [Mul β] [Add β] [RingEquivClass F α β] (f : F) :
-  α ≃+* β :=
-{ (f : α ≃* β), (f : α ≃+ β) with }
+    α ≃+* β :=
+  { (f : α ≃* β), (f : α ≃+ β) with }
 
 end RingEquivClass
 

Mathlib/Algebra/Ring/Opposite.lean

@@ -198,7 +198,7 @@ def NonUnitalRingHom.fromOpposite {R S : Type*} [NonUnitalNonAssocSemiring R]
 `αᵐᵒᵖ →+* βᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/
 @[simps]
 def NonUnitalRingHom.op {α β} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] :
-  (α →ₙ+* β) ≃ (αᵐᵒᵖ →ₙ+* βᵐᵒᵖ) where
+    (α →ₙ+* β) ≃ (αᵐᵒᵖ →ₙ+* βᵐᵒᵖ) where
   toFun f := { AddMonoidHom.mulOp f.toAddMonoidHom, MulHom.op f.toMulHom with }
   invFun f := { AddMonoidHom.mulUnop f.toAddMonoidHom, MulHom.unop f.toMulHom with }
   left_inv _ := rfl

Mathlib/CategoryTheory/Adjunction/Limits.lean

@@ -67,8 +67,8 @@ Auxiliary definition for `functorialityIsLeftAdjoint`.
 -/
 @[simps]
 def functorialityUnit :
-  𝟭 (Cocone K) ⟶ Cocones.functoriality _ F ⋙ functorialityRightAdjoint adj K where
-    app c := { hom := adj.unit.app c.pt }
+    𝟭 (Cocone K) ⟶ Cocones.functoriality _ F ⋙ functorialityRightAdjoint adj K where
+  app c := { hom := adj.unit.app c.pt }
 #align category_theory.adjunction.functoriality_unit CategoryTheory.Adjunction.functorialityUnit
 
 /-- The counit for the adjunction for `Cocones.functoriality K F : Cocone K ⥤ Cocone (K ⋙ F)`.
@@ -77,8 +77,8 @@ Auxiliary definition for `functorialityIsLeftAdjoint`.
 -/
 @[simps]
 def functorialityCounit :
-  functorialityRightAdjoint adj K ⋙ Cocones.functoriality _ F ⟶ 𝟭 (Cocone (K ⋙ F)) where
-    app c := { hom := adj.counit.app c.pt }
+    functorialityRightAdjoint adj K ⋙ Cocones.functoriality _ F ⟶ 𝟭 (Cocone (K ⋙ F)) where
+  app c := { hom := adj.counit.app c.pt }
 #align category_theory.adjunction.functoriality_counit CategoryTheory.Adjunction.functorialityCounit
 
 /-- The functor `Cocones.functoriality K F : Cocone K ⥤ Cocone (K ⋙ F)` is a left adjoint. -/
@@ -181,8 +181,8 @@ Auxiliary definition for `functorialityIsRightAdjoint`.
 -/
 @[simps]
 def functorialityUnit' :
-  𝟭 (Cone (K ⋙ G)) ⟶ functorialityLeftAdjoint adj K ⋙ Cones.functoriality _ G where
-    app c := { hom := adj.unit.app c.pt }
+    𝟭 (Cone (K ⋙ G)) ⟶ functorialityLeftAdjoint adj K ⋙ Cones.functoriality _ G where
+  app c := { hom := adj.unit.app c.pt }
 #align category_theory.adjunction.functoriality_unit' CategoryTheory.Adjunction.functorialityUnit'
 
 /-- The counit for the adjunction for `Cones.functoriality K G : Cone K ⥤ Cone (K ⋙ G)`.
@@ -191,8 +191,8 @@ Auxiliary definition for `functorialityIsRightAdjoint`.
 -/
 @[simps]
 def functorialityCounit' :
-  Cones.functoriality _ G ⋙ functorialityLeftAdjoint adj K ⟶ 𝟭 (Cone K) where
-    app c := { hom := adj.counit.app c.pt }
+    Cones.functoriality _ G ⋙ functorialityLeftAdjoint adj K ⟶ 𝟭 (Cone K) where
+  app c := { hom := adj.counit.app c.pt }
 #align category_theory.adjunction.functoriality_counit' CategoryTheory.Adjunction.functorialityCounit'
 
 /-- The functor `Cones.functoriality K G : Cone K ⥤ Cone (K ⋙ G)` is a right adjoint. -/

Mathlib/CategoryTheory/Adjunction/Reflective.lean

@@ -167,21 +167,21 @@ Functor.essImage.unit_isIso X.property
 /-- The counit isomorphism of the equivalence `D ≌ i.EssImageSubcategory` given
 by `equivEssImageOfReflective` when the functor `i` is reflective. -/
 def equivEssImageOfReflective_counitIso_app [Reflective i] (X : Functor.EssImageSubcategory i) :
-  ((Functor.essImageInclusion i ⋙ leftAdjoint i) ⋙ Functor.toEssImage i).obj X ≅ X := by
+    ((Functor.essImageInclusion i ⋙ leftAdjoint i) ⋙ Functor.toEssImage i).obj X ≅ X := by
   refine' Iso.symm (@asIso _ _ X _ ((ofRightAdjoint i).unit.app X.obj) ?_)
   refine @isIso_of_reflects_iso _ _ _ _ _ _ _ i.essImageInclusion ?_ _
   dsimp
   exact inferInstance
 
 lemma equivEssImageOfReflective_map_counitIso_app_hom [Reflective i]
-  (X : Functor.EssImageSubcategory i) :
+    (X : Functor.EssImageSubcategory i) :
   (Functor.essImageInclusion i).map (equivEssImageOfReflective_counitIso_app X).hom =
     inv (NatTrans.app (ofRightAdjoint i).unit X.obj) := by
     simp [equivEssImageOfReflective_counitIso_app, asIso]
     rfl
 
 lemma equivEssImageOfReflective_map_counitIso_app_inv [Reflective i]
-  (X : Functor.EssImageSubcategory i) :
+    (X : Functor.EssImageSubcategory i) :
   (Functor.essImageInclusion i).map (equivEssImageOfReflective_counitIso_app X).inv =
     (NatTrans.app (ofRightAdjoint i).unit X.obj) := rfl