chore: fix some indentation (#24874)

Author: sgouezel

Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean

@@ -217,7 +217,7 @@ theorem continuousAt_rpow (p : ℝ × ℝ) (h : p.1 ≠ 0 ∨ 0 < p.2) :
 @[fun_prop]
 theorem continuousAt_rpow_const (x : ℝ) (q : ℝ) (h : x ≠ 0 ∨ 0 ≤ q) :
     ContinuousAt (fun x : ℝ => x ^ q) x := by
-· rw [le_iff_lt_or_eq, ← or_assoc] at h
+  rw [le_iff_lt_or_eq, ← or_assoc] at h
   obtain h|rfl := h
   · exact (continuousAt_rpow (x, q) h).comp₂ continuousAt_id continuousAt_const
   · simp_rw [rpow_zero]; exact continuousAt_const

Mathlib/Deprecated/Cardinal/Finite.lean

@@ -77,7 +77,7 @@ theorem _root_.Cardinal.natCast_eq_toPartENat_iff {n : ℕ} {c : Cardinal} :
 @[simp]
 theorem _root_.Cardinal.toPartENat_eq_natCast_iff {c : Cardinal} {n : ℕ} :
     Cardinal.toPartENat c = n ↔ c = n := by
-rw [eq_comm, Cardinal.natCast_eq_toPartENat_iff, eq_comm]
+  rw [eq_comm, Cardinal.natCast_eq_toPartENat_iff, eq_comm]
 
 @[simp]
 theorem _root_.Cardinal.natCast_lt_toPartENat_iff {n : ℕ} {c : Cardinal} :

Mathlib/LinearAlgebra/Lagrange.lean

@@ -471,10 +471,10 @@ theorem natDegree_nodal [Nontrivial R] : (nodal s v).natDegree = #s := by
     natDegree_X_sub_C, sum_const, smul_eq_mul, mul_one]
 
 theorem nodal_ne_zero [Nontrivial R] : nodal s v ≠ 0 := by
-rcases s.eq_empty_or_nonempty with (rfl | h)
-· exact one_ne_zero
-· apply ne_zero_of_natDegree_gt (n := 0)
-  simp only [natDegree_nodal, h.card_pos]
+  rcases s.eq_empty_or_nonempty with (rfl | h)
+  · exact one_ne_zero
+  · apply ne_zero_of_natDegree_gt (n := 0)
+    simp only [natDegree_nodal, h.card_pos]
 
 @[simp]
 theorem degree_nodal [Nontrivial R] : (nodal s v).degree = #s := by

Mathlib/Logic/Relation.lean

@@ -482,7 +482,7 @@ theorem TransGen.lift {p : β → β → Prop} {a b : α} (f : α → β) (h : 
 theorem TransGen.lift' {p : β → β → Prop} {a b : α} (f : α → β)
     (h : ∀ a b, r a b → TransGen p (f a) (f b)) (hab : TransGen r a b) :
     TransGen p (f a) (f b) := by
-simpa [transGen_idem] using hab.lift f h
+  simpa [transGen_idem] using hab.lift f h
 
 theorem TransGen.closed {p : α → α → Prop} :
     (∀ a b, r a b → TransGen p a b) → TransGen r a b → TransGen p a b :=