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

@@ -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,41 +475,41 @@ 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`
     {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
   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,

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

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

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
 

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. -/

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

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]

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