style: add missing spaces around colons (#8293)

This is not exhaustive

Mathlib/Algebra/Group/TypeTags.lean

@@ -128,9 +128,9 @@ instance [Finite α] : Finite (Additive α) :=
 instance [Finite α] : Finite (Multiplicative α) :=
   Finite.of_equiv α (by rfl)
 
-instance [h: Infinite α] : Infinite (Additive α) := h
+instance [h : Infinite α] : Infinite (Additive α) := h
 
-instance [h: Infinite α] : Infinite (Multiplicative α) := h
+instance [h : Infinite α] : Infinite (Multiplicative α) := h
 
 instance [h : DecidableEq α] : DecidableEq (Multiplicative α) := h
 

Mathlib/Algebra/Homology/ShortComplex/FunctorEquivalence.lean

@@ -58,7 +58,7 @@ def unitIso : 𝟭 _ ≅ functor J C ⋙ inverse J C :=
 /-- The counit isomorphism of the equivalence
 `ShortComplex.functorEquivalence : ShortComplex (J ⥤ C) ≌ J ⥤ ShortComplex C`. -/
 @[simps!]
-def counitIso : inverse J C ⋙ functor J C ≅ 𝟭 _:=
+def counitIso : inverse J C ⋙ functor J C ≅ 𝟭 _ :=
   NatIso.ofComponents (fun _ => NatIso.ofComponents
     (fun _ => isoMk (Iso.refl _) (Iso.refl _) (Iso.refl _)
       (by aesop_cat) (by aesop_cat)) (by aesop_cat)) (by aesop_cat)

Mathlib/Algebra/PUnitInstances.lean

@@ -23,7 +23,7 @@ set_option autoImplicit true
 namespace PUnit
 
 @[to_additive]
-instance commGroup: CommGroup PUnit where
+instance commGroup : CommGroup PUnit where
   mul _ _ := unit
   one := unit
   inv _ := unit
@@ -69,7 +69,7 @@ theorem inv_eq : x⁻¹ = unit :=
 #align punit.inv_eq PUnit.inv_eq
 #align punit.neg_eq PUnit.neg_eq
 
-instance commRing: CommRing PUnit where
+instance commRing : CommRing PUnit where
   __ := PUnit.commGroup
   __ := PUnit.addCommGroup
   left_distrib := by intros; rfl
@@ -78,10 +78,10 @@ instance commRing: CommRing PUnit where
   mul_zero := by intros; rfl
   natCast _ := unit
 
-instance cancelCommMonoidWithZero: CancelCommMonoidWithZero PUnit := by
+instance cancelCommMonoidWithZero : CancelCommMonoidWithZero PUnit := by
   refine' { PUnit.commRing with .. }; intros; exact Subsingleton.elim _ _
 
-instance normalizedGCDMonoid: NormalizedGCDMonoid PUnit where
+instance normalizedGCDMonoid : NormalizedGCDMonoid PUnit where
   gcd _ _ := unit
   lcm _ _ := unit
   normUnit _ := 1
@@ -112,14 +112,14 @@ theorem norm_unit_eq {x : PUnit} : normUnit x = 1 :=
   rfl
 #align punit.norm_unit_eq PUnit.norm_unit_eq
 
-instance canonicallyOrderedAddCommMonoid: CanonicallyOrderedAddCommMonoid PUnit := by
+instance canonicallyOrderedAddCommMonoid : CanonicallyOrderedAddCommMonoid PUnit := by
   refine'
     { PUnit.commRing, PUnit.completeBooleanAlgebra with
       exists_add_of_le := fun {_ _} _ => ⟨unit, Subsingleton.elim _ _⟩.. } <;>
     intros <;>
     trivial
 
-instance linearOrderedCancelAddCommMonoid: LinearOrderedCancelAddCommMonoid PUnit where
+instance linearOrderedCancelAddCommMonoid : LinearOrderedCancelAddCommMonoid PUnit where
   __ := PUnit.canonicallyOrderedAddCommMonoid
   __ := PUnit.linearOrder
   le_of_add_le_add_left _ _ _ _ := trivial

Mathlib/Analysis/NormedSpace/lpSpace.lean

@@ -14,7 +14,7 @@ import Mathlib.Topology.Algebra.Order.LiminfLimsup
 # ℓp space
 
 This file describes properties of elements `f` of a pi-type `∀ i, E i` with finite "norm",
-defined for `p:ℝ≥0∞` as the size of the support of `f` if `p=0`, `(∑' a, ‖f a‖^p) ^ (1/p)` for
+defined for `p : ℝ≥0∞` as the size of the support of `f` if `p=0`, `(∑' a, ‖f a‖^p) ^ (1/p)` for
 `0 < p < ∞` and `⨆ a, ‖f a‖` for `p=∞`.
 
 The Prop-valued `Memℓp f p` states that a function `f : ∀ i, E i` has finite norm according

Mathlib/CategoryTheory/Monad/Monadicity.lean

@@ -296,7 +296,7 @@ class PreservesColimitOfIsSplitPair (G : D ⥤ C) where
 instance {A B} (f g : A ⟶ B) [G.IsSplitPair f g] [PreservesColimitOfIsSplitPair G] :
     PreservesColimit (parallelPair f g) G := PreservesColimitOfIsSplitPair.out f g
 
-instance [PreservesColimitOfIsSplitPair G] : ∀ (A: Algebra (toMonad (ofRightAdjoint G))),
+instance [PreservesColimitOfIsSplitPair G] : ∀ (A : Algebra (toMonad (ofRightAdjoint G))),
    PreservesColimit (parallelPair ((leftAdjoint G).map A.a)
       (NatTrans.app (Adjunction.ofRightAdjoint G).counit ((leftAdjoint G).obj A.A))) G :=
   fun _ => PreservesColimitOfIsSplitPair.out _ _
@@ -309,7 +309,7 @@ class ReflectsColimitOfIsSplitPair (G : D ⥤ C) where
 instance {A B} (f g : A ⟶ B) [G.IsSplitPair f g] [ReflectsColimitOfIsSplitPair G] :
     ReflectsColimit (parallelPair f g) G := ReflectsColimitOfIsSplitPair.out f g
 
-instance [ReflectsColimitOfIsSplitPair G] : ∀ (A: Algebra (toMonad (ofRightAdjoint G))),
+instance [ReflectsColimitOfIsSplitPair G] : ∀ (A : Algebra (toMonad (ofRightAdjoint G))),
     ReflectsColimit (parallelPair ((leftAdjoint G).map A.a)
       (NatTrans.app (Adjunction.ofRightAdjoint G).counit ((leftAdjoint G).obj A.A))) G :=
   fun _ => ReflectsColimitOfIsSplitPair.out _ _
@@ -359,7 +359,7 @@ class CreatesColimitOfIsSplitPair (G : D ⥤ C) where
 instance {A B} (f g : A ⟶ B) [G.IsSplitPair f g] [CreatesColimitOfIsSplitPair G] :
     CreatesColimit (parallelPair f g) G := CreatesColimitOfIsSplitPair.out f g
 
-instance [CreatesColimitOfIsSplitPair G] : ∀ (A: Algebra (toMonad (ofRightAdjoint G))),
+instance [CreatesColimitOfIsSplitPair G] : ∀ (A : Algebra (toMonad (ofRightAdjoint G))),
     CreatesColimit (parallelPair ((leftAdjoint G).map A.a)
       (NatTrans.app (Adjunction.ofRightAdjoint G).counit ((leftAdjoint G).obj A.A))) G :=
   fun _ => CreatesColimitOfIsSplitPair.out _ _

Mathlib/CategoryTheory/Monoidal/Category.lean

@@ -213,7 +213,7 @@ theorem whisker_exchange {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) :
   simp [← id_tensorHom, ← tensorHom_id, ← tensor_comp]
 
 @[reassoc]
-theorem tensorHom_def' {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g: X₂ ⟶ Y₂) :
+theorem tensorHom_def' {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :
     f ⊗ g = X₁ ◁ g ≫ f ▷ Y₂ :=
   whisker_exchange f g ▸ tensorHom_def f g
 

Mathlib/Combinatorics/Partition.lean

@@ -66,7 +66,7 @@ structure Partition (n : ℕ) where
 
 namespace Partition
 
-instance decidableEqParition: DecidableEq (Partition n)
+instance decidableEqParition : DecidableEq (Partition n)
   | p, q => by simp [Partition.ext_iff]; exact decidableEq p.parts q.parts
 
 /-- A composition induces a partition (just convert the list to a multiset). -/

Mathlib/Data/List/MinMax.lean

@@ -387,7 +387,7 @@ theorem maximum_le_of_forall_le {b : WithBot α} (h : ∀ a ∈ l, a ≤ b) : l.
     exact ⟨h a (by simp), ih fun a w => h a (mem_cons.mpr (Or.inr w))⟩
 
 theorem le_minimum_of_forall_le {b : WithTop α} (h : ∀ a ∈ l, b ≤ a) : b ≤ l.minimum :=
-  maximum_le_of_forall_le (α:= αᵒᵈ) h
+  maximum_le_of_forall_le (α := αᵒᵈ) h
 
 theorem maximum_eq_coe_iff : maximum l = m ↔ m ∈ l ∧ ∀ a ∈ l, a ≤ m := by
   rw [maximum, ← WithBot.some_eq_coe, argmax_eq_some_iff]

Mathlib/Data/Nat/Digits.lean

@@ -463,7 +463,7 @@ theorem ofDigits_monotone {p q : ℕ} (L : List ℕ) (h : p ≤ q) : ofDigits p
   · simp only [ofDigits, cast_id, add_le_add_iff_left]
     exact Nat.mul_le_mul h hi
 
-theorem sum_le_ofDigits (L : List ℕ) (h: 1 ≤ p) : L.sum ≤ ofDigits p L :=
+theorem sum_le_ofDigits (L : List ℕ) (h : 1 ≤ p) : L.sum ≤ ofDigits p L :=
   (ofDigits_one L).symm ▸ ofDigits_monotone L h
 
 theorem digit_sum_le (p n : ℕ) : List.sum (digits p n) ≤ n := by

Mathlib/Data/Nat/PartENat.lean

@@ -210,7 +210,7 @@ theorem get_one (h : (1 : PartENat).Dom) : (1 : PartENat).get h = 1 :=
 
 -- See note [no_index around OfNat.ofNat]
 @[simp]
-theorem get_ofNat' (x : ℕ) [x.AtLeastTwo] (h : (no_index (OfNat.ofNat x: PartENat)).Dom) :
+theorem get_ofNat' (x : ℕ) [x.AtLeastTwo] (h : (no_index (OfNat.ofNat x : PartENat)).Dom) :
     Part.get (no_index (OfNat.ofNat x : PartENat)) h = (no_index (OfNat.ofNat x)) :=
   get_natCast' x h
 

Mathlib/Data/Ordmap/Ordnode.lean

@@ -348,7 +348,7 @@ def Any (P : α → Prop) : Ordnode α → Prop
   | node _ l x r => Any P l ∨ P x ∨ Any P r
 #align ordnode.any Ordnode.Any
 
-instance Any.decidable {P : α → Prop} : (t: Ordnode α ) → [DecidablePred P] → Decidable (Any P t)
+instance Any.decidable {P : α → Prop} : (t : Ordnode α ) → [DecidablePred P] → Decidable (Any P t)
   | nil => decidableFalse
   | node _ l _ r =>
     have : Decidable (Any P l) := Any.decidable l

Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean

@@ -387,7 +387,7 @@ theorem liftR_map {α β : TypeVec n} {F' : TypeVec n → Type u} [MvFunctor F']
 
 open Function
 
-theorem liftR_map_last [lawful: LawfulMvFunctor F]
+theorem liftR_map_last [lawful : LawfulMvFunctor F]
     {α : TypeVec n} {ι ι'} (R : ι' → ι' → Prop)
     (x : F (α ::: ι)) (f g : ι → ι') (hh : ∀ x : ι, R (f x) (g x)) :
     LiftR' (RelLast' _ R) ((id ::: f) <$$> x) ((id ::: g) <$$> x) :=

Mathlib/Geometry/Manifold/Algebra/SmoothFunctions.lean

@@ -141,7 +141,7 @@ def restrictMonoidHom (G : Type*) [Monoid G] [TopologicalSpace G] [ChartedSpace
     [SmoothMul I' G] {U V : Opens N} (h : U ≤ V) : C^∞⟮I, V; I', G⟯ →* C^∞⟮I, U; I', G⟯ where
   toFun f := ⟨f ∘ Set.inclusion h, f.smooth.comp (smooth_inclusion h)⟩
   map_one' := rfl
-  map_mul' _ _:= rfl
+  map_mul' _ _ := rfl
 #align smooth_map.restrict_monoid_hom SmoothMap.restrictMonoidHom
 #align smooth_map.restrict_add_monoid_hom SmoothMap.restrictAddMonoidHom
 

Mathlib/Init/Algebra/Classes.lean

@@ -420,7 +420,7 @@ theorem not_lt_of_equiv' {a b : α} : a ≈ b → ¬b ≺ a := fun h => h.2
 instance isEquiv : IsEquiv α (@Equiv _ r) where
   refl := erefl
   trans _ _ _ := etrans
-  symm _ _:= esymm
+  symm _ _ := esymm
 #align strict_weak_order.is_equiv StrictWeakOrder.isEquiv
 
 end

Mathlib/Order/Basic.lean

@@ -1371,7 +1371,7 @@ namespace PUnit
 
 variable (a b : PUnit.{u + 1})
 
-instance linearOrder: LinearOrder PUnit where
+instance linearOrder : LinearOrder PUnit where
   le  := fun _ _ ↦ True
   lt  := fun _ _ ↦ False
   max := fun _ _ ↦ unit

Mathlib/RingTheory/Derivation/Lie.lean

@@ -52,7 +52,7 @@ instance : LieRing (Derivation R A A) where
   lie_self d := by ext a; simp only [commutator_apply, add_apply, map_add]; ring_nf; simp
   leibniz_lie d e f := by ext a; simp only [commutator_apply, add_apply, sub_apply, map_sub]; ring
 
-instance instLieAlgebra: LieAlgebra R (Derivation R A A) :=
+instance instLieAlgebra : LieAlgebra R (Derivation R A A) :=
   { Derivation.instModule with
     lie_smul := fun r d e => by
       ext a; simp only [commutator_apply, map_smul, smul_sub, smul_apply] }

Mathlib/RingTheory/Flat.lean

@@ -174,7 +174,7 @@ instance directSum (ι : Type v) (M : ι → Type w) [(i : ι) → AddCommGroup
     · subst j; simp
     · simp [h₂]
   intro a ha; rw [DirectSum.ext_iff R]; intro i
-  have f := LinearMap.congr_arg (f:= (π i)) ha
+  have f := LinearMap.congr_arg (f := (π i)) ha
   erw [LinearMap.congr_fun (h₁ i) a] at f
   rw [(map_zero (π i) : (π i) 0 = (0 : M i))] at f
   have h₂ := (F i)

Mathlib/RingTheory/PowerSeries/Derivative.lean

@@ -56,7 +56,7 @@ theorem derivativeFun_C (r : R) : derivativeFun (C R r) = 0 := by
   rw [coeff_derivativeFun, coeff_succ_C, zero_mul, map_zero]
 
 theorem trunc_derivativeFun (f : R⟦X⟧) (n : ℕ) :
-    trunc n f.derivativeFun = derivative (trunc (n + 1) f):= by
+    trunc n f.derivativeFun = derivative (trunc (n + 1) f) := by
   ext d
   rw [coeff_trunc]
   split_ifs with h

Mathlib/RingTheory/TensorProduct.lean

@@ -860,7 +860,7 @@ theorem map_tmul (f : A →ₐ[S] B) (g : C →ₐ[R] D) (a : A) (c : C) : map f
 #align algebra.tensor_product.map_tmul Algebra.TensorProduct.map_tmul
 
 @[simp]
-theorem map_id : map (.id S A) (.id R C) = .id S _:=
+theorem map_id : map (.id S A) (.id R C) = .id S _ :=
   ext (AlgHom.ext fun _ => rfl) (AlgHom.ext fun _ => rfl)
 
 theorem map_comp (f₂ : B →ₐ[S] C) (f₁ : A →ₐ[S] B) (g₂ : E →ₐ[R] F) (g₁ : D →ₐ[R] E) :

Mathlib/SetTheory/Ordinal/NaturalOps.lean

@@ -58,9 +58,9 @@ def NatOrdinal : Type _ :=
   Ordinal deriving Zero, Inhabited, One, WellFoundedRelation
 #align nat_ordinal NatOrdinal
 
-instance NatOrdinal.linearOrder: LinearOrder NatOrdinal := {Ordinal.linearOrder with}
+instance NatOrdinal.linearOrder : LinearOrder NatOrdinal := {Ordinal.linearOrder with}
 
-instance NatOrdinal.succOrder: SuccOrder NatOrdinal := {Ordinal.succOrder with}
+instance NatOrdinal.succOrder : SuccOrder NatOrdinal := {Ordinal.succOrder with}
 
 /-- The identity function between `Ordinal` and `NatOrdinal`. -/
 @[match_pattern]

Mathlib/Tactic/Linarith/Preprocessing.lean

@@ -121,7 +121,7 @@ partial def isNatProp (e : Expr) : Bool :=
 
 
 /-- If `e` is of the form `((n : ℕ) : C)`, `isNatCoe e` returns `⟨n, C⟩`. -/
-def isNatCoe (e: Expr) : Option (Expr × Expr) :=
+def isNatCoe (e : Expr) : Option (Expr × Expr) :=
   match e.getAppFnArgs with
   | (``Nat.cast, #[target, _, n]) => some ⟨n, target⟩
   | _ => none

Mathlib/Topology/Category/Profinite/Nobeling.lean

@@ -803,7 +803,7 @@ instance {α : Type*} [TopologicalSpace α] [Inhabited α] : Nontrivial (Locally
   apply @zero_ne_one ℤ
   exact FunLike.congr_fun h default
 
-theorem Products.isGood_nil : Products.isGood ({fun _ ↦ false} : Set (I → Bool)) Products.nil:= by
+theorem Products.isGood_nil : Products.isGood ({fun _ ↦ false} : Set (I → Bool)) Products.nil := by
   intro h
   simp only [Products.lt_nil_empty, Products.eval, List.map, List.prod_nil, Set.image_empty,
     Submodule.span_empty, Submodule.mem_bot, one_ne_zero] at h

Mathlib/Topology/LocallyConstant/Algebra.lean

@@ -380,7 +380,7 @@ def comapRingHom [Semiring Z] (f : X → Y) (hf : Continuous f) :
 /-- `LocallyConstant.comap` as an `AlgHom` -/
 @[simps!]
 noncomputable
-def comapₐ (R: Type*) [CommSemiring R] [Semiring Z] [Algebra R Z]
+def comapₐ (R : Type*) [CommSemiring R] [Semiring Z] [Algebra R Z]
     (f : X → Y) (hf : Continuous f) : LocallyConstant Y Z →ₐ[R] LocallyConstant X Z where
   toRingHom := comapRingHom f hf
   commutes' r := by ext x; simp [hf]
@@ -401,7 +401,7 @@ def congrLeftMulEquiv [Mul Z] (e : X ≃ₜ Y) :
 /-- `LocallyConstant.congrLeft` as a linear equivalence. -/
 @[simps!]
 noncomputable
-def congrLeftₗ (R: Type*) [Semiring R] [AddCommMonoid Z] [Module R Z] (e : X ≃ₜ Y) :
+def congrLeftₗ (R : Type*) [Semiring R] [AddCommMonoid Z] [Module R Z] (e : X ≃ₜ Y) :
     LocallyConstant X Z ≃ₗ[R] LocallyConstant Y Z where
   toLinearMap := comapₗ R _ e.symm.continuous
   __ := congrLeft e
@@ -418,7 +418,7 @@ def congrLeftRingEquiv [Semiring Z] (e : X ≃ₜ Y) :
 /-- `LocallyConstant.congrLeft` as an `AlgEquiv`. -/
 @[simps!]
 noncomputable
-def congrLeftₐ (R: Type*) [CommSemiring R] [Semiring Z] [Algebra R Z] (e : X ≃ₜ Y) :
+def congrLeftₐ (R : Type*) [CommSemiring R] [Semiring Z] [Algebra R Z] (e : X ≃ₜ Y) :
     LocallyConstant X Z ≃ₐ[R] LocallyConstant Y Z where
   toEquiv := congrLeft e
   __ := comapₐ R _ e.symm.continuous