chore: various indentation fixes (leanprover-community#27869)

grunweg · grunweg · commit 359a2a60a2ce · 2025-08-02T11:30:50.000Z
Found by the linter in leanprover-community#27525.
diff --git a/Mathlib/Algebra/Lie/Weights/RootSystem.lean b/Mathlib/Algebra/Lie/Weights/RootSystem.lean
@@ -429,10 +429,9 @@ section IsSimple
 variable [IsSimple K L]
 
 open Weight in
-lemma eq_top_of_invtSubmodule_ne_bot
-   (q : Submodule K (Dual K H))
-   (h₀ : ∀ (i : H.root), q ∈ End.invtSubmodule ((rootSystem H).reflection i))
-   (h₁ : q ≠ ⊥) : q = ⊤ := by
+lemma eq_top_of_invtSubmodule_ne_bot (q : Submodule K (Dual K H))
+    (h₀ : ∀ (i : H.root), q ∈ End.invtSubmodule ((rootSystem H).reflection i))
+    (h₁ : q ≠ ⊥) : q = ⊤ := by
   have _i := nontrivial_of_isIrreducible K L L
   let S := rootSystem H
   by_contra h₃
diff --git a/Mathlib/Algebra/Order/Monoid/LocallyFiniteOrder.lean b/Mathlib/Algebra/Order/Monoid/LocallyFiniteOrder.lean
@@ -107,11 +107,11 @@ def LocallyFiniteOrder.orderAddMonoidHom :
 
 @[simp]
 lemma LocallyFiniteOrder.orderAddMonoidHom_toAddMonoidHom :
-  orderAddMonoidHom G = addMonoidHom G := rfl
+    orderAddMonoidHom G = addMonoidHom G := rfl
 
 @[simp]
 lemma LocallyFiniteOrder.orderAddMonoidHom_apply (x : G) :
-  orderAddMonoidHom G x = addMonoidHom G x := rfl
+    orderAddMonoidHom G x = addMonoidHom G x := rfl
 
 lemma LocallyFiniteOrder.orderAddMonoidHom_strictMono :
     StrictMono (orderAddMonoidHom G) := by
@@ -158,7 +158,7 @@ def LocallyFiniteOrder.orderAddMonoidEquiv [Nontrivial G] :
     · simp [orderAddMonoidHom, addMonoidHom, hb]
 
 lemma LocallyFiniteOrder.orderAddMonoidEquiv_apply [Nontrivial G] (x : G) :
-  orderAddMonoidEquiv G x = addMonoidHom G x := rfl
+    orderAddMonoidEquiv G x = addMonoidHom G x := rfl
 
 /-- Any linearly ordered abelian group that is locally finite embeds to `Multiplicative ℤ`. -/
 noncomputable
diff --git a/Mathlib/AlgebraicGeometry/AffineSpace.lean b/Mathlib/AlgebraicGeometry/AffineSpace.lean
@@ -465,8 +465,8 @@ One should bear this equality in mind when breaking the `Spec R/ PrimeSpectrum R
 boundary, since these instances are not definitionally equal.
 -/
 example (R : CommRingCat) :
-    inferInstance (α := Preorder (Spec R)) =
-    inferInstance (α := Preorder (PrimeSpectrum R)ᵒᵈ) := by aesop (add simp spec_le_iff)
+    inferInstance (α := Preorder (Spec R)) = inferInstance (α := Preorder (PrimeSpectrum R)ᵒᵈ) := by
+  aesop (add simp spec_le_iff)
 
 end instances
 
diff --git a/Mathlib/Analysis/InnerProductSpace/Harmonic/Constructions.lean b/Mathlib/Analysis/InnerProductSpace/Harmonic/Constructions.lean
@@ -52,13 +52,14 @@ theorem AnalyticAt.harmonicAt_re {f : ℂ → ℂ} (h : AnalyticAt ℂ f x) :
 If `f : ℂ → ℂ` is complex-analytic, then its imaginary part is harmonic.
 -/
 theorem AnalyticAt.harmonicAt_im {f : ℂ → ℂ} (h : AnalyticAt ℂ f x) :
-  HarmonicAt (fun z ↦ (f z).im) x := h.harmonicAt.comp_CLM imCLM
+    HarmonicAt (fun z ↦ (f z).im) x :=
+  h.harmonicAt.comp_CLM imCLM
 
 /--
 If `f : ℂ → ℂ` is complex-analytic, then its complex conjugate is harmonic.
 -/
-theorem AnalyticAt.harmonicAt_conj {f : ℂ → ℂ} (h : AnalyticAt ℂ f x) :
-  HarmonicAt (conj f) x := (harmonicAt_comp_CLE_iff conjCLE).2 h.harmonicAt
+theorem AnalyticAt.harmonicAt_conj {f : ℂ → ℂ} (h : AnalyticAt ℂ f x) : HarmonicAt (conj f) x :=
+  (harmonicAt_comp_CLE_iff conjCLE).2 h.harmonicAt
 
 /-!
 ## Harmonicity of `log ‖analytic‖`
diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean
@@ -240,7 +240,7 @@ variable {J} in
 is a transfinite composition of pushouts of monomorphisms in the
 family `generatingMonomorphisms G`. -/
 noncomputable def transfiniteCompositionOfShapeMapFromBot (j : J) :
-  (generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape (Set.Iic j)
+    (generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape (Set.Iic j)
     ((functor hG A₀ J).map (homOfLE bot_le : ⊥ ⟶ j)) where
   F := (Set.initialSegIic j).monotone.functor ⋙ functor hG A₀ J
   isoBot := Iso.refl _
diff --git a/Mathlib/CategoryTheory/Bicategory/Functor/Oplax.lean b/Mathlib/CategoryTheory/Bicategory/Functor/Oplax.lean
@@ -68,7 +68,7 @@ structure OplaxFunctor (B : Type u₁) [Bicategory.{w₁, v₁} B] (C : Type u
   map₂_associator :
     ∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
       map₂ (α_ f g h).hom ≫ mapComp f (g ≫ h) ≫ map f ◁ mapComp g h =
-    mapComp (f ≫ g) h ≫ mapComp f g ▷ map h ≫ (α_ (map f) (map g) (map h)).hom := by
+      mapComp (f ≫ g) h ≫ mapComp f g ▷ map h ≫ (α_ (map f) (map g) (map h)).hom := by
     aesop_cat
   /-- Oplax left unity. -/
   map₂_leftUnitor :
diff --git a/Mathlib/CategoryTheory/EffectiveEpi/Basic.lean b/Mathlib/CategoryTheory/EffectiveEpi/Basic.lean
@@ -110,7 +110,7 @@ structure EffectiveEpiFamilyStruct {B : C} {α : Type*}
   `X ⟶ W`...
   -/
   desc : ∀ {W} (e : (a : α) → (X a ⟶ W)),
-          (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
+      (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
       g₁ ≫ π _ = g₂ ≫ π _ → g₁ ≫ e _ = g₂ ≫ e _) → (B ⟶ W)
   /-- ...factorizing the components of `e` through the components of `π`... -/
   fac : ∀ {W} (e : (a : α) → (X a ⟶ W))
diff --git a/Mathlib/CategoryTheory/GradedObject/Trifunctor.lean b/Mathlib/CategoryTheory/GradedObject/Trifunctor.lean
@@ -291,8 +291,8 @@ lemma ιMapBifunctor₁₂BifunctorMapObj_eq (i₁ : I₁) (i₂ : I₂) (i₃ :
     (h : r (i₁, i₂, i₃) = j) (i₁₂ : ρ₁₂.I₁₂) (h₁₂ : ρ₁₂.p ⟨i₁, i₂⟩ = i₁₂) :
     ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h =
       (G.map (ιMapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂ i₁ i₂ i₁₂ h₁₂)).app (X₃ i₃) ≫
-    ιMapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ i₁₂ i₃ j
-      (by rw [← h₁₂, ← h, ← ρ₁₂.hpq]) := by
+      ιMapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ i₁₂ i₃ j
+        (by rw [← h₁₂, ← h, ← ρ₁₂.hpq]) := by
   subst h₁₂
   rfl
 
diff --git a/Mathlib/CategoryTheory/Join/Pseudofunctor.lean b/Mathlib/CategoryTheory/Join/Pseudofunctor.lean
@@ -78,17 +78,17 @@ variable (A) in
 @[reassoc]
 lemma mapWhiskerLeft_associator_hom (F : B ⥤ C) (G : C ⥤ D) (H : D ⥤ E) :
     mapWhiskerLeft _ (F.associator G H).hom =
-    (mapCompRight A (F ⋙ G) H).hom ≫ whiskerRight (mapCompRight A F G).hom (mapPair (𝟭 A) H) ≫
+      (mapCompRight A (F ⋙ G) H).hom ≫ whiskerRight (mapCompRight A F G).hom (mapPair (𝟭 A) H) ≫
       ((mapPair (𝟭 A) F).associator (mapPair (𝟭 A) G) (mapPair (𝟭 A) H)).hom ≫
-    whiskerLeft (mapPair (𝟭 A) F) (mapCompRight A G H).inv ≫ (mapCompRight A F (G ⋙ H)).inv := by
+      whiskerLeft (mapPair (𝟭 A) F) (mapCompRight A G H).inv ≫ (mapCompRight A F (G ⋙ H)).inv := by
   apply natTrans_ext <;> ext <;> simp [mapCompRight]
 
 variable (E) in
 lemma mapWhiskerRight_associator_hom (F : A ⥤ B) (G : B ⥤ C) (H : C ⥤ D) :
     mapWhiskerRight (F.associator G H).hom _ =
     (mapCompLeft E (F ⋙ G) H).hom ≫ whiskerRight (mapCompLeft E F G).hom (mapPair H (𝟭 E)) ≫
       ((mapPair F (𝟭 E)).associator (mapPair G (𝟭 E)) (mapPair H (𝟭 E))).hom ≫
-    whiskerLeft (mapPair F (𝟭 E)) (mapCompLeft E G H).inv ≫ (mapCompLeft E F (G ⋙ H)).inv := by
+      whiskerLeft (mapPair F (𝟭 E)) (mapCompLeft E G H).inv ≫ (mapCompLeft E F (G ⋙ H)).inv := by
   apply natTrans_ext <;> ext <;> simp [mapCompLeft]
 
 variable (A) in
diff --git a/Mathlib/CategoryTheory/Limits/HasLimits.lean b/Mathlib/CategoryTheory/Limits/HasLimits.lean
@@ -1027,11 +1027,10 @@ theorem colimit.pre_id (F : J ⥤ C) :
     colimit.pre F (𝟭 _) = colim.map (Functor.leftUnitor F).hom := by aesop_cat
 
 theorem colimit.map_post {D : Type u'} [Category.{v'} D] [HasColimitsOfShape J D]
-    (H : C ⥤ D) :/- H (colimit F) ⟶ H (colimit G) ⟶ colimit (G ⋙ H) vs
-             H (colimit F) ⟶ colimit (F ⋙ H) ⟶ colimit (G ⋙ H) -/
-          colimit.post
-          F H ≫
-        H.map (colim.map α) =
+    (H : C ⥤ D) :
+    /- H (colimit F) ⟶ H (colimit G) ⟶ colimit (G ⋙ H) vs
+      H (colimit F) ⟶ colimit (F ⋙ H) ⟶ colimit (G ⋙ H) -/
+    colimit.post F H ≫ H.map (colim.map α) =
       colim.map (whiskerRight α H) ≫ colimit.post G H := by
   ext
   rw [← assoc, colimit.ι_post, ← H.map_comp, colimit.ι_map, H.map_comp]
diff --git a/Mathlib/CategoryTheory/Localization/Trifunctor.lean b/Mathlib/CategoryTheory/Localization/Trifunctor.lean
@@ -209,12 +209,12 @@ lemma associator_hom_app_app_app (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) :
           (F₁₂ ⋙ (whiskeringRight C₂ C₁₂ D₁₂).obj L₁₂) F₁₂').hom.app X₁).app X₂)).app (L₃.obj X₃) ≫
           ((Lifting₂.iso L₁₂ L₃ W₁₂ W₃ (G ⋙ (whiskeringRight C₃ C D).obj L) G').hom.app
               ((F₁₂.obj X₁).obj X₂)).app X₃ ≫
-            L.map (((iso.hom.app X₁).app X₂).app X₃) ≫
+          L.map (((iso.hom.app X₁).app X₂).app X₃) ≫
           ((Lifting₂.iso L₁ L₂₃ W₁ W₂₃
             (F ⋙ (whiskeringRight _ _ _).obj L) F').inv.app X₁).app ((G₂₃.obj X₂).obj X₃) ≫
-        (F'.obj (L₁.obj X₁)).map
-          (((Lifting₂.iso L₂ L₃ W₂ W₃
-            (G₂₃ ⋙ (whiskeringRight _ _ _).obj L₂₃) G₂₃').inv.app X₂).app X₃) := by
+          (F'.obj (L₁.obj X₁)).map
+            (((Lifting₂.iso L₂ L₃ W₂ W₃
+              (G₂₃ ⋙ (whiskeringRight _ _ _).obj L₂₃) G₂₃').inv.app X₂).app X₃) := by
   dsimp [associator]
   rw [lift₃NatTrans_app_app_app]
   dsimp [Lifting₃.iso, Lifting₃.bifunctorComp₁₂, Lifting₃.bifunctorComp₂₃]
diff --git a/Mathlib/CategoryTheory/Shift/Localization.lean b/Mathlib/CategoryTheory/Shift/Localization.lean
@@ -155,8 +155,8 @@ lemma iso_hom_app (a : A) (X : C) :
 @[simp, reassoc]
 lemma iso_inv_app (a : A) (X : C) :
     (commShiftOfLocalization.iso L W F F' a).inv.app (L.obj X) =
-        (shiftFunctor E a).map ((Lifting.iso L W F F').hom.app X) ≫
-        (F.commShiftIso a).inv.app X ≫
+      (shiftFunctor E a).map ((Lifting.iso L W F F').hom.app X) ≫
+      (F.commShiftIso a).inv.app X ≫
       (Lifting.iso L W F F').inv.app (X⟦a⟧) ≫
       F'.map ((L.commShiftIso a).hom.app X) := by
   simp [commShiftOfLocalization.iso]
@@ -221,7 +221,7 @@ lemma commShiftOfLocalization_iso_inv_app (a : A) (X : C) :
     (F'.commShiftIso a).inv.app (L.obj X) =
       (shiftFunctor E a).map ((Lifting.iso L W F F').hom.app X) ≫
       (F.commShiftIso a).inv.app X ≫ (Lifting.iso L W F F').inv.app (X⟦a⟧) ≫
-     F'.map ((L.commShiftIso a).hom.app X) := by
+      F'.map ((L.commShiftIso a).hom.app X) := by
   apply commShiftOfLocalization.iso_inv_app
 
 end Functor
diff --git a/Mathlib/CategoryTheory/Shift/SingleFunctors.lean b/Mathlib/CategoryTheory/Shift/SingleFunctors.lean
@@ -85,8 +85,8 @@ lemma shiftIso_add'_hom_app (n m mn : A) (hnm : m + n = mn) (a a' a'' : A)
 lemma shiftIso_add'_inv_app (n m mn : A) (hnm : m + n = mn) (a a' a'' : A)
     (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) :
     (F.shiftIso mn a a'' (by rw [← hnm, ← ha'', ← ha', add_assoc])).inv.app X =
-        (F.shiftIso n a a' ha').inv.app X ≫
-        ((F.shiftIso m a' a'' ha'').inv.app X)⟦n⟧' ≫
+      (F.shiftIso n a a' ha').inv.app X ≫
+      ((F.shiftIso m a' a'' ha'').inv.app X)⟦n⟧' ≫
       (shiftFunctorAdd' D m n mn hnm).inv.app ((F.functor a'').obj X) := by
   simp [F.shiftIso_add' n m mn hnm a a' a'' ha' ha'']
 
diff --git a/Mathlib/CategoryTheory/Sites/Coherent/Basic.lean b/Mathlib/CategoryTheory/Sites/Coherent/Basic.lean
@@ -55,12 +55,10 @@ class Precoherent : Prop where
   an effective epi family `π₂` over `B₂`, such that `π₂` factors through `π₁`.
   -/
   pullback {B₁ B₂ : C} (f : B₂ ⟶ B₁) :
-    ∀ (α : Type) [Finite α] (X₁ : α → C) (π₁ : (a : α) → (X₁ a ⟶ B₁)),
-      EffectiveEpiFamily X₁ π₁ →
+    ∀ (α : Type) [Finite α] (X₁ : α → C) (π₁ : (a : α) → (X₁ a ⟶ B₁)), EffectiveEpiFamily X₁ π₁ →
     ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → (X₂ b ⟶ B₂)),
       EffectiveEpiFamily X₂ π₂ ∧
-      ∃ (i : β → α) (ι : (b :  β) → (X₂ b ⟶ X₁ (i b))),
-      ∀ (b : β), ι b ≫ π₁ _ = π₂ _ ≫ f
+    ∃ (i : β → α) (ι : (b :  β) → (X₂ b ⟶ X₁ (i b))), ∀ (b : β), ι b ≫ π₁ _ = π₂ _ ≫ f
 
 /--
 The coherent coverage on a precoherent category `C`.
diff --git a/Mathlib/Combinatorics/SimpleGraph/Clique.lean b/Mathlib/Combinatorics/SimpleGraph/Clique.lean
@@ -482,7 +482,7 @@ lemma CliqueFree.mem_of_sup_edge_isNClique {x y : α} {t : Finset α} {n : ℕ}
 open Classical in
 /-- Adding an edge increases the clique number by at most one. -/
 protected theorem CliqueFree.sup_edge (h : G.CliqueFree n) (v w : α) :
-   (G ⊔ edge v w).CliqueFree (n + 1) :=
+    (G ⊔ edge v w).CliqueFree (n + 1) :=
   fun _ hs ↦ (hs.erase_of_sup_edge_of_mem <|
     (h.mono n.le_succ).mem_of_sup_edge_isNClique hs).not_cliqueFree h
 
diff --git a/Mathlib/FieldTheory/JacobsonNoether.lean b/Mathlib/FieldTheory/JacobsonNoether.lean
@@ -175,7 +175,7 @@ open Subring Algebra in
   that is separable over `L`. -/
 theorem exists_separable_and_not_isCentral' {L D : Type*} [Field L] [DivisionRing D]
     [Algebra L D] [Algebra.IsAlgebraic L D] [Algebra.IsCentral L D]
-  (hneq : (⊥ : Subalgebra L D) ≠ ⊤) :
+    (hneq : (⊥ : Subalgebra L D) ≠ ⊤) :
     ∃ x : D, x ∉ (⊥ : Subalgebra L D) ∧ IsSeparable L x := by
   have hcenter : Subalgebra.center L D = ⊥ := le_bot_iff.mp IsCentral.out
   have ntrivial : Subring.center D ≠ ⊤ :=
diff --git a/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Lemmas.lean b/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Lemmas.lean
@@ -128,8 +128,8 @@ private lemma chainBotCoeff_mul_chainTopCoeff.aux_1
     have _i := P.reflexive_left; letI := P.indexNeg
     P.root i + P.root m ∈ range P.root → P.root j + P.root (-l) ∈ range P.root →
       P.root j + P.root (-k) ∈ range P.root →
-    (P.chainBotCoeff i m + 1) * (P.chainBotCoeff j (-k) + 1) =
-      (P.chainBotCoeff j (-l) + 1) * (P.chainBotCoeff i k + 1) := by
+      (P.chainBotCoeff i m + 1) * (P.chainBotCoeff j (-k) + 1) =
+        (P.chainBotCoeff j (-l) + 1) * (P.chainBotCoeff i k + 1) := by
   intro _ him_mem hjl_mem hjk_mem
   /- Setup some typeclasses and name the 6th root `n`. -/
   letI := P.indexNeg
@@ -189,7 +189,7 @@ private lemma chainBotCoeff_mul_chainTopCoeff.aux_2
     have _i := P.reflexive_left; letI := P.indexNeg
     P.root i + P.root m ∈ range P.root → P.root j + P.root (-l) ∈ range P.root →
       P.root j + P.root (-k) ∈ range P.root →
-    ¬ (P.chainBotCoeff i m = 1 ∧ P.chainBotCoeff j (-l) = 0) := by
+      ¬ (P.chainBotCoeff i m = 1 ∧ P.chainBotCoeff j (-l) = 0) := by
   intro _ him_mem hjl_mem hjk_mem
   letI := P.indexNeg
   /- Setup some typeclasses. -/
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean b/Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean
@@ -274,8 +274,9 @@ theorem rTensor_injective_of_forall_fg_rTensor_injective
   (forall_vanishesTrivially_iff_forall_rTensor_injective R).mp
     ((forall_vanishesTrivially_iff_forall_fg_rTensor_injective R).mpr hMN) M'
 
-@[deprecated (since := "2025-01-03")] alias forall_vanishesTrivially_iff_forall_FG_rTensor_injective
-  := forall_vanishesTrivially_iff_forall_fg_rTensor_injective
+@[deprecated (since := "2025-01-03")] alias
+forall_vanishesTrivially_iff_forall_FG_rTensor_injective :=
+  forall_vanishesTrivially_iff_forall_fg_rTensor_injective
 @[deprecated (since := "2025-01-03")] alias rTensor_injective_of_forall_FG_rTensor_injective :=
   rTensor_injective_of_forall_fg_rTensor_injective
 
diff --git a/Mathlib/MeasureTheory/SetSemiring.lean b/Mathlib/MeasureTheory/SetSemiring.lean
@@ -219,8 +219,8 @@ open scoped Classical in
 `s \ ⋃₀ I = ⋃₀ (hC.disjointOfDiffUnion hs I hI)`.
 `disjointOfDiff` is a special case of `disjointOfDiffUnion` where `I` is a
 singleton. -/
-noncomputable def disjointOfDiffUnion (hC : IsSetSemiring C) (hs : s ∈ C)
-  (hI : ↑I ⊆ C) : Finset (Set α) :=
+noncomputable def disjointOfDiffUnion (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) :
+    Finset (Set α) :=
   (hC.exists_disjoint_finset_diff_eq hs hI).choose \ {∅}
 
 lemma empty_notMem_disjointOfDiffUnion (hC : IsSetSemiring C) (hs : s ∈ C)
diff --git a/Mathlib/ModelTheory/Basic.lean b/Mathlib/ModelTheory/Basic.lean
@@ -68,8 +68,7 @@ abbrev IsRelational : Prop := ∀ n, IsEmpty (L.Functions n)
 abbrev IsAlgebraic : Prop := ∀ n, IsEmpty (L.Relations n)
 
 /-- The empty language has no symbols. -/
-protected def empty : Language :=
-  ⟨fun _ => Empty, fun _ => Empty⟩
+protected def empty : Language := ⟨fun _ => Empty, fun _ => Empty⟩
   deriving IsAlgebraic, IsRelational
 
 instance : Inhabited Language :=
diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Defs.lean b/Mathlib/Order/ConditionallyCompleteLattice/Defs.lean
@@ -96,7 +96,7 @@ attribute [instance 100] ConditionallyCompleteLinearOrderBot.toOrderBot
 open scoped Classical in
 /-- A well founded linear order is conditionally complete, with a bottom element. -/
 noncomputable abbrev WellFoundedLT.conditionallyCompleteLinearOrderBot (α : Type*)
-  [i₁ : LinearOrder α] [i₂ : OrderBot α] [h : WellFoundedLT α] :
+    [i₁ : LinearOrder α] [i₂ : OrderBot α] [h : WellFoundedLT α] :
     ConditionallyCompleteLinearOrderBot α :=
   { i₁, i₂, LinearOrder.toLattice with
     sInf := fun s => if hs : s.Nonempty then h.wf.min s hs else ⊥
diff --git a/Mathlib/RingTheory/Frobenius.lean b/Mathlib/RingTheory/Frobenius.lean
@@ -179,7 +179,7 @@ Suppose `S` is an `R` algebra, `M` is a monoid acting on `S` whose action is tri
 `σ : M` is an (arithmetic) Frobenius at an ideal `Q` of `S` if `σ • x ≡ x ^ q (mod Q)` for all `x`.
 -/
 abbrev IsArithFrobAt {M : Type*} [Monoid M] [MulSemiringAction M S] [SMulCommClass M R S]
-  (σ : M) (Q : Ideal S) : Prop :=
+    (σ : M) (Q : Ideal S) : Prop :=
   (MulSemiringAction.toAlgHom R S σ).IsArithFrobAt Q
 
 namespace IsArithFrobAt
diff --git a/Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.lean b/Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.lean
@@ -663,8 +663,8 @@ lemma chevalley_mvPolynomialC
     (hSn : ∀ C ∈ S, C.n ≤ k)
     (hS : ∀ C ∈ S, ∀ j, C.g j ∈ coeffsIn _ M ⊓ (degreesLE _ _ d).restrictScalars _) :
     ∃ T : ConstructibleSetData R,
-      comap MvPolynomial.C '' S.toSet = T.toSet ∧ ∀ C ∈ T,
-        C.n ≤ numBound k (fun i ↦ 1 + (d.map Fin.val).count i) n ∧
+      comap MvPolynomial.C '' S.toSet = T.toSet ∧
+      ∀ C ∈ T, C.n ≤ numBound k (fun i ↦ 1 + (d.map Fin.val).count i) n ∧
       ∀ i, C.g i ∈ M ^ (degBound k (fun i ↦ 1 + (d.map Fin.val).count i) n) := by
   classical
   induction' n with n IH generalizing k M
diff --git a/Mathlib/RingTheory/Unramified/Finite.lean b/Mathlib/RingTheory/Unramified/Finite.lean
@@ -83,7 +83,7 @@ lemma finite_of_free_aux (I) [DecidableEq I] (b : Basis I R S)
     (f : I →₀ S) (x : S) (a : I → I →₀ R) (ha : a = fun i ↦ b.repr (b i * x)) :
     (1 ⊗ₜ[R] x * Finsupp.sum f fun i y ↦ y ⊗ₜ[R] b i) =
       Finset.sum (f.support.biUnion fun i ↦ (a i).support) fun k ↦
-    Finsupp.sum (b.repr (f.sum fun i y ↦ a i k • y)) fun j c ↦ c • b j ⊗ₜ[R] b k := by
+      Finsupp.sum (b.repr (f.sum fun i y ↦ a i k • y)) fun j c ↦ c • b j ⊗ₜ[R] b k := by
   rw [Finsupp.sum, Finset.mul_sum]
   subst ha
   let a i := b.repr (b i * x)
diff --git a/Mathlib/Tactic/ToAdditive/Frontend.lean b/Mathlib/Tactic/ToAdditive/Frontend.lean
@@ -1244,7 +1244,7 @@ def elabToAdditive : Syntax → CoreM Config
 mutual
 /-- Apply attributes to the multiplicative and additive declarations. -/
 partial def applyAttributes (stx : Syntax) (rawAttrs : Array Syntax) (thisAttr src tgt : Name) :
-  TermElabM (Array Name) := do
+    TermElabM (Array Name) := do
   -- we only copy the `instance` attribute, since `@[to_additive] instance` is nice to allow
   copyInstanceAttribute src tgt
   -- Warn users if the multiplicative version has an attribute
@@ -1360,7 +1360,7 @@ See the attribute implementation for more details.
 It returns an array with names of additive declarations (usually 1, but more if there are nested
 `to_additive` calls. -/
 partial def addToAdditiveAttr (src : Name) (cfg : Config) (kind := AttributeKind.global) :
-  AttrM (Array Name) := do
+    AttrM (Array Name) := do
   if (kind != AttributeKind.global) then
     throwError "`to_additive` can only be used as a global attribute"
   withOptions (· |>.updateBool `trace.to_additive (cfg.trace || ·)) <| do
diff --git a/Mathlib/Tactic/Widget/SelectPanelUtils.lean b/Mathlib/Tactic/Widget/SelectPanelUtils.lean
diff --git a/Mathlib/Topology/Algebra/ProperAction/Basic.lean b/Mathlib/Topology/Algebra/ProperAction/Basic.lean
diff --git a/Mathlib/Topology/GDelta/Basic.lean b/Mathlib/Topology/GDelta/Basic.lean
