style: a linter for colons (#6761)

A linter that throws on seeing a colon at the start of a line, according to the [style guideline](https://leanprover-community.github.io/contribute/style.html#structuring-definitions-and-theorems) that says these operators should go before linebreaks.
leanprover-community · Sep 12, 2023 · 69a3de3 · 69a3de3
1 parent 198327e
commit 69a3de3
Show file tree

Hide file tree

Showing 40 changed files with 93 additions and 95 deletions.
diff --git a/Mathlib/Algebra/Algebra/RestrictScalars.lean b/Mathlib/Algebra/Algebra/RestrictScalars.lean
@@ -137,9 +137,9 @@ instance RestrictScalars.isCentralScalar [Module S M] [Module Sᵐᵒᵖ M] [IsC
 of `RestrictScalars R S M`.
 -/
 def RestrictScalars.lsmul [Module S M] : S →ₐ[R] Module.End R (RestrictScalars R S M) :=
-  letI-- We use `RestrictScalars.moduleOrig` in the implementation,
+  -- We use `RestrictScalars.moduleOrig` in the implementation,
   -- but not in the type.
-   : Module S (RestrictScalars R S M) := RestrictScalars.moduleOrig R S M
+  letI : Module S (RestrictScalars R S M) := RestrictScalars.moduleOrig R S M
   Algebra.lsmul R R (RestrictScalars R S M)
 #align restrict_scalars.lsmul RestrictScalars.lsmul
 

diff --git a/Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean b/Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean
@@ -148,8 +148,8 @@ some technical translation lemmas. More precisely, in this section, we show that
 number `q : ℚ` and value `v : K` with `v = ↑q`, the continued fraction of `q` and `v` coincide.
 In particular, we show that
 ```lean
-    (↑(GeneralizedContinuedFraction.of q : GeneralizedContinuedFraction ℚ)
-      : GeneralizedContinuedFraction K)
+    (↑(GeneralizedContinuedFraction.of q : GeneralizedContinuedFraction ℚ) :
+      GeneralizedContinuedFraction K)
   = GeneralizedContinuedFraction.of v`
 ```
 in `generalized_continued_fraction.coe_of_rat`.

diff --git a/Mathlib/Algebra/GCDMonoid/Finset.lean b/Mathlib/Algebra/GCDMonoid/Finset.lean
@@ -185,8 +185,8 @@ theorem gcd_union [DecidableEq β] : (s₁ ∪ s₂).gcd f = GCDMonoid.gcd (s₁
     fun a s _ ih ↦ by rw [insert_union, gcd_insert, gcd_insert, ih, gcd_assoc]
 #align finset.gcd_union Finset.gcd_union
 
-theorem gcd_congr {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ a ∈ s₂, f a = g a)
-    : s₁.gcd f = s₂.gcd g := by
+theorem gcd_congr {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ a ∈ s₂, f a = g a) :
+    s₁.gcd f = s₂.gcd g := by
   subst hs
   exact Finset.fold_congr hfg
 #align finset.gcd_congr Finset.gcd_congr

diff --git a/Mathlib/Algebra/Order/Interval.lean b/Mathlib/Algebra/Order/Interval.lean
@@ -305,8 +305,7 @@ namespace NonemptyInterval
 @[to_additive]
 theorem coe_pow_interval [OrderedCommMonoid α] (s : NonemptyInterval α) (n : ℕ) :
     (s ^ n : Interval α) = (s : Interval α) ^ n :=
-  map_pow ({ toFun := (↑), map_one' := coe_one_interval, map_mul' := coe_mul_interval }
-    : NonemptyInterval α →* Interval α) _ _
+  map_pow (⟨⟨(↑), coe_one_interval⟩, coe_mul_interval⟩ : NonemptyInterval α →* Interval α) _ _
 #align nonempty_interval.coe_pow_interval NonemptyInterval.coe_pow_interval
 #align nonempty_interval.coe_nsmul_interval NonemptyInterval.coe_nsmul_interval
 
@@ -667,8 +666,7 @@ theorem length_sub : (s - t).length = s.length + t.length := by simp [sub_eq_add
 @[simp]
 theorem length_sum (f : ι → NonemptyInterval α) (s : Finset ι) :
     (∑ i in s, f i).length = ∑ i in s, (f i).length :=
-  map_sum ({ toFun := length, map_zero' := length_zero, map_add' := length_add}
-    : NonemptyInterval α →+ α) _ _
+  map_sum (⟨⟨length, length_zero⟩, length_add⟩ : NonemptyInterval α →+ α) _ _
 #align nonempty_interval.length_sum NonemptyInterval.length_sum
 
 end NonemptyInterval

diff --git a/Mathlib/Algebra/Order/Ring/Lemmas.lean b/Mathlib/Algebra/Order/Ring/Lemmas.lean
@@ -813,8 +813,8 @@ theorem lt_mul_of_lt_of_one_lt_of_pos [PosMulStrictMono α] [MulPosStrictMono α
 /-! Lemmas of the form `a ≤ 1 → b ≤ c → a * b ≤ c`. -/
 
 
-theorem mul_le_of_le_one_of_le_of_nonneg [MulPosMono α] (ha : a ≤ 1) (h : b ≤ c) (hb : 0 ≤ b)
-    : a * b ≤ c :=
+theorem mul_le_of_le_one_of_le_of_nonneg [MulPosMono α] (ha : a ≤ 1) (h : b ≤ c) (hb : 0 ≤ b) :
+    a * b ≤ c :=
   (mul_le_of_le_one_left hb ha).trans h
 #align mul_le_of_le_one_of_le_of_nonneg mul_le_of_le_one_of_le_of_nonneg
 
@@ -922,8 +922,8 @@ theorem lt_of_lt_mul_of_le_one_of_nonneg_right [MulPosMono α] (h : a < b * c) (
   h.trans_le <| mul_le_of_le_one_left hc hb
 #align lt_of_lt_mul_of_le_one_of_nonneg_right lt_of_lt_mul_of_le_one_of_nonneg_right
 
-theorem le_mul_of_one_le_of_le_of_nonneg [MulPosMono α] (ha : 1 ≤ a) (bc : b ≤ c) (c0 : 0 ≤ c)
-    : b ≤ a * c :=
+theorem le_mul_of_one_le_of_le_of_nonneg [MulPosMono α] (ha : 1 ≤ a) (bc : b ≤ c) (c0 : 0 ≤ c) :
+    b ≤ a * c :=
   bc.trans <| le_mul_of_one_le_left c0 ha
 #align le_mul_of_one_le_of_le_of_nonneg le_mul_of_one_le_of_le_of_nonneg
 

diff --git a/Mathlib/CategoryTheory/Limits/Constructions/Equalizers.lean b/Mathlib/CategoryTheory/Limits/Constructions/Equalizers.lean
@@ -160,8 +160,8 @@ def coequalizerCocone (F : WalkingParallelPair ⥤ C) : Cocone F :=
   Cocone.ofCofork
     (Cofork.ofπ (pushoutInl F) (by
         conv_rhs => rw [pushoutInl_eq_pushout_inr]
-        convert (whisker_eq Limits.coprod.inr pushout.condition
-          : (_ : F.obj _ ⟶ constructCoequalizer _) = _) using 1 <;> simp))
+        convert (whisker_eq Limits.coprod.inr pushout.condition :
+          (_ : F.obj _ ⟶ constructCoequalizer _) = _) using 1 <;> simp))
 #align category_theory.limits.has_coequalizers_of_has_pushouts_and_binary_coproducts.coequalizer_cocone CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.coequalizerCocone
 
 /-- Show the equalizing cocone is a colimit -/

diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Basic.lean b/Mathlib/CategoryTheory/Limits/Preserves/Basic.lean
@@ -134,8 +134,8 @@ def isColimitOfPreserves (F : C ⥤ D) {c : Cocone K} (t : IsColimit c) [Preserv
   PreservesColimit.preserves t
 #align category_theory.limits.is_colimit_of_preserves CategoryTheory.Limits.isColimitOfPreserves
 
-instance preservesLimit_subsingleton (K : J ⥤ C) (F : C ⥤ D) : Subsingleton (PreservesLimit K F)
-    := by
+instance preservesLimit_subsingleton (K : J ⥤ C) (F : C ⥤ D) :
+    Subsingleton (PreservesLimit K F) := by
   constructor; rintro ⟨a⟩ ⟨b⟩; congr!
 #align category_theory.limits.preserves_limit_subsingleton CategoryTheory.Limits.preservesLimit_subsingleton
 

diff --git a/Mathlib/CategoryTheory/Limits/Presheaf.lean b/Mathlib/CategoryTheory/Limits/Presheaf.lean
@@ -84,8 +84,7 @@ def restrictedYonedaYoneda : restrictedYoneda (yoneda : C ⥤ Cᵒᵖ ⥤ Type u
       funext fun x => by
         dsimp
         have : x.app X (CategoryStruct.id (Opposite.unop X)) =
-            (x.app X (𝟙 (Opposite.unop X)))
-              := rfl
+            (x.app X (𝟙 (Opposite.unop X))) := rfl
         rw [this]
         rw [← FunctorToTypes.naturality _ _ x f (𝟙 _)]
         simp only [id_comp, Functor.op_obj, Opposite.unop_op, yoneda_obj_map, comp_id]

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean b/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
@@ -523,8 +523,8 @@ def Cofork.IsColimit.mk (t : Cofork f g) (desc : ∀ s : Cofork f g, t.pt ⟶ s.
     only asks for a proof of facts that carry any mathematical content, and allows access to the
     same `s` for all parts. -/
 def Cofork.IsColimit.mk' {X Y : C} {f g : X ⟶ Y} (t : Cofork f g)
-    (create : ∀ s : Cofork f g, { l : t.pt ⟶ s.pt // t.π ≫ l = s.π ∧ ∀ {m}, t.π ≫ m = s.π → m = l })
-    : IsColimit t :=
+    (create : ∀ s : Cofork f g, { l : t.pt ⟶ s.pt // t.π ≫ l = s.π
+                                    ∧ ∀ {m}, t.π ≫ m = s.π → m = l }) : IsColimit t :=
   Cofork.IsColimit.mk t (fun s => (create s).1) (fun s => (create s).2.1) fun s _ w =>
     (create s).2.2 w
 #align category_theory.limits.cofork.is_colimit.mk' CategoryTheory.Limits.Cofork.IsColimit.mk'

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.lean b/Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.lean
@@ -69,9 +69,9 @@ theorem hasFiniteLimits_of_hasFiniteLimits_of_size
     HasFiniteLimits C where
   out := fun J hJ hhJ => by
     haveI := h (ULiftHom.{w} (ULift.{w} J)) <| @CategoryTheory.finCategoryUlift J hJ hhJ
-    have l :
-      @Equivalence J (ULiftHom (ULift J)) hJ (@ULiftHom.category (ULift J) (@uliftCategory J hJ))
-      := @ULiftHomULiftCategory.equiv J hJ
+    have l : @Equivalence J (ULiftHom (ULift J)) hJ
+                          (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) :=
+      @ULiftHomULiftCategory.equiv J hJ
     apply @hasLimitsOfShape_of_equivalence (ULiftHom (ULift J))
       (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) C _ J hJ
       (@Equivalence.symm J hJ (ULiftHom (ULift J))
@@ -114,9 +114,9 @@ theorem hasFiniteColimits_of_hasFiniteColimits_of_size
     HasFiniteColimits C where
   out := fun J hJ hhJ => by
     haveI := h (ULiftHom.{w} (ULift.{w} J)) <| @CategoryTheory.finCategoryUlift J hJ hhJ
-    have l :
-      @Equivalence J (ULiftHom (ULift J)) hJ (@ULiftHom.category (ULift J) (@uliftCategory J hJ))
-      := @ULiftHomULiftCategory.equiv J hJ
+    have l : @Equivalence J (ULiftHom (ULift J)) hJ
+                           (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) :=
+      @ULiftHomULiftCategory.equiv J hJ
     apply @hasColimitsOfShape_of_equivalence (ULiftHom (ULift J))
       (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) C _ J hJ
       (@Equivalence.symm J hJ (ULiftHom (ULift J))

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean
@@ -1708,8 +1708,8 @@ theorem pullbackConeOfRightIso_π_app_left : (pullbackConeOfRightIso f g).π.app
 #align category_theory.limits.pullback_cone_of_right_iso_π_app_left CategoryTheory.Limits.pullbackConeOfRightIso_π_app_left
 
 @[simp]
-theorem pullbackConeOfRightIso_π_app_right : (pullbackConeOfRightIso f g).π.app right = f ≫ inv g
-  := rfl
+theorem pullbackConeOfRightIso_π_app_right : (pullbackConeOfRightIso f g).π.app right = f ≫ inv g :=
+  rfl
 #align category_theory.limits.pullback_cone_of_right_iso_π_app_right CategoryTheory.Limits.pullbackConeOfRightIso_π_app_right
 
 /-- Verify that the constructed limit cone is indeed a limit. -/

diff --git a/Mathlib/CategoryTheory/Limits/Types.lean b/Mathlib/CategoryTheory/Limits/Types.lean
@@ -505,8 +505,7 @@ noncomputable def isColimitOf (t : Cocone F) (hsurj : ∀ x : t.pt, ∃ i xi, x
       intro a b h
       rcases jointly_surjective.{v, u} F (colimit.isColimit F) a with ⟨i, xi, rfl⟩
       rcases jointly_surjective.{v, u} F (colimit.isColimit F) b with ⟨j, xj, rfl⟩
-      replace h : (colimit.ι F i ≫ colimit.desc F t) xi = (colimit.ι F j ≫ colimit.desc F t) xj
-        := h
+      replace h : (colimit.ι F i ≫ colimit.desc F t) xi = (colimit.ι F j ≫ colimit.desc F t) xj := h
       rw [colimit.ι_desc, colimit.ι_desc] at h
       rcases hinj i j xi xj h with ⟨k, f, g, h'⟩
       change colimit.ι F i xi = colimit.ι F j xj

diff --git a/Mathlib/CategoryTheory/Monad/Monadicity.lean b/Mathlib/CategoryTheory/Monad/Monadicity.lean
@@ -434,8 +434,8 @@ def monadicOfHasPreservesReflexiveCoequalizersOfReflectsIsomorphisms : MonadicRi
     ⟨_, comparisonAdjunction⟩
   constructor
   let _ : ∀ X : (Adjunction.ofRightAdjoint G).toMonad.Algebra,
-      IsIso ((Adjunction.ofRightAdjoint (comparison (Adjunction.ofRightAdjoint G))).unit.app X)
-    := by
+      IsIso ((Adjunction.ofRightAdjoint
+                (comparison (Adjunction.ofRightAdjoint G))).unit.app X) := by
     intro X
     apply
       @isIso_of_reflects_iso _ _ _ _ _ _ _ (Monad.forget (Adjunction.ofRightAdjoint G).toMonad) ?_ _

diff --git a/Mathlib/CategoryTheory/Monoidal/Category.lean b/Mathlib/CategoryTheory/Monoidal/Category.lean
@@ -292,8 +292,9 @@ theorem rightUnitor_conjugation {X Y : C} (f : X ⟶ Y) :
 #align category_theory.monoidal_category.right_unitor_conjugation CategoryTheory.MonoidalCategory.rightUnitor_conjugation
 
 @[simp]
-theorem leftUnitor_conjugation {X Y : C} (f : X ⟶ Y) : 𝟙 (𝟙_ C) ⊗ f = (λ_ X).hom ≫ f ≫ (λ_ Y).inv
-  := by rw [← leftUnitor_naturality_assoc, Iso.hom_inv_id, Category.comp_id]
+theorem leftUnitor_conjugation {X Y : C} (f : X ⟶ Y) :
+    𝟙 (𝟙_ C) ⊗ f = (λ_ X).hom ≫ f ≫ (λ_ Y).inv := by
+  rw [← leftUnitor_naturality_assoc, Iso.hom_inv_id, Category.comp_id]
 #align category_theory.monoidal_category.left_unitor_conjugation CategoryTheory.MonoidalCategory.leftUnitor_conjugation
 
 @[reassoc]

diff --git a/Mathlib/CategoryTheory/Pi/Basic.lean b/Mathlib/CategoryTheory/Pi/Basic.lean
@@ -239,8 +239,8 @@ theorem pi'_eval (f : ∀ i, A ⥤ C i) (i : I) : pi' f ⋙ Pi.eval C i = f i :=
 #align category_theory.functor.pi'_eval CategoryTheory.Functor.pi'_eval
 
 /-- Two functors to a product category are equal iff they agree on every coordinate. -/
-theorem pi_ext (f f' : A ⥤ ∀ i, C i) (h : ∀ i, f ⋙ (Pi.eval C i) = f' ⋙ (Pi.eval C i))
-    : f = f' := by
+theorem pi_ext (f f' : A ⥤ ∀ i, C i) (h : ∀ i, f ⋙ (Pi.eval C i) = f' ⋙ (Pi.eval C i)) :
+    f = f' := by
   apply Functor.ext; rotate_left
   · intro X
     ext i

diff --git a/Mathlib/CategoryTheory/Sigma/Basic.lean b/Mathlib/CategoryTheory/Sigma/Basic.lean
@@ -58,8 +58,7 @@ lemma comp_def (i : I) (X Y Z : C i) (f : X ⟶ Y) (g : Y ⟶ Z) : comp (mk f) (
   rfl
 #align category_theory.sigma.sigma_hom.comp_def CategoryTheory.Sigma.SigmaHom.comp_def
 
-lemma assoc
-  : ∀ {X Y Z W : Σi, C i} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W), (f ≫ g) ≫ h = f ≫ g ≫ h
+lemma assoc : ∀ {X Y Z W : Σi, C i} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W), (f ≫ g) ≫ h = f ≫ g ≫ h
   | _, _, _, _, mk _, mk _, mk _ => congr_arg mk (Category.assoc _ _ _)
 #align category_theory.sigma.sigma_hom.assoc CategoryTheory.Sigma.SigmaHom.assoc
 

diff --git a/Mathlib/CategoryTheory/Simple.lean b/Mathlib/CategoryTheory/Simple.lean
@@ -162,8 +162,8 @@ theorem simple_of_cosimple (X : C) (h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso
 
 /-- A nonzero epimorphism from a simple object is an isomorphism. -/
 theorem isIso_of_epi_of_nonzero {X Y : C} [Simple X] {f : X ⟶ Y} [Epi f] (w : f ≠ 0) : IsIso f :=
-  haveI-- `f ≠ 0` means that `kernel.ι f` is not an iso, and hence zero, and hence `f` is a mono.
-   : Mono f :=
+  -- `f ≠ 0` means that `kernel.ι f` is not an iso, and hence zero, and hence `f` is a mono.
+  haveI : Mono f :=
     Preadditive.mono_of_kernel_zero (mono_to_simple_zero_of_not_iso (kernel_not_iso_of_nonzero w))
   isIso_of_mono_of_epi f
 #align category_theory.is_iso_of_epi_of_nonzero CategoryTheory.isIso_of_epi_of_nonzero

diff --git a/Mathlib/CategoryTheory/Yoneda.lean b/Mathlib/CategoryTheory/Yoneda.lean
@@ -485,8 +485,8 @@ def curriedYonedaLemma {C : Type u₁} [SmallCategory C] :
 
 /-- The curried version of yoneda lemma when `C` is small. -/
 def curriedYonedaLemma' {C : Type u₁} [SmallCategory C] :
-    yoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op ≅ 𝟭 (Cᵒᵖ ⥤ Type u₁)
-    := by
+    yoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op
+      ≅ 𝟭 (Cᵒᵖ ⥤ Type u₁) := by
   refine eqToIso ?_ ≪≫ curry.mapIso (isoWhiskerLeft (Prod.swap _ _)
     (yonedaLemma C ≪≫ isoWhiskerLeft (evaluationUncurried Cᵒᵖ (Type u₁)) uliftFunctorTrivial :_))
     ≪≫ eqToIso ?_

diff --git a/Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean b/Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean
@@ -95,8 +95,8 @@ variable [Fintype α]
 
 /-- **Harris-Kleitman inequality**: Any two lower sets of finsets correlate. -/
 theorem IsLowerSet.le_card_inter_finset (h𝒜 : IsLowerSet (𝒜 : Set (Finset α)))
-    (hℬ : IsLowerSet (ℬ : Set (Finset α))) : 𝒜.card * ℬ.card ≤ 2 ^ Fintype.card α * (𝒜 ∩ ℬ).card
-    := h𝒜.le_card_inter_finset' hℬ (fun _ _ => subset_univ _) fun _ _ => subset_univ _
+    (hℬ : IsLowerSet (ℬ : Set (Finset α))) : 𝒜.card * ℬ.card ≤ 2 ^ Fintype.card α * (𝒜 ∩ ℬ).card :=
+h𝒜.le_card_inter_finset' hℬ (fun _ _ => subset_univ _) fun _ _ => subset_univ _
 #align is_lower_set.le_card_inter_finset IsLowerSet.le_card_inter_finset
 
 /-- **Harris-Kleitman inequality**: Upper sets and lower sets of finsets anticorrelate. -/

diff --git a/Mathlib/Computability/TMToPartrec.lean b/Mathlib/Computability/TMToPartrec.lean
@@ -312,8 +312,8 @@ theorem exists_code {n} {f : Vector ℕ n →. ℕ} (hf : Nat.Partrec' f) :
         show ∀ x, pure x = [x] from fun _ => rfl, Bind.bind, Functor.map]
     suffices ∀ a b, a + b = n →
       (n.succ :: 0 ::
-        g (n ::ᵥ Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail)
-          :: v.val.tail : List ℕ) ∈
+        g (n ::ᵥ Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) ::
+            v.val.tail : List ℕ) ∈
         PFun.fix
           (fun v : List ℕ => Part.bind (cg.eval (v.headI :: v.tail.tail))
             (fun x => Part.some (if v.tail.headI = 0

diff --git a/Mathlib/Data/Finmap.lean b/Mathlib/Data/Finmap.lean
@@ -477,8 +477,8 @@ def insert (a : α) (b : β a) (s : Finmap β) : Finmap β :=
 #align finmap.insert Finmap.insert
 
 @[simp]
-theorem insert_toFinmap (a : α) (b : β a) (s : AList β)
-  : insert a b (AList.toFinmap s) = AList.toFinmap (s.insert a b) := by
+theorem insert_toFinmap (a : α) (b : β a) (s : AList β) :
+    insert a b (AList.toFinmap s) = AList.toFinmap (s.insert a b) := by
   simp [insert]
 #align finmap.insert_to_finmap Finmap.insert_toFinmap
 
@@ -571,8 +571,8 @@ theorem mem_union {a} {s₁ s₂ : Finmap β} : a ∈ s₁ ∪ s₂ ↔ a ∈ s
 #align finmap.mem_union Finmap.mem_union
 
 @[simp]
-theorem union_toFinmap (s₁ s₂ : AList β)
-  : (toFinmap s₁) ∪ (toFinmap s₂) = toFinmap (s₁ ∪ s₂) := by simp [(· ∪ ·), union]
+theorem union_toFinmap (s₁ s₂ : AList β) : (toFinmap s₁) ∪ (toFinmap s₂) = toFinmap (s₁ ∪ s₂) := by
+  simp [(· ∪ ·), union]
 #align finmap.union_to_finmap Finmap.union_toFinmap
 
 theorem keys_union {s₁ s₂ : Finmap β} : (s₁ ∪ s₂).keys = s₁.keys ∪ s₂.keys :=

diff --git a/Mathlib/Data/List/Defs.lean b/Mathlib/Data/List/Defs.lean
@@ -449,8 +449,8 @@ def mapDiagM' {m} [Monad m] {α} (f : α → α → m Unit) : List α → m Unit
 /-- Map each element of a `List` to an action, evaluate these actions in order,
     and collect the results.
 -/
-protected def traverse {F : Type u → Type v} [Applicative F] {α β : Type _} (f : α → F β)
-    : List α → F (List β)
+protected def traverse {F : Type u → Type v} [Applicative F] {α β : Type _} (f : α → F β) :
+    List α → F (List β)
   | [] => pure []
   | x :: xs => List.cons <$> f x <*> List.traverse f xs
 #align list.traverse List.traverse

diff --git a/Mathlib/Data/List/Nodup.lean b/Mathlib/Data/List/Nodup.lean
@@ -435,8 +435,8 @@ theorem Nodup.pairwise_of_set_pairwise {l : List α} {r : α → α → Prop} (h
 #align list.nodup.pairwise_of_set_pairwise List.Nodup.pairwise_of_set_pairwise
 
 @[simp]
-theorem Nodup.pairwise_coe [IsSymm α r] (hl : l.Nodup)
-    : { a | a ∈ l }.Pairwise r ↔ l.Pairwise r := by
+theorem Nodup.pairwise_coe [IsSymm α r] (hl : l.Nodup) :
+    { a | a ∈ l }.Pairwise r ↔ l.Pairwise r := by
   induction' l with a l ih
   · simp
   rw [List.nodup_cons] at hl

diff --git a/Mathlib/Data/PFunctor/Multivariate/M.lean b/Mathlib/Data/PFunctor/Multivariate/M.lean
@@ -149,8 +149,8 @@ def M.corecContents {α : TypeVec.{u} n}
                     (g₂ : ∀ b : β, P.last.B (g₀ b) → β)
                     (x : _)
                     (b : β)
-                    (h: x = M.corecShape P g₀ g₂ b)
-                    : M.Path P x ⟹ α
+                    (h: x = M.corecShape P g₀ g₂ b) :
+                    M.Path P x ⟹ α
   | _, M.Path.root x a f h' i c =>
     have : a = g₀ b := by
       rw [h, M.corecShape, PFunctor.M.dest_corec] at h'

diff --git a/Mathlib/Data/TypeVec.lean b/Mathlib/Data/TypeVec.lean
@@ -248,8 +248,7 @@ theorem appendFun_comp_splitFun {α γ : TypeVec n} {β δ : Type*} {ε : TypeVe
           (g₀ : last ε → β)
           (g₁ : β → δ) :
    appendFun f₁ g₁ ⊚ splitFun f₀ g₀
-      = splitFun (α' := γ.append1 δ) (f₁ ⊚ f₀) (g₁ ∘ g₀)
-  :=
+      = splitFun (α' := γ.append1 δ) (f₁ ⊚ f₀) (g₁ ∘ g₀) :=
   (splitFun_comp _ _ _ _).symm
 #align typevec.append_fun_comp_split_fun TypeVec.appendFun_comp_splitFun
 
@@ -306,8 +305,8 @@ instance subsingleton0 : Subsingleton (TypeVec 0) :=
 -- Porting note: `simp` attribute `TypeVec` moved to file `Tactic/Attr/Register.lean`
 
 /-- cases distinction for 0-length type vector -/
-protected def casesNil {β : TypeVec 0 → Sort*} (f : β Fin2.elim0) : ∀ v, β v
-  := fun v => cast (by congr; funext i; cases i) f
+protected def casesNil {β : TypeVec 0 → Sort*} (f : β Fin2.elim0) : ∀ v, β v :=
+  fun v => cast (by congr; funext i; cases i) f
 #align typevec.cases_nil TypeVec.casesNil
 
 /-- cases distinction for (n+1)-length type vector -/

diff --git a/Mathlib/Geometry/Euclidean/MongePoint.lean b/Mathlib/Geometry/Euclidean/MongePoint.lean
@@ -73,8 +73,8 @@ the intersection of the Monge planes, where a Monge plane is the
 simplex that passes through the centroid of an (n-2)-dimensional face
 and is orthogonal to the opposite edge (in 2 dimensions, this is the
 same as an altitude).  The circumcenter O, centroid G and Monge point
-M are collinear in that order on the Euler line, with OG : GM = (n-1)
-: 2.  Here, we use that ratio to define the Monge point (so resulting
+M are collinear in that order on the Euler line, with OG : GM = (n-1): 2.
+Here, we use that ratio to define the Monge point (so resulting
 in a point that equals the centroid in 0 or 1 dimensions), and then
 show in subsequent lemmas that the point so defined lies in the Monge
 planes and is their unique point of intersection. -/

diff --git a/Mathlib/GroupTheory/Nilpotent.lean b/Mathlib/GroupTheory/Nilpotent.lean
@@ -294,8 +294,8 @@ theorem lowerCentralSeries_one : lowerCentralSeries G 1 = commutator G := rfl
 
 theorem mem_lowerCentralSeries_succ_iff (n : ℕ) (q : G) :
     q ∈ lowerCentralSeries G (n + 1) ↔
-    q ∈ closure { x | ∃ p ∈ lowerCentralSeries G n, ∃ q ∈ (⊤ : Subgroup G), p * q * p⁻¹ * q⁻¹ = x }
-  := Iff.rfl
+    q ∈ closure { x | ∃ p ∈ lowerCentralSeries G n,
+                        ∃ q ∈ (⊤ : Subgroup G), p * q * p⁻¹ * q⁻¹ = x } := Iff.rfl
 #align mem_lower_central_series_succ_iff mem_lowerCentralSeries_succ_iff
 
 theorem lowerCentralSeries_succ (n : ℕ) :