chore: tidy various files (leanprover-community#33340)

Ruben-VandeVelde · Ruben-VandeVelde · commit c05a1aed8ce5 · 2025-12-27T16:28:50.000Z
diff --git a/Counterexamples/NowhereDifferentiable.lean b/Counterexamples/NowhereDifferentiable.lean
@@ -103,7 +103,7 @@ theorem lt_seq {b : ℝ} (hb : 0 < b) (x : ℝ) (m : ℕ) : x < seq b x m := by
 
 theorem le_seq {b : ℝ} (hb : 0 < b) (x : ℝ) (m : ℕ) : x ≤ seq b x m := (lt_seq hb x m).le
 
-theorem seq_le {b : ℝ} (hb : 0 < b) (x : ℝ) (m : ℕ) : seq b x m ≤ x + (3 / 2) * b⁻¹ ^ m  := by
+theorem seq_le {b : ℝ} (hb : 0 < b) (x : ℝ) (m : ℕ) : seq b x m ≤ x + (3 / 2) * b⁻¹ ^ m := by
   grw [seq, Int.floor_le]
   simp [field]
 
@@ -235,13 +235,13 @@ theorem weierstrass_slope {a : ℝ} (ha : a ∈ Set.Ioo 0 1) {b : ℕ} (hb : Odd
     |seq b x m - x| * ((2 / 3 - π / (a * b - 1)) * (a * b) ^ m) ≤
       |weierstrass a b (seq b x m) - weierstrass a b x| := by
   simp_rw [weierstrass]
-  obtain hsseq := summable_weierstrass ha b (seq b x m)
-  obtain hsx := summable_weierstrass ha b x
-  obtain hsum := hsseq.sub hsx
+  have hsseq := summable_weierstrass ha b (seq b x m)
+  have hsx := summable_weierstrass ha b x
+  have hsum := hsseq.sub hsx
   rw [← hsseq.tsum_sub hsx]
   simp_rw [← mul_sub] at ⊢ hsum
   rw [← hsum.sum_add_tsum_nat_add m]
-  obtain hsum_shift := (summable_nat_add_iff m).mpr hsum
+  have hsum_shift := (summable_nat_add_iff m).mpr hsum
   rw [add_comm]
   refine le_trans ?_ (abs_sub_abs_le_abs_add _ _)
   rw [sub_mul (2 / 3), mul_sub |seq b x m - x|]
@@ -263,7 +263,7 @@ theorem not_differentiableAt_weierstrass
       atTop (𝓝 (f' 1)) := by
     convert (h.lim_real 1).comp (tendsto_seq_sub_inv hb1 x)
     simp
-  obtain h := (continuous_abs.tendsto _).comp this
+  have h := (continuous_abs.tendsto _).comp this
   contrapose! h
   apply not_tendsto_nhds_of_tendsto_atTop
   -- To show the absolute value of slope tends to ∞, it suffices to show its lower bound does.
diff --git a/Mathlib/Algebra/AffineMonoid/Basic.lean b/Mathlib/Algebra/AffineMonoid/Basic.lean
@@ -17,10 +17,10 @@ monoids.
 public section
 
 /-- An affine monoid is a finitely generated cancellative torsion-free commutative monoid. -/
-class abbrev IsAffineAddMonoid(M : Type*)[AddCommMonoid M] : Prop :=
+class abbrev IsAffineAddMonoid (M : Type*) [AddCommMonoid M] : Prop :=
   IsCancelAdd M, AddMonoid.FG M, IsAddTorsionFree M
 
 /-- An affine monoid is a finitely generated cancellative torsion-free commutative monoid. -/
 @[to_additive]
-class abbrev IsAffineMonoid(M : Type*)[CommMonoid M] : Prop :=
+class abbrev IsAffineMonoid (M : Type*) [CommMonoid M] : Prop :=
   IsCancelMul M, Monoid.FG M, IsMulTorsionFree M
diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Pointwise.lean b/Mathlib/Algebra/Algebra/Subalgebra/Pointwise.lean
@@ -25,10 +25,10 @@ section Pointwise
 variable {R : Type*} {A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
 
 theorem mul_toSubmodule_le (S T : Subalgebra R A) :
-    (Subalgebra.toSubmodule S) * (Subalgebra.toSubmodule T) ≤ Subalgebra.toSubmodule (S ⊔ T) := by
+    Subalgebra.toSubmodule S * Subalgebra.toSubmodule T ≤ Subalgebra.toSubmodule (S ⊔ T) := by
   rw [Submodule.mul_le]
   intro y hy z hz
-  change y * z ∈ S ⊔ T
+  simp only [mem_toSubmodule]
   exact mul_mem (Algebra.mem_sup_left hy) (Algebra.mem_sup_right hz)
 
 /-- As submodules, subalgebras are idempotent. -/
diff --git a/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean b/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@@ -522,10 +522,8 @@ theorem prod_bij_ne_one {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ 
 
 @[to_additive]
 theorem exists_ne_one_of_prod_ne_one (h : ∏ x ∈ s, f x ≠ 1) : ∃ a ∈ s, f a ≠ 1 := by
-  classical
-    rw [← prod_filter_ne_one] at h
-    rcases nonempty_of_prod_ne_one h with ⟨x, hx⟩
-    exact ⟨x, (mem_filter.1 hx).1, by simpa using (mem_filter.1 hx).2⟩
+  contrapose! h
+  exact prod_eq_one h
 
 @[to_additive]
 theorem prod_range_succ_comm (f : ℕ → M) (n : ℕ) :
diff --git a/Mathlib/Algebra/Module/LocalizedModule/Basic.lean b/Mathlib/Algebra/Module/LocalizedModule/Basic.lean
@@ -1203,7 +1203,7 @@ lemma map_mk' (h : M →ₗ[R] N) (x) (s : S) :
   rfl
 
 @[simp]
-lemma map_id : map S f f (.id) = .id := by
+lemma map_id : map S f f .id = .id := by
   ext x
   obtain ⟨⟨x, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S f x
   simp
diff --git a/Mathlib/Algebra/Order/Floor/Ring.lean b/Mathlib/Algebra/Order/Floor/Ring.lean
@@ -286,7 +286,7 @@ variable {k : Type*} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [FloorRin
 theorem floor_div_cast_of_nonneg {n : ℤ} (hn : 0 ≤ n) (a : k) : ⌊a / n⌋ = ⌊a⌋ / n := by
   obtain rfl | hn := hn.eq_or_lt
   · simp
-  nth_rw 2 [<- div_mul_cancel₀ (a := a) (ne_of_gt (Int.cast_pos.mpr hn))]
+  nth_rw 2 [← div_mul_cancel₀ (a := a) (ne_of_gt (Int.cast_pos.mpr hn))]
   rw [mul_cast_floor_div_cancel_of_pos hn]
 
 theorem floor_div_natCast (a : k) (n : ℕ) : ⌊a / n⌋ = ⌊a⌋ / n := by
diff --git a/Mathlib/Algebra/Order/Floor/Semifield.lean b/Mathlib/Algebra/Order/Floor/Semifield.lean
@@ -36,7 +36,7 @@ variable [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K]
 theorem floor_div_natCast (a : K) (n : ℕ) : ⌊a / n⌋₊ = ⌊a⌋₊ / n := by
   obtain rfl | hn := n.eq_zero_or_pos
   · simp
-  nth_rw 2 [<- div_mul_cancel₀ (a := a) (b := ↑n) (by positivity)]
+  nth_rw 2 [← div_mul_cancel₀ (a := a) (b := ↑n) (by positivity)]
   rw [mul_cast_floor_div_cancel (Nat.ne_zero_of_lt hn)]
 
 theorem floor_div_ofNat (a : K) (n : ℕ) [n.AtLeastTwo] :
diff --git a/Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean b/Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
@@ -933,7 +933,7 @@ theorem coeff_single_mul_aux (f : SkewMonoidAlgebra k G) {r : k} {x y z : G}
   classical
   have : (f.sum fun a b ↦ ite (x * a = y) (0 * x • b) 0) = 0 := by simp
   calc
-    ((single x r) * f).coeff y =
+    (single x r * f).coeff y =
         sum f fun a b ↦ ite (x * a = y) (r * x • b) 0 :=
       (coeff_mul _ _ _).trans <| sum_single_index this
     _ = f.sum fun a b ↦ ite (a = z) (r * x • b) 0 := by simp [H]
diff --git a/Mathlib/Analysis/MeanInequalities.lean b/Mathlib/Analysis/MeanInequalities.lean
@@ -343,22 +343,22 @@ version for real-valued nonnegative functions. -/
 theorem harm_mean_le_geom_mean_weighted (w z : ι → ℝ) (hs : s.Nonempty) (hw : ∀ i ∈ s, 0 < w i)
     (hw' : ∑ i ∈ s, w i = 1) (hz : ∀ i ∈ s, 0 < z i) :
     (∑ i ∈ s, w i / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ w i := by
-    have : ∏ i ∈ s, (1 / z) i ^ w i ≤ ∑ i ∈ s, w i * (1 / z) i :=
-      geom_mean_le_arith_mean_weighted s w (1 / z) (fun i hi ↦ le_of_lt (hw i hi)) hw'
-      (fun i hi ↦ one_div_nonneg.2 (le_of_lt (hz i hi)))
-    have p_pos : 0 < ∏ i ∈ s, (z i)⁻¹ ^ w i :=
-      prod_pos fun i hi => rpow_pos_of_pos (inv_pos.2 (hz i hi)) _
-    have s_pos : 0 < ∑ i ∈ s, w i * (z i)⁻¹ :=
-      sum_pos (fun i hi => mul_pos (hw i hi) (inv_pos.2 (hz i hi))) hs
-    norm_num at this
-    rw [← inv_le_inv₀ s_pos p_pos] at this
-    apply le_trans this
-    have p_pos₂ : 0 < (∏ i ∈ s, (z i) ^ w i)⁻¹ :=
-      inv_pos.2 (prod_pos fun i hi => rpow_pos_of_pos ((hz i hi)) _)
-    rw [← inv_inv (∏ i ∈ s, z i ^ w i), inv_le_inv₀ p_pos p_pos₂, ← Finset.prod_inv_distrib]
-    gcongr
-    · exact fun i hi ↦ inv_nonneg.mpr (Real.rpow_nonneg (le_of_lt (hz i hi)) _)
-    · rw [Real.inv_rpow]; apply fun i hi ↦ le_of_lt (hz i hi); assumption
+  have : ∏ i ∈ s, (1 / z) i ^ w i ≤ ∑ i ∈ s, w i * (1 / z) i :=
+    geom_mean_le_arith_mean_weighted s w (1 / z) (fun i hi ↦ le_of_lt (hw i hi)) hw'
+    (fun i hi ↦ one_div_nonneg.2 (le_of_lt (hz i hi)))
+  have p_pos : 0 < ∏ i ∈ s, (z i)⁻¹ ^ w i :=
+    prod_pos fun i hi => rpow_pos_of_pos (inv_pos.2 (hz i hi)) _
+  have s_pos : 0 < ∑ i ∈ s, w i * (z i)⁻¹ :=
+    sum_pos (fun i hi => mul_pos (hw i hi) (inv_pos.2 (hz i hi))) hs
+  norm_num at this
+  rw [← inv_le_inv₀ s_pos p_pos] at this
+  apply le_trans this
+  have p_pos₂ : 0 < (∏ i ∈ s, (z i) ^ w i)⁻¹ :=
+    inv_pos.2 (prod_pos fun i hi => rpow_pos_of_pos ((hz i hi)) _)
+  rw [← inv_inv (∏ i ∈ s, z i ^ w i), inv_le_inv₀ p_pos p_pos₂, ← Finset.prod_inv_distrib]
+  gcongr
+  · exact fun i hi ↦ inv_nonneg.mpr (Real.rpow_nonneg (le_of_lt (hz i hi)) _)
+  · rw [Real.inv_rpow]; apply fun i hi ↦ le_of_lt (hz i hi); assumption
 
 
 /-- **HM-GM inequality**: The **harmonic mean is less than or equal to the geometric mean. -/
diff --git a/Mathlib/CategoryTheory/Functor/Derived/PointwiseLeftDerived.lean b/Mathlib/CategoryTheory/Functor/Derived/PointwiseLeftDerived.lean
@@ -19,7 +19,7 @@ We show that if `F : C ⥤ H` inverts `W : MorphismProperty C`,
 then it has a pointwise left derived functor.
 
 Note: this file was obtained by dualizing the definitions in the file
-`Functor.Derived.PointwiseRightDerived`. These two files should be
+`Mathlib/CategoryTheory/Functor/Derived/PointwiseRightDerived.lean`. These two files should be
 kept in sync.
 
 -/
diff --git a/Mathlib/CategoryTheory/Functor/Derived/PointwiseRightDerived.lean b/Mathlib/CategoryTheory/Functor/Derived/PointwiseRightDerived.lean
@@ -18,7 +18,7 @@ of pointwise left Kan extensions.
 We show that if `F : C ⥤ H` inverts `W : MorphismProperty C`,
 then it has a pointwise right derived functor.
 
-Note: the file `Functor.Derived.PointwiseLeftDerived` was obtained
+Note: the file `Mathlib/CategoryTheory/Functor/Derived/PointwiseLeftDerived.lean` was obtained
 by dualizing this file. These two files should be kept in sync.
 
 -/
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean
@@ -209,7 +209,7 @@ def isColimitMapCoconePushoutCoconeEquiv :
 def isColimitPushoutCoconeMapOfIsColimit [PreservesColimit (span f g) G]
     (l : IsColimit (PushoutCocone.mk h k comm)) :
     IsColimit (PushoutCocone.mk (G.map h) (G.map k) (show G.map f ≫ G.map h = G.map g ≫ G.map k
-      from by simp only [← G.map_comp, comm])) :=
+      by simp only [← G.map_comp, comm])) :=
   isColimitMapCoconePushoutCoconeEquiv G comm (isColimitOfPreserves G l)
 
 /-- The property of reflecting pushouts expressed in terms of binary cofans. -/
diff --git a/Mathlib/Combinatorics/SetFamily/Compression/Down.lean b/Mathlib/Combinatorics/SetFamily/Compression/Down.lean
@@ -225,7 +225,7 @@ open FinsetFamily
 /-- `a` is in the down-compressed family iff it's in the original and its compression is in the
 original, or it's not in the original but it's the compression of something in the original. -/
 theorem mem_compression : s ∈ 𝓓 a 𝒜 ↔ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜 := by
-  simp_rw [compression, mem_disjUnion, mem_filter, mem_image, and_comm (a := (s ∉ 𝒜))]
+  simp_rw [compression, mem_disjUnion, mem_filter, mem_image, and_comm (a := s ∉ 𝒜)]
   refine
     or_congr_right
       (and_congr_left fun hs =>
diff --git a/Mathlib/Combinatorics/SimpleGraph/Matching.lean b/Mathlib/Combinatorics/SimpleGraph/Matching.lean
@@ -399,14 +399,14 @@ lemma Walk.IsPath.isCycles_spanningCoe_toSubgraph_sup_edge {u v} {p : G.Walk u v
 lemma Walk.IsCycle.adj_toSubgraph_iff_of_isCycles [LocallyFinite G] {u} {p : G.Walk u u}
     (hp : p.IsCycle) (hcyc : G.IsCycles) (hv : v ∈ p.toSubgraph.verts) :
     ∀ w, p.toSubgraph.Adj v w ↔ G.Adj v w := by
-  refine fun w ↦ Subgraph.adj_iff_of_neighborSet_equiv (?_ : Inhabited _).default (Set.toFinite _)
-  apply Classical.inhabited_of_nonempty
+  refine fun w ↦ Subgraph.adj_iff_of_neighborSet_equiv (?_ : Nonempty _).some (Set.toFinite _)
+  have := hp.ncard_neighborSet_toSubgraph_eq_two (by aesop)
   rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _),
-      ← Set.cast_ncard (finite_neighborSet_toSubgraph p), hcyc
-        (Set.Nonempty.mono (p.toSubgraph.neighborSet_subset v) <|
-          Set.nonempty_of_ncard_ne_zero <| by
-            simp [hp.ncard_neighborSet_toSubgraph_eq_two (by aesop)]),
-      hp.ncard_neighborSet_toSubgraph_eq_two (by simp_all)]
+    ← Set.cast_ncard (finite_neighborSet_toSubgraph p),
+    hcyc
+      (Set.Nonempty.mono (p.toSubgraph.neighborSet_subset v) <|
+        Set.nonempty_of_ncard_ne_zero <| by simp [this]),
+    this]
 
 open scoped symmDiff
 
diff --git a/Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean b/Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean
@@ -216,11 +216,11 @@ lemma eventually_atTop_nonneg_or_nonpos (hf : GrowsPolynomially f) :
         have half_z_to_base : f (1 / 2 * z) = f (max n₀ 2) := by
           refine hyp_ind (1 / 2 * z) ⟨?lb, ?ub⟩
           case lb =>
-            calc max n₀ 2 ≤ ((1 : ℝ) / (2 : ℝ)) * (2 : ℝ) ^ 1 * max n₀ 2 := by simp
-                        _ ≤ ((1 : ℝ) / (2 : ℝ)) * (2 : ℝ) ^ n * max n₀ 2 := by gcongr; norm_num
+            calc max n₀ 2 ≤ (1 / 2 : ℝ) * (2 : ℝ) ^ 1 * max n₀ 2 := by simp
+                        _ ≤ (1 / 2 : ℝ) * (2 : ℝ) ^ n * max n₀ 2 := by gcongr; norm_num
                         _ ≤ _ := by rw [mul_assoc]; gcongr; exact_mod_cast hz.1
           case ub =>
-            have h₁ : (2 : ℝ)^n = ((1 : ℝ) / (2 : ℝ)) * (2 : ℝ)^(n + 1) := by
+            have h₁ : (2 : ℝ) ^ n = (1 / 2 : ℝ) * (2 : ℝ) ^ (n + 1) := by
               rw [one_div, pow_add, pow_one]
               ring
             rw [h₁, mul_assoc]
diff --git a/Mathlib/Data/ZMod/Basic.lean b/Mathlib/Data/ZMod/Basic.lean
@@ -998,9 +998,9 @@ theorem val_cast_of_lt {n : ℕ} {a : ℕ} (h : a < n) : (a : ZMod n).val = a :=
 
 theorem val_cast_zmod_lt {m : ℕ} [NeZero m] (n : ℕ) [NeZero n] (a : ZMod m) :
     (a.cast : ZMod n).val < m := by
-  rcases m with (⟨⟩ | ⟨m⟩); · cases NeZero.ne 0 rfl
+  obtain ⟨m, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero (NeZero.ne m)
   by_cases! h : m < n
-  · rcases n with (⟨⟩ | ⟨n⟩); · simp at h
+  · obtain ⟨n, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero (NeZero.ne n)
     rw [← natCast_val, val_cast_of_lt]
     · apply a.val_lt
     apply lt_of_le_of_lt (Nat.le_of_lt_succ (ZMod.val_lt a)) h
@@ -1020,9 +1020,7 @@ theorem neg_val {n : ℕ} [NeZero n] (a : ZMod n) : (-a).val = if a = 0 then 0 e
   by_cases h : a = 0; · rw [if_pos h, h, val_zero, tsub_zero, Nat.mod_self]
   rw [if_neg h]
   apply Nat.mod_eq_of_lt
-  apply Nat.sub_lt (NeZero.pos n)
-  contrapose! h
-  rwa [Nat.le_zero, val_eq_zero] at h
+  exact Nat.sub_lt (NeZero.pos n) (val_pos.mpr h)
 
 theorem val_neg_of_ne_zero {n : ℕ} [nz : NeZero n] (a : ZMod n) [na : NeZero a] :
     (-a).val = n - a.val := by simp_all [neg_val a, na.out]
@@ -1038,13 +1036,9 @@ theorem val_sub {n : ℕ} [NeZero n] {a b : ZMod n} (h : b.val ≤ a.val) :
 
 theorem val_cast_eq_val_of_lt {m n : ℕ} [nzm : NeZero m] {a : ZMod m}
     (h : a.val < n) : (a.cast : ZMod n).val = a.val := by
-  have nzn : NeZero n := by constructor; rintro rfl; simp at h
-  cases m with
-  | zero => cases nzm; simp_all
-  | succ m =>
-    cases n with
-    | zero => cases nzn; simp_all
-    | succ n => exact Fin.val_cast_of_lt h
+  obtain ⟨m, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero (NeZero.ne m)
+  obtain ⟨n, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero <| by rintro (rfl : n = 0); simp at h
+  exact Fin.val_cast_of_lt h
 
 theorem cast_cast_zmod_of_le {m n : ℕ} [hm : NeZero m] (h : m ≤ n) (a : ZMod m) :
     (cast (cast a : ZMod n) : ZMod m) = a := by
diff --git a/Mathlib/Geometry/Convex/Cone/Basic.lean b/Mathlib/Geometry/Convex/Cone/Basic.lean
@@ -433,11 +433,11 @@ See also (`IsGenerating`). -/
 def IsReproducing [AddCommGroup M] (C : ConvexCone R M) : Prop :=
   (C : Set M) - (C : Set M) = Set.univ
 
-/-- A sufficient criteria for a convex cone `C` to be reproducing is that `Set.univ` is a subset
+/-- A sufficient criterion for a convex cone `C` to be reproducing is that `Set.univ` is a subset
 of `C - C`. -/
 theorem IsReproducing.of_univ_subset [AddCommGroup M] {C : ConvexCone R M}
     (h : Set.univ ⊆ (C : Set M) - (C : Set M)) : C.IsReproducing :=
-  Set.eq_univ_iff_forall.mpr fun _ ↦ h trivial
+  Set.eq_univ_iff_forall.mpr fun _ ↦ h (Set.mem_univ _)
 
 /-- The set difference of a reproducing cone with itself equals `Set.univ`. -/
 lemma IsReproducing.sub_eq_univ [AddCommGroup M] {C : ConvexCone R M} (hC : C.IsReproducing) :
diff --git a/Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean b/Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
@@ -214,7 +214,7 @@ theorem oangle_sign_eq_zero_iff_collinear {p₁ p₂ p₃ : P} :
 
 /-- An oriented angle is not zero and `π` if and only if the three points are not collinear. -/
 theorem oangle_ne_zero_and_ne_pi_iff_not_collinear {p₁ p₂ p₃ : P} :
-  ∡ p₁ p₂ p₃ ≠ 0 ∧ ∡ p₁ p₂ p₃ ≠ π ↔ ¬ Collinear ℝ {p₁, p₂, p₃} := by
+    ∡ p₁ p₂ p₃ ≠ 0 ∧ ∡ p₁ p₂ p₃ ≠ π ↔ ¬ Collinear ℝ {p₁, p₂, p₃} := by
   rw [oangle_ne_zero_and_ne_pi_iff_affineIndependent, affineIndependent_iff_not_collinear_set]
 
 /-- If twice the oriented angles between two triples of points are equal, one triple is affinely
diff --git a/Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean b/Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
@@ -333,8 +333,7 @@ theorem sin_eq_one_iff_angle_eq_pi_div_two : sin (angle x y) = 1 ↔ angle x y =
   rw [← cos_eq_zero_iff_angle_eq_pi_div_two, ← abs_eq_zero, abs_cos_eq_sqrt_one_sub_sin_sq, h]
   simp
 
-/-- If two vectors of equal norms has the angle between them equal to 0, then
-they are equal. -/
+/-- If the angle between two vectors of equal norm is equal to 0, then the vectors are equal. -/
 lemma eq_of_angle_eq_zero_of_norm_eq {x y : V} (hxy : angle x y = 0) (h : ‖x‖ = ‖y‖) : x = y := by
   grind [angle_eq_zero_iff, norm_smul, Real.norm_eq_abs, norm_ne_zero_iff, abs, one_smul]
 
diff --git a/Mathlib/Geometry/Euclidean/Triangle.lean b/Mathlib/Geometry/Euclidean/Triangle.lean
@@ -328,7 +328,7 @@ measures of the remote interior angles. -/
 theorem exterior_angle_eq_angle_add_angle {p₁ p₂ p₃ : P} (p : P) (h : Sbtw ℝ p p₁ p₂) :
     ∠ p₃ p₁ p = ∠ p₁ p₃ p₂ + ∠ p₃ p₂ p₁ := by
   linarith [angle_add_angle_eq_pi_of_angle_eq_pi p₃ h.angle₁₂₃_eq_pi,
-  angle_add_angle_add_angle_eq_pi p₃ h.right_ne.symm, angle_comm p₃ p₁ p₂]
+    angle_add_angle_add_angle_eq_pi p₃ h.right_ne.symm, angle_comm p₃ p₁ p₂]
 
 /-- The **sum of the angles of a triangle** (possibly degenerate, where the triangle is a line),
 oriented angles at point. -/
diff --git a/Mathlib/GroupTheory/QuotientGroup/Basic.lean b/Mathlib/GroupTheory/QuotientGroup/Basic.lean
@@ -270,23 +270,19 @@ noncomputable def quotientInfEquivProdNormalizerQuotient (H N : Subgroup G)
     H ⧸ N.subgroupOf H ≃* (H ⊔ N : Subgroup G) ⧸ N.subgroupOf (H ⊔ N) :=
   letI := Subgroup.normal_subgroupOf_of_le_normalizer hLE
   letI := Subgroup.normal_subgroupOf_sup_of_le_normalizer hLE
-  let
-    φ : -- φ is the natural homomorphism H →* (HN)/N.
-      H →*
-      _ ⧸ N.subgroupOf (H ⊔ N) :=
+  -- φ is the natural homomorphism H →* (HN)/N.
+  let φ : H →* _ ⧸ N.subgroupOf (H ⊔ N) :=
     (mk' <| N.subgroupOf (H ⊔ N)).comp (inclusion le_sup_left)
   have φ_surjective : Surjective φ := fun x =>
     x.inductionOn' <| by
       rintro ⟨y, hy : y ∈ (H ⊔ N)⟩
       rw [← SetLike.mem_coe] at hy
       rw [coe_mul_of_left_le_normalizer_right H N hLE] at hy
       rcases hy with ⟨h, hh, n, hn, rfl⟩
+      simp only [SetLike.mem_coe] at hn
       use ⟨h, hh⟩
       refine Quotient.eq.mpr ?_
-      change leftRel _ _ _
-      rw [leftRel_apply]
-      change h⁻¹ * (h * n) ∈ N
-      rwa [← mul_assoc, inv_mul_cancel, one_mul]
+      simp [leftRel_apply, inclusion, mem_subgroupOf, hn]
   (quotientMulEquivOfEq (by simp [φ, ← comap_ker])).trans
     (quotientKerEquivOfSurjective φ φ_surjective)
 
diff --git a/Mathlib/LinearAlgebra/RootSystem/Defs.lean b/Mathlib/LinearAlgebra/RootSystem/Defs.lean
@@ -148,8 +148,8 @@ variable (ι R M N) in
   invFun P := P.flip
 
 instance [P.IsRootSystem] : P.flip.IsRootSystem where
-    span_root_eq_top := IsRootSystem.span_coroot_eq_top
-    span_coroot_eq_top := IsRootSystem.span_root_eq_top
+  span_root_eq_top := IsRootSystem.span_coroot_eq_top
+  span_coroot_eq_top := IsRootSystem.span_root_eq_top
 
 lemma ne_zero [NeZero (2 : R)] : (P.root i : M) ≠ 0 :=
   fun h ↦ NeZero.ne' (2 : R) <| by simpa [h] using P.root_coroot_two i
diff --git a/Mathlib/LinearAlgebra/Transvection.lean b/Mathlib/LinearAlgebra/Transvection.lean
@@ -92,14 +92,14 @@ theorem eq_id_of_finrank_le_one
     [Free R V] [Module.Finite R V] [StrongRankCondition R]
     {f : Dual R V} {v : V} (hfv : f v = 0) (h1 : finrank R V ≤ 1) :
     transvection f v = LinearMap.id := by
-  let b := finBasis R V
-  rcases (by lia : finrank R V = 0 ∨ finrank R V = 1) with h0 | h1
-  · have : Subsingleton V := (finrank_eq_zero_iff_of_free R V).mp h0
+  interval_cases h : finrank R V
+  · have : Subsingleton V := (finrank_eq_zero_iff_of_free R V).mp h
     simp [Subsingleton.eq_zero v]
-  · ext x
+  · let b := finBasis R V
+    ext x
     suffices f x • v = 0 by
       simp [apply, this]
-    let i : Fin (finrank R V) := ⟨0, by simp [h1]⟩
+    let i : Fin (finrank R V) := ⟨0, by simp [h]⟩
     suffices ∀ x, x = b.repr x i • (b i) by
       rw [this v, map_smul, smul_eq_mul, mul_comm] at hfv
       rw [this x, this v, map_smul, smul_eq_mul, ← mul_smul, mul_assoc, hfv, mul_zero, zero_smul]
diff --git a/Mathlib/MeasureTheory/Measure/Tight.lean b/Mathlib/MeasureTheory/Measure/Tight.lean
diff --git a/Mathlib/NumberTheory/NumberField/House.lean b/Mathlib/NumberTheory/NumberField/House.lean
diff --git a/Mathlib/Probability/Distributions/Gaussian/Real.lean b/Mathlib/Probability/Distributions/Gaussian/Real.lean
diff --git a/Mathlib/Probability/Distributions/SetBernoulli.lean b/Mathlib/Probability/Distributions/SetBernoulli.lean
diff --git a/Mathlib/RepresentationTheory/Homological/GroupCohomology/FiniteCyclic.lean b/Mathlib/RepresentationTheory/Homological/GroupCohomology/FiniteCyclic.lean
diff --git a/Mathlib/Topology/Algebra/UniformField.lean b/Mathlib/Topology/Algebra/UniformField.lean
