chore: more indentation fixes (#27502)

Found by the linter in #27473.

Author: grunweg

Mathlib/Algebra/Algebra/NonUnitalHom.lean

@@ -86,7 +86,7 @@ namespace NonUnitalAlgHomClass
 
 -- See note [lower instance priority]
 instance (priority := 100) toNonUnitalRingHomClass
-  {F R S A B : Type*} {_ : Monoid R} {_ : Monoid S} {φ : outParam (R →* S)}
+    {F R S A B : Type*} {_ : Monoid R} {_ : Monoid S} {φ : outParam (R →* S)}
     {_ : NonUnitalNonAssocSemiring A} [DistribMulAction R A]
     {_ : NonUnitalNonAssocSemiring B} [DistribMulAction S B] [FunLike F A B]
     [NonUnitalAlgSemiHomClass F φ A B] : NonUnitalRingHomClass F A B :=

Mathlib/Algebra/Azumaya/Defs.lean

@@ -32,8 +32,7 @@ variable (R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A]
 open TensorProduct MulOpposite
 
 /-- `A` as a `A ⊗[R] Aᵐᵒᵖ`-module (or equivalently, an `A`-`A` bimodule). -/
-abbrev instModuleTensorProductMop :
-  Module (A ⊗[R] Aᵐᵒᵖ) A := TensorProduct.Algebra.module
+abbrev instModuleTensorProductMop : Module (A ⊗[R] Aᵐᵒᵖ) A := TensorProduct.Algebra.module
 
 /-- The canonical map from `A ⊗[R] Aᵐᵒᵖ` to `Module.End R A` where
   `a ⊗ b` maps to `f : x ↦ a * x * b`. -/

Mathlib/Algebra/Category/FGModuleCat/Basic.lean

@@ -87,7 +87,7 @@ section Ring
 variable (R : Type u) [Ring R]
 
 @[simp] lemma hom_comp (A B C : FGModuleCat.{v} R) (f : A ⟶ B) (g : B ⟶ C) :
-  (f ≫ g).hom = g.hom.comp f.hom := rfl
+    (f ≫ g).hom = g.hom.comp f.hom := rfl
 
 @[simp] lemma hom_id (A : FGModuleCat.{v} R) : (𝟙 A : A ⟶ A).hom = LinearMap.id := rfl
 
@@ -100,7 +100,7 @@ abbrev of (V : Type v) [AddCommGroup V] [Module R V] [Module.Finite R V] : FGMod
 
 @[simp]
 lemma of_carrier (V : Type v) [AddCommGroup V] [Module R V] [Module.Finite R V] :
-  of R V = V := rfl
+    of R V = V := rfl
 
 variable {R} in
 /-- Lift a linear map between finitely generated modules to `FGModuleCat R`. -/

Mathlib/Algebra/Category/Grp/Basic.lean

@@ -378,8 +378,7 @@ lemma hom_ext {X Y : CommGrp} {f g : X ⟶ Y} (hf : f.hom = g.hom) : f = g :=
   Hom.ext hf
 
 @[to_additive (attr := simp)]
-lemma hom_ofHom {X Y : Type u} [CommGroup X] [CommGroup Y] (f : X →* Y) :
-  (ofHom f).hom = f := rfl
+lemma hom_ofHom {X Y : Type u} [CommGroup X] [CommGroup Y] (f : X →* Y) : (ofHom f).hom = f := rfl
 
 @[to_additive (attr := simp)]
 lemma ofHom_hom {X Y : CommGrp} (f : X ⟶ Y) :

Mathlib/Algebra/Category/Grp/Limits.lean

@@ -170,8 +170,7 @@ instance forget₂Mon_preservesLimitsOfSize [UnivLE.{v, u}] :
   preservesLimitsOfShape {J _} := { }
 
 @[to_additive]
-instance forget₂Mon_preservesLimits :
-  PreservesLimits (forget₂ Grp.{u} MonCat.{u}) :=
+instance forget₂Mon_preservesLimits : PreservesLimits (forget₂ Grp.{u} MonCat.{u}) :=
   Grp.forget₂Mon_preservesLimitsOfSize.{u, u}
 
 /-- If `J` is `u`-small, the forgetful functor from `Grp.{u}` preserves limits of shape `J`. -/

Mathlib/Algebra/Category/GrpWithZero.lean

@@ -64,8 +64,7 @@ lemma coe_id {X : GrpWithZero} : (𝟙 X : X → X) = id := rfl
 
 lemma coe_comp {X Y Z : GrpWithZero} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
 
-@[simp] lemma forget_map {X Y : GrpWithZero} (f : X ⟶ Y) :
-  (forget GrpWithZero).map f = f := rfl
+@[simp] lemma forget_map {X Y : GrpWithZero} (f : X ⟶ Y) : (forget GrpWithZero).map f = f := rfl
 
 instance hasForgetToBipointed : HasForget₂ GrpWithZero Bipointed where
   forget₂ :=

Mathlib/Algebra/Category/ModuleCat/Colimits.lean

@@ -147,6 +147,6 @@ example (R : Type u) [Ring R] : HasCoequalizers (ModuleCat.{u} R) := by
 instance : HasCoequalizers (ModuleCat.{v} R) where
 
 noncomputable example (R : Type u) [Ring R] :
-  PreservesColimits (forget₂ (ModuleCat.{u} R) AddCommGrp) := inferInstance
+    PreservesColimits (forget₂ (ModuleCat.{u} R) AddCommGrp) := inferInstance
 
 end ModuleCat

Mathlib/Algebra/Category/ModuleCat/Presheaf.lean

@@ -375,7 +375,7 @@ noncomputable def forgetToPresheafModuleCatObjMap {Y Z : Cᵒᵖ} (f : Y ⟶ Z)
 
 @[simp]
 lemma forgetToPresheafModuleCatObjMap_apply {Y Z : Cᵒᵖ} (f : Y ⟶ Z) (m : M.obj Y) :
-  (forgetToPresheafModuleCatObjMap X hX M f).hom m = M.map f m := rfl
+    (forgetToPresheafModuleCatObjMap X hX M f).hom m = M.map f m := rfl
 
 /--
 Implementation of the functor `PresheafOfModules R ⥤ Cᵒᵖ ⥤ ModuleCat (R.obj X)`

Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean

@@ -89,16 +89,14 @@ abbrev ofHom {X Y : Type v}
     [AddCommGroup X] [Module R X] [TopologicalSpace X] [ContinuousAdd X] [ContinuousSMul R X]
     [AddCommGroup Y] [Module R Y] [TopologicalSpace Y] [ContinuousAdd Y] [ContinuousSMul R Y]
     (f : X →L[R] Y) :
-  (ofHom f).hom = f := rfl
+    (ofHom f).hom = f := rfl
 
-@[simp] lemma ofHom_hom {X Y : TopModuleCat R} (f : X.Hom Y) :
-  ofHom f.hom = f := rfl
+@[simp] lemma ofHom_hom {X Y : TopModuleCat R} (f : X.Hom Y) : ofHom f.hom = f := rfl
 
 @[simp] lemma hom_comp {X Y Z : TopModuleCat R} (f : X ⟶ Y) (g : Y ⟶ Z) :
-  (f ≫ g).hom = g.hom.comp f.hom := rfl
+    (f ≫ g).hom = g.hom.comp f.hom := rfl
 
-@[simp] lemma hom_id (X : TopModuleCat R) :
-  hom (𝟙 X) = .id _ _ := rfl
+@[simp] lemma hom_id (X : TopModuleCat R) : hom (𝟙 X) = .id _ _ := rfl
 
 /-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/
 def Hom.Simps.hom (A B : TopModuleCat.{v} R) (f : A.Hom B) :=
@@ -157,8 +155,7 @@ instance [CommRing S] : Linear S (TopModuleCat S) where
   comp_smul _ _ _ _ _ _ := ConcreteCategory.ext (ContinuousLinearMap.smul_comp _ _ _)
 
 @[simp]
-lemma hom_smul {M₁ M₂ : TopModuleCat S} (s : S) (φ : M₁ ⟶ M₂) :
-  (s • φ).hom = s • φ.hom := rfl
+lemma hom_smul {M₁ M₂ : TopModuleCat S} (s : S) (φ : M₁ ⟶ M₂) : (s • φ).hom = s • φ.hom := rfl
 
 end CommRing
 
@@ -184,7 +181,7 @@ instance : (forget₂ (TopModuleCat R) TopCat).ReflectsIsomorphisms where
 
 @[simp]
 lemma hom_forget₂_TopCat_map {X Y : TopModuleCat R} (f : X ⟶ Y) :
-  ((forget₂ _ TopCat).map f).hom = f.hom := rfl
+    ((forget₂ _ TopCat).map f).hom = f.hom := rfl
 
 @[simp]
 lemma forget₂_TopCat_obj {X : TopModuleCat R} : ((forget₂ _ TopCat).obj X : Type _) = X := rfl

Mathlib/Algebra/Category/MonCat/FilteredColimits.lean

@@ -75,8 +75,8 @@ variable [IsFiltered J]
 @[to_additive
   "As `J` is nonempty, we can pick an arbitrary object `j₀ : J`. We use this object to
   define the \"zero\" in the colimit as the equivalence class of `⟨j₀, 0 : F.obj j₀⟩`."]
-noncomputable instance colimitOne :
-  One (M.{v, u} F) where one := M.mk F ⟨IsFiltered.nonempty.some,1⟩
+noncomputable instance colimitOne : One (M.{v, u} F) where
+  one := M.mk F ⟨IsFiltered.nonempty.some,1⟩
 
 /-- The definition of the "one" in the colimit is independent of the chosen object of `J`.
 In particular, this lemma allows us to "unfold" the definition of `colimit_one` at a custom chosen