chore(AlgebraicTopology): fix whitespace (leanprover-community#33177)

Found by extending the commandStart linter to proof bodies.

Author: harahu

Mathlib/AlgebraicTopology/DoldKan/Projections.lean

@@ -52,7 +52,7 @@ noncomputable def P : ℕ → (K[X] ⟶ K[X])
   | q + 1 => P q ≫ (𝟙 _ + Hσ q)
 
 lemma P_zero : (P 0 : K[X] ⟶ K[X]) = 𝟙 _ := rfl
-lemma P_succ (q : ℕ) : (P (q+1) : K[X] ⟶ K[X]) = P q ≫ (𝟙 _ + Hσ q) := rfl
+lemma P_succ (q : ℕ) : (P (q + 1) : K[X] ⟶ K[X]) = P q ≫ (𝟙 _ + Hσ q) := rfl
 
 /-- All the `P q` coincide with `𝟙 _` in degree 0. -/
 @[simp]

Mathlib/AlgebraicTopology/Quasicategory/Basic.lean

@@ -37,9 +37,9 @@ every map of simplicial sets `σ₀ : Λ[n, i] → S` can be extended to a map `
 -/
 @[kerodon 003A]
 class Quasicategory (S : SSet) : Prop where
-  hornFilling' : ∀ ⦃n : ℕ⦄ ⦃i : Fin (n+3)⦄ (σ₀ : (Λ[n+2, i] : SSet) ⟶ S)
-    (_h0 : 0 < i) (_hn : i < Fin.last (n+2)),
-      ∃ σ : Δ[n+2] ⟶ S, σ₀ = Λ[n + 2, i].ι ≫ σ
+  hornFilling' : ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : (Λ[n + 2, i] : SSet) ⟶ S)
+    (_h0 : 0 < i) (_hn : i < Fin.last (n + 2)),
+      ∃ σ : Δ[n + 2] ⟶ S, σ₀ = Λ[n + 2, i].ι ≫ σ
 
 lemma Quasicategory.hornFilling {S : SSet} [Quasicategory S] ⦃n : ℕ⦄ ⦃i : Fin (n + 1)⦄
     (h0 : 0 < i) (hn : i < Fin.last n)

Mathlib/AlgebraicTopology/SimplicialSet/FiniteProd.lean

@@ -51,7 +51,7 @@ variable (X₁ X₂) in
 lemma hasDimensionLT_prod
     (d₁ d₂ : ℕ) [X₁.HasDimensionLT d₁] [X₂.HasDimensionLT d₂]
     (n : ℕ) (hn : d₁ + d₂ ≤ n + 1 := by lia) :
-    (X₁ ⊗ X₂).HasDimensionLT  n := by
+    (X₁ ⊗ X₂).HasDimensionLT n := by
   rw [← hasDimensionLT_subcomplex_top_iff, ← iSup_subcomplexOfSimplex_prod_eq_top]
   simp only [Subcomplex.ofSimplexProd_eq_range, hasDimensionLT_iSup_iff]
   intro x₁ x₂

Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean

@@ -82,8 +82,8 @@ section
 variable (n : ℕ) (i k : Fin (n + 3))
 
 /-- The (degenerate) subsimplex of `Λ[n+2, i]` concentrated in vertex `k`. -/
-def const (m : SimplexCategoryᵒᵖ) : Λ[n+2, i].obj m :=
-  SSet.yonedaEquiv (X := Λ[n+2, i])
+def const (m : SimplexCategoryᵒᵖ) : Λ[n + 2, i].obj m :=
+  SSet.yonedaEquiv (X := Λ[n + 2, i])
     (SSet.const ⟨stdSimplex.obj₀Equiv.symm k, by simp⟩)
 
 @[simp]
@@ -146,7 +146,7 @@ which is the type of horn that occurs in the horn-filling condition of quasicate
 @[simps]
 def primitiveTriangle {n : ℕ} (i : Fin (n + 4))
     (h₀ : 0 < i) (hₙ : i < Fin.last (n + 3))
-    (k : ℕ) (h : k < n + 2) : (Λ[n+3, i] : SSet.{u}) _⦋2⦌ := by
+    (k : ℕ) (h : k < n + 2) : (Λ[n + 3, i] : SSet.{u}) _⦋2⦌ := by
   refine ⟨stdSimplex.triangle
     (n := n+3) ⟨k, by lia⟩ ⟨k+1, by lia⟩ ⟨k+2, by lia⟩ ?_ ?_, ?_⟩
   · simp only [Fin.mk_le_mk, le_add_iff_nonneg_right, zero_le]