From a2a45bc713796526a2aa748e5b524559d422ae83 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 1 Mar 2024 17:22:50 +0000
Subject: [PATCH] chore: rename induction principle arguments around
 `CliffordAlgebra` (#10908)

In order to improve the ergonomics of the `induction` tactic, this renames the arguments of:
* `ExteriorAlgebra.induction`
* `TensorAlgebra.induction`
* `CliffordAlgebra.induction`
* `CliffordAlgebra.left_induction`
* `CliffordAlgebra.right_induction`
* `CliffordAlgebra.even_induction`
* `CliffordAlgebra.odd_induction`
* `Submodule.iSup_induction'`
* `Submodule.pow_induction_on_left'`
* `Submodule.pow_induction_on_right'`

This is slightly awkward for name-resolution within these induction principles, as the argument names end up clashing with the function they are about. Thankfully, this pain is not transferred to the caller using `induction _ using _`.
---
 Mathlib/Algebra/Algebra/Operations.lean       | 33 +++----
 .../InnerProductSpace/Projection.lean         |  6 +-
 .../LinearAlgebra/CliffordAlgebra/Basic.lean  | 15 +--
 .../CliffordAlgebra/Conjugation.lean          | 22 +++--
 .../LinearAlgebra/CliffordAlgebra/Equivs.lean | 32 +++----
 .../LinearAlgebra/CliffordAlgebra/Even.lean   | 16 ++--
 .../CliffordAlgebra/EvenEquiv.lean            |  8 +-
 .../LinearAlgebra/CliffordAlgebra/Fold.lean   | 42 +++++----
 .../CliffordAlgebra/Grading.lean              | 91 +++++++++----------
 .../LinearAlgebra/CliffordAlgebra/Prod.lean   | 24 ++---
 .../LinearAlgebra/ExteriorAlgebra/Basic.lean  |  6 +-
 .../ExteriorAlgebra/Grading.lean              |  6 +-
 Mathlib/LinearAlgebra/Span.lean               | 10 +-
 .../LinearAlgebra/TensorAlgebra/Basic.lean    | 12 +--
 .../LinearAlgebra/TensorAlgebra/Grading.lean  |  6 +-
 15 files changed, 167 insertions(+), 162 deletions(-)

diff --git a/Mathlib/Algebra/Algebra/Operations.lean b/Mathlib/Algebra/Algebra/Operations.lean
index 9d140b53613bb..0aa597fa1843c 100644
--- a/Mathlib/Algebra/Algebra/Operations.lean
+++ b/Mathlib/Algebra/Algebra/Operations.lean
@@ -187,13 +187,14 @@ protected theorem mul_induction_on {C : A → Prop} {r : A} (hr : r ∈ M * N)
 /-- A dependent version of `mul_induction_on`. -/
 @[elab_as_elim]
 protected theorem mul_induction_on' {C : ∀ r, r ∈ M * N → Prop}
-    (hm : ∀ m (hm : m ∈ M) n (hn : n ∈ N), C (m * n) (mul_mem_mul hm hn))
-    (ha : ∀ x hx y hy, C x hx → C y hy → C (x + y) (add_mem hx hy)) {r : A} (hr : r ∈ M * N) :
+    (mem_mul_mem : ∀ m (hm : m ∈ M) n (hn : n ∈ N), C (m * n) (mul_mem_mul hm hn))
+    (add : ∀ x hx y hy, C x hx → C y hy → C (x + y) (add_mem hx hy)) {r : A} (hr : r ∈ M * N) :
     C r hr := by
   refine' Exists.elim _ fun (hr : r ∈ M * N) (hc : C r hr) => hc
   exact
-    Submodule.mul_induction_on hr (fun x hx y hy => ⟨_, hm _ hx _ hy⟩) fun x y ⟨_, hx⟩ ⟨_, hy⟩ =>
-      ⟨_, ha _ _ _ _ hx hy⟩
+    Submodule.mul_induction_on hr
+      (fun x hx y hy => ⟨_, mem_mul_mem _ hx _ hy⟩)
+      fun x y ⟨_, hx⟩ ⟨_, hy⟩ => ⟨_, add _ _ _ _ hx hy⟩
 #align submodule.mul_induction_on' Submodule.mul_induction_on'
 
 variable (R)
@@ -474,27 +475,27 @@ theorem le_pow_toAddSubmonoid {n : ℕ} : M.toAddSubmonoid ^ n ≤ (M ^ n).toAdd
 /-- Dependent version of `Submodule.pow_induction_on_left`. -/
 @[elab_as_elim]
 protected theorem pow_induction_on_left' {C : ∀ (n : ℕ) (x), x ∈ M ^ n → Prop}
-    (hr : ∀ r : R, C 0 (algebraMap _ _ r) (algebraMap_mem r))
-    (hadd : ∀ x y i hx hy, C i x hx → C i y hy → C i (x + y) (add_mem ‹_› ‹_›))
-    (hmul : ∀ m (hm : m ∈ M), ∀ (i x hx), C i x hx → C i.succ (m * x) (mul_mem_mul hm hx))
+    (algebraMap : ∀ r : R, C 0 (algebraMap _ _ r) (algebraMap_mem r))
+    (add : ∀ x y i hx hy, C i x hx → C i y hy → C i (x + y) (add_mem ‹_› ‹_›))
+    (mem_mul : ∀ m (hm : m ∈ M), ∀ (i x hx), C i x hx → C i.succ (m * x) (mul_mem_mul hm hx))
     -- porting note: swapped argument order to match order of `C`
     {n : ℕ} {x : A}
     (hx : x ∈ M ^ n) : C n x hx := by
   induction' n with n n_ih generalizing x
   · rw [pow_zero] at hx
     obtain ⟨r, rfl⟩ := hx
-    exact hr r
+    exact algebraMap r
   exact
-    Submodule.mul_induction_on' (fun m hm x ih => hmul _ hm _ _ _ (n_ih ih))
-      (fun x hx y hy Cx Cy => hadd _ _ _ _ _ Cx Cy) hx
+    Submodule.mul_induction_on' (fun m hm x ih => mem_mul _ hm _ _ _ (n_ih ih))
+      (fun x hx y hy Cx Cy => add _ _ _ _ _ Cx Cy) hx
 #align submodule.pow_induction_on_left' Submodule.pow_induction_on_left'
 
 /-- Dependent version of `Submodule.pow_induction_on_right`. -/
 @[elab_as_elim]
 protected theorem pow_induction_on_right' {C : ∀ (n : ℕ) (x), x ∈ M ^ n → Prop}
-    (hr : ∀ r : R, C 0 (algebraMap _ _ r) (algebraMap_mem r))
-    (hadd : ∀ x y i hx hy, C i x hx → C i y hy → C i (x + y) (add_mem ‹_› ‹_›))
-    (hmul :
+    (algebraMap : ∀ r : R, C 0 (algebraMap _ _ r) (algebraMap_mem r))
+    (add : ∀ x y i hx hy, C i x hx → C i y hy → C i (x + y) (add_mem ‹_› ‹_›))
+    (mul_mem :
       ∀ i x hx, C i x hx →
         ∀ m (hm : m ∈ M), C i.succ (x * m) ((pow_succ' M i).symm ▸ mul_mem_mul hx hm))
     -- porting note: swapped argument order to match order of `C`
@@ -502,13 +503,13 @@ protected theorem pow_induction_on_right' {C : ∀ (n : ℕ) (x), x ∈ M ^ n 
   induction' n with n n_ih generalizing x
   · rw [pow_zero] at hx
     obtain ⟨r, rfl⟩ := hx
-    exact hr r
+    exact algebraMap r
   revert hx
   simp_rw [pow_succ']
   intro hx
   exact
-    Submodule.mul_induction_on' (fun m hm x ih => hmul _ _ hm (n_ih _) _ ih)
-      (fun x hx y hy Cx Cy => hadd _ _ _ _ _ Cx Cy) hx
+    Submodule.mul_induction_on' (fun m hm x ih => mul_mem _ _ hm (n_ih _) _ ih)
+      (fun x hx y hy Cx Cy => add _ _ _ _ _ Cx Cy) hx
 #align submodule.pow_induction_on_right' Submodule.pow_induction_on_right'
 
 /-- To show a property on elements of `M ^ n` holds, it suffices to show that it holds for scalars,
diff --git a/Mathlib/Analysis/InnerProductSpace/Projection.lean b/Mathlib/Analysis/InnerProductSpace/Projection.lean
index 2186eb31dfe4e..243e42084fce4 100644
--- a/Mathlib/Analysis/InnerProductSpace/Projection.lean
+++ b/Mathlib/Analysis/InnerProductSpace/Projection.lean
@@ -1301,15 +1301,15 @@ theorem OrthogonalFamily.sum_projection_of_mem_iSup [Fintype ι] {V : ι → Sub
   -- porting note: switch to the better `induction _ using`. Need the primed induction principle,
   -- the unprimed one doesn't work with `induction` (as it isn't as syntactically general)
   induction hx using Submodule.iSup_induction' with
-  | hp i x hx =>
+  | mem i x hx =>
     refine'
       (Finset.sum_eq_single_of_mem i (Finset.mem_univ _) fun j _ hij => _).trans
         (orthogonalProjection_eq_self_iff.mpr hx)
     rw [orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero, Submodule.coe_zero]
     exact hV.isOrtho hij.symm hx
-  | h0 =>
+  | zero =>
     simp_rw [map_zero, Submodule.coe_zero, Finset.sum_const_zero]
-  | hadd x y _ _ hx hy =>
+  | add x y _ _ hx hy =>
     simp_rw [map_add, Submodule.coe_add, Finset.sum_add_distrib]
     exact congr_arg₂ (· + ·) hx hy
 #align orthogonal_family.sum_projection_of_mem_supr OrthogonalFamily.sum_projection_of_mem_iSup
diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
index 6e1019947c3b8..8cc06f79ee058 100644
--- a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
+++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
@@ -207,19 +207,20 @@ See also the stronger `CliffordAlgebra.left_induction` and `CliffordAlgebra.righ
 -/
 @[elab_as_elim]
 theorem induction {C : CliffordAlgebra Q → Prop}
-    (h_grade0 : ∀ r, C (algebraMap R (CliffordAlgebra Q) r)) (h_grade1 : ∀ x, C (ι Q x))
-    (h_mul : ∀ a b, C a → C b → C (a * b)) (h_add : ∀ a b, C a → C b → C (a + b))
+    (algebraMap : ∀ r, C (algebraMap R (CliffordAlgebra Q) r)) (ι : ∀ x, C (ι Q x))
+    (mul : ∀ a b, C a → C b → C (a * b)) (add : ∀ a b, C a → C b → C (a + b))
     (a : CliffordAlgebra Q) : C a := by
   -- the arguments are enough to construct a subalgebra, and a mapping into it from M
   let s : Subalgebra R (CliffordAlgebra Q) :=
     { carrier := C
-      mul_mem' := @h_mul
-      add_mem' := @h_add
-      algebraMap_mem' := h_grade0 }
+      mul_mem' := @mul
+      add_mem' := @add
+      algebraMap_mem' := algebraMap }
   -- porting note: Added `h`. `h` is needed for `of`.
   letI h : AddCommMonoid s := inferInstanceAs (AddCommMonoid (Subalgebra.toSubmodule s))
-  let of : { f : M →ₗ[R] s // ∀ m, f m * f m = algebraMap _ _ (Q m) } :=
-    ⟨(ι Q).codRestrict (Subalgebra.toSubmodule s) h_grade1, fun m => Subtype.eq <| ι_sq_scalar Q m⟩
+  let of : { f : M →ₗ[R] s // ∀ m, f m * f m = _root_.algebraMap _ _ (Q m) } :=
+    ⟨(CliffordAlgebra.ι Q).codRestrict (Subalgebra.toSubmodule s) ι,
+      fun m => Subtype.eq <| ι_sq_scalar Q m⟩
   -- the mapping through the subalgebra is the identity
   have of_id : AlgHom.id R (CliffordAlgebra Q) = s.val.comp (lift Q of) := by
     ext
diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean
index baf99539b5db7..ff5fa68dafdc1 100644
--- a/Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean
+++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean
@@ -157,10 +157,10 @@ theorem reverse_comp_involute :
   ext x
   simp only [LinearMap.comp_apply, AlgHom.toLinearMap_apply]
   induction x using CliffordAlgebra.induction with
-  | h_grade0 => simp
-  | h_grade1 => simp
-  | h_mul a b ha hb => simp only [ha, hb, reverse.map_mul, AlgHom.map_mul]
-  | h_add a b ha hb => simp only [ha, hb, reverse.map_add, AlgHom.map_add]
+  | algebraMap => simp
+  | ι => simp
+  | mul a b ha hb => simp only [ha, hb, reverse.map_mul, AlgHom.map_mul]
+  | add a b ha hb => simp only [ha, hb, reverse.map_add, AlgHom.map_add]
 #align clifford_algebra.reverse_comp_involute CliffordAlgebra.reverse_comp_involute
 
 /-- `CliffordAlgebra.reverse` and `CliffordAlgebra.involute` commute. Note that the composition
@@ -336,18 +336,20 @@ TODO: show that these are `iff`s when `Invertible (2 : R)`.
 
 
 theorem involute_eq_of_mem_even {x : CliffordAlgebra Q} (h : x ∈ evenOdd Q 0) : involute x = x := by
-  refine' even_induction Q (AlgHom.commutes _) _ _ x h
-  · rintro x y _hx _hy ihx ihy
+  induction x, h using even_induction with
+  | algebraMap r => exact AlgHom.commutes _ _
+  | add x y _hx _hy ihx ihy =>
     rw [map_add, ihx, ihy]
-  · intro m₁ m₂ x _hx ihx
+  | ι_mul_ι_mul m₁ m₂ x _hx ihx =>
     rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg]
 #align clifford_algebra.involute_eq_of_mem_even CliffordAlgebra.involute_eq_of_mem_even
 
 theorem involute_eq_of_mem_odd {x : CliffordAlgebra Q} (h : x ∈ evenOdd Q 1) : involute x = -x := by
-  refine' odd_induction Q involute_ι _ _ x h
-  · rintro x y _hx _hy ihx ihy
+  induction x, h using odd_induction with
+  | ι m => exact involute_ι _
+  | add x y _hx _hy ihx ihy =>
     rw [map_add, ihx, ihy, neg_add]
-  · intro m₁ m₂ x _hx ihx
+  | ι_mul_ι_mul m₁ m₂ x _hx ihx =>
     rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg, mul_neg]
 #align clifford_algebra.involute_eq_of_mem_odd CliffordAlgebra.involute_eq_of_mem_odd
 
diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
index f2a70b4f76fc9..8f936d174f584 100644
--- a/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
+++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
@@ -81,19 +81,19 @@ instance : CommRing (CliffordAlgebra (0 : QuadraticForm R Unit)) :=
   { CliffordAlgebra.instRing _ with
     mul_comm := fun x y => by
       induction x using CliffordAlgebra.induction with
-      | h_grade0 r => apply Algebra.commutes
-      | h_grade1 x => simp
-      | h_add x₁ x₂ hx₁ hx₂ => rw [mul_add, add_mul, hx₁, hx₂]
-      | h_mul x₁ x₂ hx₁ hx₂ => rw [mul_assoc, hx₂, ← mul_assoc, hx₁, ← mul_assoc] }
+      | algebraMap r => apply Algebra.commutes
+      | ι x => simp
+      | add x₁ x₂ hx₁ hx₂ => rw [mul_add, add_mul, hx₁, hx₂]
+      | mul x₁ x₂ hx₁ hx₂ => rw [mul_assoc, hx₂, ← mul_assoc, hx₁, ← mul_assoc] }
 
 -- Porting note: Changed `x.reverse` to `reverse (R := R) x`
 theorem reverse_apply (x : CliffordAlgebra (0 : QuadraticForm R Unit)) :
     reverse (R := R) x = x := by
   induction x using CliffordAlgebra.induction with
-  | h_grade0 r => exact reverse.commutes _
-  | h_grade1 x => rw [ι_eq_zero, LinearMap.zero_apply, reverse.map_zero]
-  | h_mul x₁ x₂ hx₁ hx₂ => rw [reverse.map_mul, mul_comm, hx₁, hx₂]
-  | h_add x₁ x₂ hx₁ hx₂ => rw [reverse.map_add, hx₁, hx₂]
+  | algebraMap r => exact reverse.commutes _
+  | ι x => rw [ι_eq_zero, LinearMap.zero_apply, reverse.map_zero]
+  | mul x₁ x₂ hx₁ hx₂ => rw [reverse.map_mul, mul_comm, hx₁, hx₂]
+  | add x₁ x₂ hx₁ hx₂ => rw [reverse.map_add, hx₁, hx₂]
 #align clifford_algebra_ring.reverse_apply CliffordAlgebraRing.reverse_apply
 
 @[simp]
@@ -222,10 +222,10 @@ instance : CommRing (CliffordAlgebra Q) :=
 /-- `reverse` is a no-op over `CliffordAlgebraComplex.Q`. -/
 theorem reverse_apply (x : CliffordAlgebra Q) : reverse (R := ℝ) x = x := by
   induction x using CliffordAlgebra.induction with
-  | h_grade0 r => exact reverse.commutes _
-  | h_grade1 x => rw [reverse_ι]
-  | h_mul x₁ x₂ hx₁ hx₂ => rw [reverse.map_mul, mul_comm, hx₁, hx₂]
-  | h_add x₁ x₂ hx₁ hx₂ => rw [reverse.map_add, hx₁, hx₂]
+  | algebraMap r => exact reverse.commutes _
+  | ι x => rw [reverse_ι]
+  | mul x₁ x₂ hx₁ hx₂ => rw [reverse.map_mul, mul_comm, hx₁, hx₂]
+  | add x₁ x₂ hx₁ hx₂ => rw [reverse.map_add, hx₁, hx₂]
 #align clifford_algebra_complex.reverse_apply CliffordAlgebraComplex.reverse_apply
 
 @[simp]
@@ -312,14 +312,14 @@ theorem toQuaternion_star (c : CliffordAlgebra (Q c₁ c₂)) :
     toQuaternion (star c) = star (toQuaternion c) := by
   simp only [CliffordAlgebra.star_def']
   induction c using CliffordAlgebra.induction with
-  | h_grade0 r =>
+  | algebraMap r =>
     simp only [reverse.commutes, AlgHom.commutes, QuaternionAlgebra.coe_algebraMap,
       QuaternionAlgebra.star_coe]
-  | h_grade1 x =>
+  | ι x =>
     rw [reverse_ι, involute_ι, toQuaternion_ι, AlgHom.map_neg, toQuaternion_ι,
       QuaternionAlgebra.neg_mk, star_mk, neg_zero]
-  | h_mul x₁ x₂ hx₁ hx₂ => simp only [reverse.map_mul, AlgHom.map_mul, hx₁, hx₂, star_mul]
-  | h_add x₁ x₂ hx₁ hx₂ => simp only [reverse.map_add, AlgHom.map_add, hx₁, hx₂, star_add]
+  | mul x₁ x₂ hx₁ hx₂ => simp only [reverse.map_mul, AlgHom.map_mul, hx₁, hx₂, star_mul]
+  | add x₁ x₂ hx₁ hx₂ => simp only [reverse.map_add, AlgHom.map_add, hx₁, hx₂, star_add]
 #align clifford_algebra_quaternion.to_quaternion_star CliffordAlgebraQuaternion.toQuaternion_star
 
 /-- Map a quaternion into the clifford algebra. -/
diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Even.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Even.lean
index 5fab686be191f..489d7b361ad37 100644
--- a/Mathlib/LinearAlgebra/CliffordAlgebra/Even.lean
+++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Even.lean
@@ -119,13 +119,13 @@ theorem even.algHom_ext ⦃f g : even Q →ₐ[R] A⦄ (h : (even.ι Q).compr₂
     f = g := by
   rw [EvenHom.ext_iff] at h
   ext ⟨x, hx⟩
-  refine' even_induction _ _ _ _ _ hx
-  · intro r
+  induction x, hx using even_induction with
+  | algebraMap r =>
     exact (f.commutes r).trans (g.commutes r).symm
-  · intro x y hx hy ihx ihy
+  | add x y hx hy ihx ihy =>
     have := congr_arg₂ (· + ·) ihx ihy
     exact (f.map_add _ _).trans (this.trans <| (g.map_add _ _).symm)
-  · intro m₁ m₂ x hx ih
+  | ι_mul_ι_mul m₁ m₂ x hx ih =>
     have := congr_arg₂ (· * ·) (LinearMap.congr_fun (LinearMap.congr_fun h m₁) m₂) ih
     exact (f.map_mul _ _).trans (this.trans <| (g.map_mul _ _).symm)
 #align clifford_algebra.even.alg_hom_ext CliffordAlgebra.even.algHom_ext
@@ -234,14 +234,14 @@ theorem aux_mul (x y : even Q) : aux f (x * y) = aux f x * aux f y := by
   cases y
   refine' (congr_arg Prod.fst (foldr_mul _ _ _ _ _ _)).trans _
   dsimp only
-  refine' even_induction Q _ _ _ _ x_property
-  · intro r
+  induction x, x_property using even_induction Q with
+  | algebraMap r =>
     rw [foldr_algebraMap, aux_algebraMap]
     exact Algebra.smul_def r _
-  · intro x y hx hy ihx ihy
+  | add x y hx hy ihx ihy =>
     rw [LinearMap.map_add, Prod.fst_add, ihx, ihy, ← add_mul, ← LinearMap.map_add]
     rfl
-  · rintro m₁ m₂ x (hx : x ∈ even Q) ih
+  | ι_mul_ι_mul m₁ m₂ x hx ih =>
     rw [aux_apply, foldr_mul, foldr_mul, foldr_ι, foldr_ι, fst_fFold_fFold, ih, ← mul_assoc,
       Subtype.coe_mk, foldr_mul, foldr_mul, foldr_ι, foldr_ι, fst_fFold_fFold]
     rfl
diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean
index 8a488244fc45b..54a5edb361abf 100644
--- a/Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean
+++ b/Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean
@@ -247,14 +247,14 @@ theorem coe_toEven_reverse_involute (x : CliffordAlgebra Q) :
     ↑(toEven Q (reverse (involute x))) =
       reverse (Q := Q' Q) (toEven Q x : CliffordAlgebra (Q' Q)) := by
   induction x using CliffordAlgebra.induction with
-  | h_grade0 r => simp only [AlgHom.commutes, Subalgebra.coe_algebraMap, reverse.commutes]
-  | h_grade1 m =>
+  | algebraMap r => simp only [AlgHom.commutes, Subalgebra.coe_algebraMap, reverse.commutes]
+  | ι m =>
     -- porting note: added `letI`
     letI : SubtractionMonoid (even (Q' Q)) := AddGroup.toSubtractionMonoid
     simp only [involute_ι, Subalgebra.coe_neg, toEven_ι, reverse.map_mul, reverse_v, reverse_e0,
       reverse_ι, neg_e0_mul_v, map_neg]
-  | h_mul x y hx hy => simp only [map_mul, Subalgebra.coe_mul, reverse.map_mul, hx, hy]
-  | h_add x y hx hy =>
+  | mul x y hx hy => simp only [map_mul, Subalgebra.coe_mul, reverse.map_mul, hx, hy]
+  | add x y hx hy =>
     -- TODO: The `()` around `map_add` are a regression from leanprover/lean4#2478
     rw [map_add, map_add]
     erw [RingHom.map_add, RingHom.map_add]
diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Fold.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Fold.lean
index 2bf1c626a2868..f1b45ae3872e9 100644
--- a/Mathlib/LinearAlgebra/CliffordAlgebra/Fold.lean
+++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Fold.lean
@@ -139,34 +139,36 @@ theorem foldl_prod_map_ι (l : List M) (f : M →ₗ[R] N →ₗ[R] N) (hf) (n :
 
 end Foldl
 
-theorem right_induction {P : CliffordAlgebra Q → Prop} (hr : ∀ r : R, P (algebraMap _ _ r))
-    (h_add : ∀ x y, P x → P y → P (x + y)) (h_ι_mul : ∀ m x, P x → P (x * ι Q m)) : ∀ x, P x := by
+@[elab_as_elim]
+theorem right_induction {P : CliffordAlgebra Q → Prop} (algebraMap : ∀ r : R, P (algebraMap _ _ r))
+    (add : ∀ x y, P x → P y → P (x + y)) (mul_ι : ∀ m x, P x → P (x * ι Q m)) : ∀ x, P x := by
   /- It would be neat if we could prove this via `foldr` like how we prove
     `CliffordAlgebra.induction`, but going via the grading seems easier. -/
   intro x
   have : x ∈ ⊤ := Submodule.mem_top (R := R)
   rw [← iSup_ι_range_eq_top] at this
-  induction this using Submodule.iSup_induction' with -- _ this (fun i x hx => ?_) _ h_add
-  | hp i x hx =>
+  induction this using Submodule.iSup_induction' with
+  | mem i x hx =>
     induction hx using Submodule.pow_induction_on_right' with
-    | hr r => exact hr r
-    | hadd _x _y _i _ _ ihx ihy => exact h_add _ _ ihx ihy
-    | hmul _i x _hx px m hm =>
+    | algebraMap r => exact algebraMap r
+    | add _x _y _i _ _ ihx ihy => exact add _ _ ihx ihy
+    | mul_mem _i x _hx px m hm =>
       obtain ⟨m, rfl⟩ := hm
-      exact h_ι_mul _ _ px
-  | h0 => simpa only [map_zero] using hr 0
-  | hadd _x _y _ _ ihx ihy =>
-    exact h_add _ _ ihx ihy
+      exact mul_ι _ _ px
+  | zero => simpa only [map_zero] using algebraMap 0
+  | add _x _y _ _ ihx ihy =>
+    exact add _ _ ihx ihy
 #align clifford_algebra.right_induction CliffordAlgebra.right_induction
 
-theorem left_induction {P : CliffordAlgebra Q → Prop} (hr : ∀ r : R, P (algebraMap _ _ r))
-    (h_add : ∀ x y, P x → P y → P (x + y)) (h_mul_ι : ∀ x m, P x → P (ι Q m * x)) : ∀ x, P x := by
+@[elab_as_elim]
+theorem left_induction {P : CliffordAlgebra Q → Prop} (algebraMap : ∀ r : R, P (algebraMap _ _ r))
+    (add : ∀ x y, P x → P y → P (x + y)) (ι_mul : ∀ x m, P x → P (ι Q m * x)) : ∀ x, P x := by
   refine' reverse_involutive.surjective.forall.2 _
   intro x
   induction' x using CliffordAlgebra.right_induction with r x y hx hy m x hx
-  · simpa only [reverse.commutes] using hr r
-  · simpa only [map_add] using h_add _ _ hx hy
-  · simpa only [reverse.map_mul, reverse_ι] using h_mul_ι _ _ hx
+  · simpa only [reverse.commutes] using algebraMap r
+  · simpa only [map_add] using add _ _ hx hy
+  · simpa only [reverse.map_mul, reverse_ι] using ι_mul _ _ hx
 #align clifford_algebra.left_induction CliffordAlgebra.left_induction
 
 /-! ### Versions with extra state -/
@@ -229,10 +231,10 @@ theorem foldr'_ι_mul (f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N)
   rw [foldr_mul, foldr_ι, foldr'Aux_apply_apply]
   refine' congr_arg (f m) (Prod.mk.eta.symm.trans _)
   congr 1
-  induction' x using CliffordAlgebra.left_induction with r x y hx hy m x hx
-  · simp_rw [foldr_algebraMap, Prod.smul_mk, Algebra.algebraMap_eq_smul_one]
-  · rw [map_add, Prod.fst_add, hx, hy]
-  · rw [foldr_mul, foldr_ι, foldr'Aux_apply_apply, hx]
+  induction x using CliffordAlgebra.left_induction with
+  | algebraMap r => simp_rw [foldr_algebraMap, Prod.smul_mk, Algebra.algebraMap_eq_smul_one]
+  | add x y hx hy => rw [map_add, Prod.fst_add, hx, hy]
+  | ι_mul m x hx => rw [foldr_mul, foldr_ι, foldr'Aux_apply_apply, hx]
 #align clifford_algebra.foldr'_ι_mul CliffordAlgebra.foldr'_ι_mul
 
 end CliffordAlgebra
diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean
index fa9e619b71dda..9bb33845ec3b3 100644
--- a/Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean
+++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean
@@ -96,30 +96,30 @@ theorem GradedAlgebra.lift_ι_eq (i' : ZMod 2) (x' : evenOdd Q i') :
   cases' x' with x' hx'
   dsimp only [Subtype.coe_mk, DirectSum.lof_eq_of]
   induction hx' using Submodule.iSup_induction' with
-  | hp i x hx =>
+  | mem i x hx =>
     obtain ⟨i, rfl⟩ := i
     -- porting note: `dsimp only [Subtype.coe_mk] at hx` doesn't work, use `change` instead
     change x ∈ LinearMap.range (ι Q) ^ i at hx
     induction hx using Submodule.pow_induction_on_left' with
-    | hr r =>
+    | algebraMap r =>
       rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
-    | hadd x y i hx hy ihx ihy =>
+    | add x y i hx hy ihx ihy =>
       -- Note: in #8386 `map_add` had to be specialized to avoid a timeout
       -- (the definition was already very slow)
       rw [AlgHom.map_add, ihx, ihy, ← AddMonoidHom.map_add]
       rfl
-    | hmul m hm i x hx ih =>
+    | mem_mul m hm i x hx ih =>
       obtain ⟨_, rfl⟩ := hm
       rw [AlgHom.map_mul, ih, lift_ι_apply, GradedAlgebra.ι_apply Q, DirectSum.of_mul_of]
       refine' DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext _ _) <;>
         dsimp only [GradedMonoid.mk, Subtype.coe_mk]
       · rw [Nat.succ_eq_add_one, add_comm, Nat.cast_add, Nat.cast_one]
       rfl
-  | h0 =>
+  | zero =>
     rw [AlgHom.map_zero]
     apply Eq.symm
     apply DFinsupp.single_eq_zero.mpr; rfl
-  | hadd x y hx hy ihx ihy =>
+  | add x y hx hy ihx ihy =>
     rw [AlgHom.map_add, ihx, ihy, ← AddMonoidHom.map_add]; rfl
 #align clifford_algebra.graded_algebra.lift_ι_eq CliffordAlgebra.GradedAlgebra.lift_ι_eq
 
@@ -160,83 +160,82 @@ theorem evenOdd_isCompl : IsCompl (evenOdd Q 0) (evenOdd Q 1) :=
 scalars or vectors (respectively), closed under addition, and under left-multiplication by a pair
 of vectors. -/
 @[elab_as_elim]
-theorem evenOdd_induction (n : ZMod 2) {P : ∀ x, x ∈ evenOdd Q n → Prop}
-    (hr :
-      ∀ (v) (h : v ∈ LinearMap.range (ι Q) ^ n.val),
-        P v (Submodule.mem_iSup_of_mem ⟨n.val, n.nat_cast_zmod_val⟩ h))
-    (hadd : ∀ {x y hx hy}, P x hx → P y hy → P (x + y) (Submodule.add_mem _ hx hy))
-    (hιι_mul :
-      ∀ (m₁ m₂) {x hx},
-        P x hx →
-          P (ι Q m₁ * ι Q m₂ * x)
+theorem evenOdd_induction (n : ZMod 2) {motive : ∀ x, x ∈ evenOdd Q n → Prop}
+    (range_ι_pow : ∀ (v) (h : v ∈ LinearMap.range (ι Q) ^ n.val),
+        motive v (Submodule.mem_iSup_of_mem ⟨n.val, n.nat_cast_zmod_val⟩ h))
+    (add : ∀ x y hx hy, motive x hx → motive y hy → motive (x + y) (Submodule.add_mem _ hx hy))
+    (ι_mul_ι_mul :
+      ∀ m₁ m₂ x hx,
+        motive x hx →
+          motive (ι Q m₁ * ι Q m₂ * x)
             (zero_add n ▸ SetLike.mul_mem_graded (ι_mul_ι_mem_evenOdd_zero Q m₁ m₂) hx))
-    (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) : P x hx := by
-  apply Submodule.iSup_induction' (C := P) _ (hr 0 (Submodule.zero_mem _)) @hadd
+    (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) : motive x hx := by
+  apply Submodule.iSup_induction' (C := motive) _ (range_ι_pow 0 (Submodule.zero_mem _)) add
   refine' Subtype.rec _
   simp_rw [ZMod.nat_coe_zmod_eq_iff, add_comm n.val]
   rintro n' ⟨k, rfl⟩ xv
   simp_rw [pow_add, pow_mul]
   intro hxv
   induction hxv using Submodule.mul_induction_on' with
-  | hm a ha b hb =>
+  | mem_mul_mem a ha b hb =>
     induction ha using Submodule.pow_induction_on_left' with
-    | hr r =>
+    | algebraMap r =>
       simp_rw [← Algebra.smul_def]
-      exact hr _ (Submodule.smul_mem _ _ hb)
-    | hadd x y n hx hy ihx ihy =>
+      exact range_ι_pow _ (Submodule.smul_mem _ _ hb)
+    | add x y n hx hy ihx ihy =>
       simp_rw [add_mul]
-      apply hadd ihx ihy
-    | hmul x hx n'' y hy ihy =>
+      apply add _ _ _ _ ihx ihy
+    | mem_mul x hx n'' y hy ihy =>
       revert hx
       simp_rw [pow_two]
       intro hx2
       induction hx2 using Submodule.mul_induction_on' with
-      | hm m hm n hn =>
+      | mem_mul_mem m hm n hn =>
         simp_rw [LinearMap.mem_range] at hm hn
         obtain ⟨m₁, rfl⟩ := hm; obtain ⟨m₂, rfl⟩ := hn
         simp_rw [mul_assoc _ y b]
-        exact hιι_mul _ _ ihy
-      | ha x hx y hy ihx ihy =>
+        exact ι_mul_ι_mul _ _ _ _ ihy
+      | add x hx y hy ihx ihy =>
         simp_rw [add_mul]
-        apply hadd ihx ihy
-  | ha x y hx hy ihx ihy =>
-    apply hadd ihx ihy
+        apply add _ _ _ _ ihx ihy
+  | add x y hx hy ihx ihy =>
+    apply add _ _ _ _ ihx ihy
 #align clifford_algebra.even_odd_induction CliffordAlgebra.evenOdd_induction
 
 /-- To show a property is true on the even parts, it suffices to show it is true on the
 scalars, closed under addition, and under left-multiplication by a pair of vectors. -/
 @[elab_as_elim]
-theorem even_induction {P : ∀ x, x ∈ evenOdd Q 0 → Prop}
-    (hr : ∀ r : R, P (algebraMap _ _ r) (SetLike.algebraMap_mem_graded _ _))
-    (hadd : ∀ {x y hx hy}, P x hx → P y hy → P (x + y) (Submodule.add_mem _ hx hy))
-    (hιι_mul :
-      ∀ (m₁ m₂) {x hx},
-        P x hx →
-          P (ι Q m₁ * ι Q m₂ * x)
+theorem even_induction {motive : ∀ x, x ∈ evenOdd Q 0 → Prop}
+    (algebraMap : ∀ r : R, motive (algebraMap _ _ r) (SetLike.algebraMap_mem_graded _ _))
+    (add : ∀ x y hx hy, motive x hx → motive y hy → motive (x + y) (Submodule.add_mem _ hx hy))
+    (ι_mul_ι_mul :
+      ∀ m₁ m₂ x hx,
+        motive x hx →
+          motive (ι Q m₁ * ι Q m₂ * x)
             (zero_add (0 : ZMod 2) ▸ SetLike.mul_mem_graded (ι_mul_ι_mem_evenOdd_zero Q m₁ m₂) hx))
-    (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 0) : P x hx := by
-  refine' evenOdd_induction Q 0 (fun rx => _) (@hadd) hιι_mul x hx
+    (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 0) : motive x hx := by
+  refine' evenOdd_induction Q 0 (fun rx => _) (@add) ι_mul_ι_mul x hx
   rintro ⟨r, rfl⟩
-  exact hr r
+  exact algebraMap r
 #align clifford_algebra.even_induction CliffordAlgebra.even_induction
 
 /-- To show a property is true on the odd parts, it suffices to show it is true on the
 vectors, closed under addition, and under left-multiplication by a pair of vectors. -/
 @[elab_as_elim]
 theorem odd_induction {P : ∀ x, x ∈ evenOdd Q 1 → Prop}
-    (hι : ∀ v, P (ι Q v) (ι_mem_evenOdd_one _ _))
-    (hadd : ∀ {x y hx hy}, P x hx → P y hy → P (x + y) (Submodule.add_mem _ hx hy))
-    (hιι_mul :
-      ∀ (m₁ m₂) {x hx},
+    (ι : ∀ v, P (ι Q v) (ι_mem_evenOdd_one _ _))
+    (add : ∀ x y hx hy, P x hx → P y hy → P (x + y) (Submodule.add_mem _ hx hy))
+    (ι_mul_ι_mul :
+      ∀ m₁ m₂ x hx,
         P x hx →
-          P (ι Q m₁ * ι Q m₂ * x)
+          P (CliffordAlgebra.ι Q m₁ * CliffordAlgebra.ι Q m₂ * x)
             (zero_add (1 : ZMod 2) ▸ SetLike.mul_mem_graded (ι_mul_ι_mem_evenOdd_zero Q m₁ m₂) hx))
     (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1) : P x hx := by
-  refine' evenOdd_induction Q 1 (fun ιv => _) (@hadd) hιι_mul x hx
+  refine' evenOdd_induction Q 1 (fun ιv => _) (@add) ι_mul_ι_mul x hx
   -- porting note: was `simp_rw [ZMod.val_one, pow_one]`, lean4#1926
   intro h; rw [ZMod.val_one, pow_one] at h; revert h
   rintro ⟨v, rfl⟩
-  exact hι v
+  exact ι v
 #align clifford_algebra.odd_induction CliffordAlgebra.odd_induction
 
 end CliffordAlgebra
diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean
index 75c83bcf76b3f..38f92c4323cd8 100644
--- a/Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean
+++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean
@@ -53,17 +53,17 @@ nonrec theorem map_mul_map_of_isOrtho_of_mem_evenOdd
   -- the strategy; for each variable, induct on powers of `ι`, then on the exponent of each
   -- power.
   induction hm₁ using Submodule.iSup_induction' with
-  | h0 => rw [map_zero, zero_mul, mul_zero, smul_zero]
-  | hadd _ _ _ _ ihx ihy => rw [map_add, add_mul, mul_add, ihx, ihy, smul_add]
-  | hp i₁' m₁' hm₁ =>
+  | zero => rw [map_zero, zero_mul, mul_zero, smul_zero]
+  | add _ _ _ _ ihx ihy => rw [map_add, add_mul, mul_add, ihx, ihy, smul_add]
+  | mem i₁' m₁' hm₁ =>
     obtain ⟨i₁n, rfl⟩ := i₁'
     dsimp only at *
     induction hm₁ using Submodule.pow_induction_on_left' with
-    | hr =>
+    | algebraMap =>
       rw [AlgHom.commutes, Nat.cast_zero, mul_zero, uzpow_zero, one_smul, Algebra.commutes]
-    | hadd _ _ _ _ _ ihx ihy =>
+    | add _ _ _ _ _ ihx ihy =>
       rw [map_add, add_mul, mul_add, ihx, ihy, smul_add]
-    | hmul m₁ hm₁ i x₁ _hx₁ ih₁ =>
+    | mem_mul m₁ hm₁ i x₁ _hx₁ ih₁ =>
       obtain ⟨v₁, rfl⟩ := hm₁
       -- this is the first interesting goal
       rw [map_mul, mul_assoc, ih₁, mul_smul_comm, map_apply_ι, Nat.cast_succ, mul_add_one,
@@ -71,18 +71,18 @@ nonrec theorem map_mul_map_of_isOrtho_of_mem_evenOdd
       clear ih₁
       congr 2
       induction hm₂ using Submodule.iSup_induction' with
-      | h0 => rw [map_zero, zero_mul, mul_zero, smul_zero]
-      | hadd _ _ _ _ ihx ihy => rw [map_add, add_mul, mul_add, ihx, ihy, smul_add]
-      | hp i₂' m₂' hm₂ =>
+      | zero => rw [map_zero, zero_mul, mul_zero, smul_zero]
+      | add _ _ _ _ ihx ihy => rw [map_add, add_mul, mul_add, ihx, ihy, smul_add]
+      | mem i₂' m₂' hm₂ =>
         clear m₂
         obtain ⟨i₂n, rfl⟩ := i₂'
         dsimp only at *
         induction hm₂ using Submodule.pow_induction_on_left' with
-        | hr =>
+        | algebraMap =>
           rw [AlgHom.commutes, Nat.cast_zero, uzpow_zero, one_smul, Algebra.commutes]
-        | hadd _ _ _ _ _ ihx ihy =>
+        | add _ _ _ _ _ ihx ihy =>
           rw [map_add, add_mul, mul_add, ihx, ihy, smul_add]
-        | hmul m₂ hm₂ i x₂ _hx₂ ih₂ =>
+        | mem_mul m₂ hm₂ i x₂ _hx₂ ih₂ =>
           obtain ⟨v₂, rfl⟩ := hm₂
           -- this is the second interesting goal
           rw [map_mul, map_apply_ι, Nat.cast_succ, ← mul_assoc,
diff --git a/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean b/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
index efc10de6c221b..b6c104ce715ad 100644
--- a/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
+++ b/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
@@ -150,10 +150,10 @@ and is preserved under addition and muliplication, then it holds for all of `Ext
 -/
 @[elab_as_elim]
 theorem induction {C : ExteriorAlgebra R M → Prop}
-    (h_grade0 : ∀ r, C (algebraMap R (ExteriorAlgebra R M) r)) (h_grade1 : ∀ x, C (ι R x))
-    (h_mul : ∀ a b, C a → C b → C (a * b)) (h_add : ∀ a b, C a → C b → C (a + b))
+    (algebraMap : ∀ r, C (algebraMap R (ExteriorAlgebra R M) r)) (ι : ∀ x, C (ι R x))
+    (mul : ∀ a b, C a → C b → C (a * b)) (add : ∀ a b, C a → C b → C (a + b))
     (a : ExteriorAlgebra R M) : C a :=
-  CliffordAlgebra.induction h_grade0 h_grade1 h_mul h_add a
+  CliffordAlgebra.induction algebraMap ι mul add a
 #align exterior_algebra.induction ExteriorAlgebra.induction
 
 /-- The left-inverse of `algebraMap`. -/
diff --git a/Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.lean b/Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.lean
index 7e121c057972b..3a635a476139c 100644
--- a/Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.lean
+++ b/Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.lean
@@ -71,10 +71,10 @@ theorem GradedAlgebra.liftι_eq (i : ℕ) (x : ⋀[R]^i M) :
   --    (fun m hm i x hx ih => ?_) hx
   -- but it created invalid goals
   induction hx using Submodule.pow_induction_on_left' with
-  | hr => simp_rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
+  | algebraMap => simp_rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
   -- FIXME: specialized `map_add` to avoid a (whole-declaration) timeout
-  | hadd _ _ _ _ _ ihx ihy => simp_rw [AlgHom.map_add, ihx, ihy, ← AddMonoidHom.map_add]; rfl
-  | hmul _ hm _ _ _ ih =>
+  | add _ _ _ _ _ ihx ihy => simp_rw [AlgHom.map_add, ihx, ihy, ← AddMonoidHom.map_add]; rfl
+  | mem_mul _ hm _ _ _ ih =>
       obtain ⟨_, rfl⟩ := hm
       simp_rw [AlgHom.map_mul, ih, GradedAlgebra.liftι, lift_ι_apply, GradedAlgebra.ι_apply R M,
         DirectSum.of_mul_of]
diff --git a/Mathlib/LinearAlgebra/Span.lean b/Mathlib/LinearAlgebra/Span.lean
index 04a5adf6f841c..ef4002baa083f 100644
--- a/Mathlib/LinearAlgebra/Span.lean
+++ b/Mathlib/LinearAlgebra/Span.lean
@@ -692,16 +692,16 @@ theorem iSup_induction {ι : Sort*} (p : ι → Submodule R M) {C : M → Prop}
 /-- A dependent version of `submodule.iSup_induction`. -/
 @[elab_as_elim]
 theorem iSup_induction' {ι : Sort*} (p : ι → Submodule R M) {C : ∀ x, (x ∈ ⨆ i, p i) → Prop}
-    (hp : ∀ (i) (x) (hx : x ∈ p i), C x (mem_iSup_of_mem i hx)) (h0 : C 0 (zero_mem _))
-    (hadd : ∀ x y hx hy, C x hx → C y hy → C (x + y) (add_mem ‹_› ‹_›)) {x : M}
+    (mem : ∀ (i) (x) (hx : x ∈ p i), C x (mem_iSup_of_mem i hx)) (zero : C 0 (zero_mem _))
+    (add : ∀ x y hx hy, C x hx → C y hy → C (x + y) (add_mem ‹_› ‹_›)) {x : M}
     (hx : x ∈ ⨆ i, p i) : C x hx := by
   refine' Exists.elim _ fun (hx : x ∈ ⨆ i, p i) (hc : C x hx) => hc
   refine' iSup_induction p (C := fun x : M ↦ ∃ (hx : x ∈ ⨆ i, p i), C x hx) hx
     (fun i x hx => _) _ fun x y => _
-  · exact ⟨_, hp _ _ hx⟩
-  · exact ⟨_, h0⟩
+  · exact ⟨_, mem _ _ hx⟩
+  · exact ⟨_, zero⟩
   · rintro ⟨_, Cx⟩ ⟨_, Cy⟩
-    exact ⟨_, hadd _ _ _ _ Cx Cy⟩
+    exact ⟨_, add _ _ _ _ Cx Cy⟩
 #align submodule.supr_induction' Submodule.iSup_induction'
 
 theorem singleton_span_isCompactElement (x : M) :
diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
index b488a21b59d8b..7b70620a9af77 100644
--- a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
+++ b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
@@ -193,18 +193,18 @@ and is preserved under addition and muliplication, then it holds for all of `Ten
 -/
 @[elab_as_elim]
 theorem induction {C : TensorAlgebra R M → Prop}
-    (h_grade0 : ∀ r, C (algebraMap R (TensorAlgebra R M) r)) (h_grade1 : ∀ x, C (ι R x))
-    (h_mul : ∀ a b, C a → C b → C (a * b)) (h_add : ∀ a b, C a → C b → C (a + b))
+    (algebraMap : ∀ r, C (algebraMap R (TensorAlgebra R M) r)) (ι : ∀ x, C (ι R x))
+    (mul : ∀ a b, C a → C b → C (a * b)) (add : ∀ a b, C a → C b → C (a + b))
     (a : TensorAlgebra R M) : C a := by
   -- the arguments are enough to construct a subalgebra, and a mapping into it from M
   let s : Subalgebra R (TensorAlgebra R M) :=
     { carrier := C
-      mul_mem' := @h_mul
-      add_mem' := @h_add
-      algebraMap_mem' := h_grade0 }
+      mul_mem' := @mul
+      add_mem' := @add
+      algebraMap_mem' := algebraMap }
   -- porting note: Added `h`. `h` is needed for `of`.
   let h : AddCommMonoid s := inferInstanceAs (AddCommMonoid (Subalgebra.toSubmodule s))
-  let of : M →ₗ[R] s := (ι R).codRestrict (Subalgebra.toSubmodule s) h_grade1
+  let of : M →ₗ[R] s := (TensorAlgebra.ι R).codRestrict (Subalgebra.toSubmodule s) ι
   -- the mapping through the subalgebra is the identity
   have of_id : AlgHom.id R (TensorAlgebra R M) = s.val.comp (lift R of) := by
     ext
diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Grading.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Grading.lean
index 5c7dfb1016dad..cf94b7043d986 100644
--- a/Mathlib/LinearAlgebra/TensorAlgebra/Grading.lean
+++ b/Mathlib/LinearAlgebra/TensorAlgebra/Grading.lean
@@ -54,14 +54,14 @@ instance gradedAlgebra :
     dsimp only [Subtype.coe_mk, DirectSum.lof_eq_of]
     -- porting note: use new `induction using` support that failed in Lean 3
     induction hx using Submodule.pow_induction_on_left' with
-    | hr r =>
+    | algebraMap r =>
       rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
-    | hadd x y i hx hy ihx ihy =>
+    | add x y i hx hy ihx ihy =>
       -- Note: #8386 had to specialize `map_add` to avoid a timeout
       -- (the extra typeclass search seems to have pushed this already slow proof over the edge)
       rw [AlgHom.map_add, ihx, ihy, ← AddMonoidHom.map_add]
       rfl
-    | hmul m hm i x hx ih =>
+    | mem_mul m hm i x hx ih =>
       obtain ⟨_, rfl⟩ := hm
       rw [AlgHom.map_mul, ih, lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.of_mul_of]
       exact DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext (add_comm _ _) rfl)