diff --git a/Mathlib/Algebra/FreeMonoid/Basic.lean b/Mathlib/Algebra/FreeMonoid/Basic.lean
index 806fe80a9bcdac..0f591afdb8aa9d 100644
--- a/Mathlib/Algebra/FreeMonoid/Basic.lean
+++ b/Mathlib/Algebra/FreeMonoid/Basic.lean
@@ -232,16 +232,18 @@ end Mem
   /-- Recursor for `FreeAddMonoid` using `0` and
   `FreeAddMonoid.of x + xs` instead of `[]` and `x :: xs`. -/]
 -- Porting note: change from `List.recOn` to `List.rec` since only the latter is computable
-def recOn {C : FreeMonoid α → Sort*} (xs : FreeMonoid α) (h0 : C 1)
-    (ih : ∀ x xs, C xs → C (of x * xs)) : C xs := List.rec h0 ih xs
+def recOn {motive : FreeMonoid α → Sort*} (xs : FreeMonoid α) (one : motive 1)
+    (of_mul : ∀ x xs, motive xs → motive (of x * xs)) : motive xs := List.rec one of_mul xs
 
 @[to_additive (attr := simp)]
-theorem recOn_one {C : FreeMonoid α → Sort*} (h0 : C 1) (ih : ∀ x xs, C xs → C (of x * xs)) :
-    @recOn α C 1 h0 ih = h0 := rfl
+theorem recOn_one {motive : FreeMonoid α → Sort*} (one : motive 1)
+    (of_mul : ∀ x xs, motive xs → motive (of x * xs)) :
+    @recOn α motive 1 one of_mul = one := rfl
 
 @[to_additive (attr := simp)]
-theorem recOn_of_mul {C : FreeMonoid α → Sort*} (x : α) (xs : FreeMonoid α) (h0 : C 1)
-    (ih : ∀ x xs, C xs → C (of x * xs)) : @recOn α C (of x * xs) h0 ih = ih x xs (recOn xs h0 ih) :=
+theorem recOn_of_mul {motive : FreeMonoid α → Sort*} (x : α) (xs : FreeMonoid α) (one : motive 1)
+    (of_mul : ∀ x xs, motive xs → motive (of x * xs)) :
+    @recOn α motive (of x * xs) one of_mul = of_mul x xs (recOn xs one of_mul) :=
   rfl
 
 /-! ### Induction -/
@@ -251,18 +253,19 @@ section induction_principles
 /-- An induction principle on free monoids, with cases for `1`, `FreeMonoid.of` and `*`. -/
 @[to_additive (attr := elab_as_elim, induction_eliminator)
 /-- An induction principle on free monoids, with cases for `0`, `FreeAddMonoid.of` and `+`. -/]
-protected theorem inductionOn {C : FreeMonoid α → Prop} (z : FreeMonoid α) (one : C 1)
-    (of : ∀ (x : α), C (FreeMonoid.of x)) (mul : ∀ (x y : FreeMonoid α), C x → C y → C (x * y)) :
-    C z :=
-  List.rec one (fun _ _ ih => mul [_] _ (of _) ih) z
+protected theorem inductionOn {motive : FreeMonoid α → Prop} (z : FreeMonoid α) (one : motive 1)
+    (of : ∀ (x : α), motive (FreeMonoid.of x))
+    (mul : ∀ (x y : FreeMonoid α), motive x → motive y → motive (x * y)) :
+    motive z :=
+  recOn z one fun x xs ih => mul (.of x) xs (of x) ih
 
 /-- An induction principle for free monoids which mirrors induction on lists, with cases analogous
 to the empty list and cons -/
 @[to_additive (attr := elab_as_elim) /-- An induction principle for free monoids which mirrors
 induction on lists, with cases analogous to the empty list and cons -/]
-protected theorem inductionOn' {p : FreeMonoid α → Prop} (a : FreeMonoid α)
-    (one : p (1 : FreeMonoid α)) (mul_of : ∀ b a, p a → p (of b * a)) : p a :=
-  List.rec one (fun _ _ tail_ih => mul_of _ _ tail_ih) a
+protected theorem inductionOn' {motive : FreeMonoid α → Prop} (a : FreeMonoid α)
+    (one : motive (1 : FreeMonoid α)) (of_mul : ∀ b a, motive a → motive (of b * a)) : motive a :=
+  recOn a one of_mul
 
 end induction_principles
 
@@ -271,16 +274,18 @@ end induction_principles
 @[to_additive (attr := elab_as_elim, cases_eliminator)
   /-- A version of `List.casesOn` for `FreeAddMonoid` using `0` and
   `FreeAddMonoid.of x + xs` instead of `[]` and `x :: xs`. -/]
-def casesOn {C : FreeMonoid α → Sort*} (xs : FreeMonoid α) (h0 : C 1)
-    (ih : ∀ x xs, C (of x * xs)) : C xs := List.casesOn xs h0 ih
+def casesOn {motive : FreeMonoid α → Sort*} (xs : FreeMonoid α) (one : motive 1)
+    (of_mul : ∀ x xs, motive (of x * xs)) : motive xs := List.casesOn xs one of_mul
 
 @[to_additive (attr := simp)]
-theorem casesOn_one {C : FreeMonoid α → Sort*} (h0 : C 1) (ih : ∀ x xs, C (of x * xs)) :
-    @casesOn α C 1 h0 ih = h0 := rfl
+theorem casesOn_one {motive : FreeMonoid α → Sort*} (one : motive 1)
+    (of_mul : ∀ x xs, motive (of x * xs)) :
+    @casesOn α motive 1 one of_mul = one := rfl
 
 @[to_additive (attr := simp)]
-theorem casesOn_of_mul {C : FreeMonoid α → Sort*} (x : α) (xs : FreeMonoid α) (h0 : C 1)
-    (ih : ∀ x xs, C (of x * xs)) : @casesOn α C (of x * xs) h0 ih = ih x xs := rfl
+theorem casesOn_of_mul {motive : FreeMonoid α → Sort*} (x : α) (xs : FreeMonoid α) (one : motive 1)
+    (of_mul : ∀ x xs, motive (of x * xs)) :
+    @casesOn α motive (of x * xs) one of_mul = of_mul x xs := rfl
 
 @[to_additive (attr := ext)]
 theorem hom_eq ⦃f g : FreeMonoid α →* M⦄ (h : ∀ x, f (of x) = g (of x)) : f = g :=
@@ -427,7 +432,7 @@ theorem map_surjective {f : α → β} : Function.Surjective (map f) ↔ Functio
     | one =>
       have H := congr_arg length hb
       simp only [length_one, length_of, Nat.zero_ne_one, map_one] at H
-    | mul_of head _ _ =>
+    | of_mul head _ _ =>
       simp only [map_mul, map_of] at hb
       use head
       have H := congr_arg length hb
@@ -437,7 +442,7 @@ theorem map_surjective {f : α → β} : Function.Surjective (map f) ↔ Functio
   intro fs d
   induction d using FreeMonoid.inductionOn' with
   | one => use 1; rfl
-  | mul_of head tail ih =>
+  | of_mul head tail ih =>
     specialize fs head
     rcases fs with ⟨a, rfl⟩
     rcases ih with ⟨b, rfl⟩
diff --git a/Mathlib/Algebra/Group/Submonoid/Membership.lean b/Mathlib/Algebra/Group/Submonoid/Membership.lean
index e9e109c8842c1a..01e73b2c7a7a47 100644
--- a/Mathlib/Algebra/Group/Submonoid/Membership.lean
+++ b/Mathlib/Algebra/Group/Submonoid/Membership.lean
@@ -277,7 +277,7 @@ theorem closure_induction_left
   obtain ⟨l, rfl⟩ := h
   induction l using FreeMonoid.inductionOn' with
   | one => exact one
-  | mul_of x y ih =>
+  | of_mul x y ih =>
     simp only [map_mul, FreeMonoid.lift_eval_of]
     refine mul_left _ x.prop (FreeMonoid.lift Subtype.val y) _ (ih ?_)
     simp only [closure_eq_mrange, mem_mrange, exists_apply_eq_apply]
diff --git a/Mathlib/GroupTheory/Coprod/Basic.lean b/Mathlib/GroupTheory/Coprod/Basic.lean
index 2cdc9c603dd46e..69f828e4fa76d1 100644
--- a/Mathlib/GroupTheory/Coprod/Basic.lean
+++ b/Mathlib/GroupTheory/Coprod/Basic.lean
@@ -200,7 +200,7 @@ theorem induction_on' {C : M ∗ N → Prop} (m : M ∗ N)
   rcases mk_surjective m with ⟨x, rfl⟩
   induction x using FreeMonoid.inductionOn' with
   | one => exact one
-  | mul_of x xs ih =>
+  | of_mul x xs ih =>
     cases x with
     | inl m => simpa using inl_mul m _ ih
     | inr n => simpa using inr_mul n _ ih
@@ -581,7 +581,7 @@ theorem con_inv_mul_cancel (x : FreeMonoid (G ⊕ H)) :
   rw [← mk_eq_mk, map_mul, map_one]
   induction x using FreeMonoid.inductionOn' with
   | one => simp
-  | mul_of x xs ihx =>
+  | of_mul x xs ihx =>
     simp only [toList_of_mul, map_cons, reverse_cons, ofList_append, map_mul, ofList_singleton]
     rwa [mul_assoc, ← mul_assoc (mk (of _)), mk_of_inv_mul, one_mul]
 
diff --git a/Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean b/Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean
index 405485f74613b9..30f274638e5728 100644
--- a/Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean
+++ b/Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean
@@ -301,7 +301,7 @@ lemma _root_.FreeAddMonoid.toPiTensorProduct (p : FreeAddMonoid (R × Π i, s i)
     List.sum (List.map (fun x ↦ x.1 • ⨂ₜ[R] i, x.2 i) p.toList) := by
   induction p using FreeAddMonoid.inductionOn' with
   | zero => rfl
-  | add_of b a ih =>
+  | of_add b a ih =>
     rw [FreeAddMonoid.toList_of_add, List.map_cons, List.sum_cons, ← ih, ← tprodCoeff_eq_smul_tprod]
     rfl