chore: add induction_eliminator and cases_eliminator for free objects (#14135)

Namely, for

* `FreeMagma` / `FreeAddMagma`
* `FreeSemigroup` / `FreeAddSemigroup`
* `FreeMonoid` / `FreeAddMonoid`
* `FreeCommRing`
* `FreeAlgebra`

Split from #12605


Co-authored-by: negiizhao <[email protected]>

Author: eric-wieser

Mathlib/Algebra/Free.lean

@@ -72,8 +72,8 @@ attribute [nolint simpNF] FreeAddMagma.add.injEq
 attribute [nolint simpNF] FreeMagma.mul.injEq
 
 /-- Recursor for `FreeMagma` using `x * y` instead of `FreeMagma.mul x y`. -/
-@[to_additive (attr := elab_as_elim) "Recursor for `FreeAddMagma` using `x + y` instead of
-`FreeAddMagma.add x y`."]
+@[to_additive (attr := elab_as_elim, induction_eliminator)
+  "Recursor for `FreeAddMagma` using `x + y` instead of `FreeAddMagma.add x y`."]
 def recOnMul {C : FreeMagma α → Sort l} (x) (ih1 : ∀ x, C (of x))
     (ih2 : ∀ x y, C x → C y → C (x * y)) : C x :=
   FreeMagma.recOn x ih1 ih2
@@ -394,7 +394,7 @@ def of : α →ₙ* AssocQuotient α where toFun := Quot.mk _; map_mul' _x _y :=
 @[to_additive]
 instance [Inhabited α] : Inhabited (AssocQuotient α) := ⟨of default⟩
 
-@[to_additive (attr := elab_as_elim)]
+@[to_additive (attr := elab_as_elim, induction_eliminator)]
 protected theorem induction_on {C : AssocQuotient α → Prop} (x : AssocQuotient α)
     (ih : ∀ x, C (of x)) : C x := Quot.induction_on x ih
 #align magma.assoc_quotient.induction_on Magma.AssocQuotient.induction_on
@@ -517,7 +517,8 @@ theorem length_of (x : α) : (of x).length = 1 := rfl
 instance [Inhabited α] : Inhabited (FreeSemigroup α) := ⟨of default⟩
 
 /-- Recursor for free semigroup using `of` and `*`. -/
-@[to_additive (attr := elab_as_elim) "Recursor for free additive semigroup using `of` and `+`."]
+@[to_additive (attr := elab_as_elim, induction_eliminator)
+  "Recursor for free additive semigroup using `of` and `+`."]
 protected def recOnMul {C : FreeSemigroup α → Sort l} (x) (ih1 : ∀ x, C (of x))
     (ih2 : ∀ x y, C (of x) → C y → C (of x * y)) : C x :=
       FreeSemigroup.recOn x fun f s ↦

Mathlib/Algebra/FreeAlgebra.lean

@@ -563,7 +563,7 @@ namespace FreeAlgebra
 If `C` holds for the `algebraMap` of `r : R` into `FreeAlgebra R X`, the `ι` of `x : X`, and is
 preserved under addition and muliplication, then it holds for all of `FreeAlgebra R X`.
 -/
-@[elab_as_elim]
+@[elab_as_elim, induction_eliminator]
 theorem induction {C : FreeAlgebra R X → Prop}
     (h_grade0 : ∀ r, C (algebraMap R (FreeAlgebra R X) 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))
@@ -591,7 +591,7 @@ theorem induction {C : FreeAlgebra R X → Prop}
 theorem adjoin_range_ι : Algebra.adjoin R (Set.range (ι R : X → FreeAlgebra R X)) = ⊤ := by
   set S := Algebra.adjoin R (Set.range (ι R : X → FreeAlgebra R X))
   refine top_unique fun x hx => ?_; clear hx
-  induction x using FreeAlgebra.induction with
+  induction x with
   | h_grade0 => exact S.algebraMap_mem _
   | h_add x y hx hy => exact S.add_mem hx hy
   | h_mul x y hx hy => exact S.mul_mem hx hy

Mathlib/Algebra/FreeMonoid/Basic.lean

@@ -151,8 +151,9 @@ theorem of_injective : Function.Injective (@of α) := List.singleton_injective
 #align free_add_monoid.of_injective FreeAddMonoid.of_injective
 
 /-- Recursor for `FreeMonoid` using `1` and `FreeMonoid.of x * xs` instead of `[]` and `x :: xs`. -/
-@[to_additive (attr := elab_as_elim) "Recursor for `FreeAddMonoid` using `0` and
-`FreeAddMonoid.of x + xs` instead of `[]` and `x :: xs`."]
+@[to_additive (attr := elab_as_elim, induction_eliminator)
+  "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
@@ -174,8 +175,9 @@ theorem recOn_of_mul {C : FreeMonoid α → Sort*} (x : α) (xs : FreeMonoid α)
 
 /-- A version of `List.cases_on` for `FreeMonoid` using `1` and `FreeMonoid.of x * xs` instead of
 `[]` and `x :: xs`. -/
-@[to_additive (attr := elab_as_elim) "A version of `List.casesOn` for `FreeAddMonoid` using `0` and
-`FreeAddMonoid.of x + xs` instead of `[]` and `x :: xs`."]
+@[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
 #align free_monoid.cases_on FreeMonoid.casesOn

Mathlib/Algebra/Group/Submonoid/Membership.lean

@@ -419,7 +419,7 @@ theorem closure_induction_left {s : Set M} {p : (m : M) → m ∈ closure s →
     p x h := by
   simp_rw [closure_eq_mrange] at h
   obtain ⟨l, rfl⟩ := h
-  induction' l using FreeMonoid.recOn with x y ih
+  induction' l with x y ih
   · exact one
   · simp only [map_mul, FreeMonoid.lift_eval_of]
     refine mul_left _ x.prop (FreeMonoid.lift Subtype.val y) _ (ih ?_)

Mathlib/GroupTheory/Coprod/Basic.lean

@@ -191,7 +191,7 @@ theorem induction_on' {C : M ∗ N → Prop} (m : M ∗ N)
     (inl_mul : ∀ m x, C x → C (inl m * x))
     (inr_mul : ∀ n x, C x → C (inr n * x)) : C m := by
   rcases mk_surjective m with ⟨x, rfl⟩
-  induction x using FreeMonoid.recOn with
+  induction x with
   | h0 => exact one
   | ih x xs ih =>
     cases x with
@@ -573,7 +573,7 @@ theorem mk_of_inv_mul : ∀ x : G ⊕ H, mk (of (x.map Inv.inv Inv.inv)) * mk (o
 theorem con_mul_left_inv (x : FreeMonoid (G ⊕ H)) :
     coprodCon G H (ofList (x.toList.map (Sum.map Inv.inv Inv.inv)).reverse * x) 1 := by
   rw [← mk_eq_mk, map_mul, map_one]
-  induction x using FreeMonoid.recOn with
+  induction x with
   | h0 => simp [map_one mk] -- TODO: fails without `[map_one mk]`
   | ih x xs ihx =>
     simp only [toList_of_mul, map_cons, reverse_cons, ofList_append, map_mul, ihx, ofList_singleton]

Mathlib/GroupTheory/FreeGroup/Basic.lean

@@ -1027,7 +1027,7 @@ instance : Monad FreeGroup.{u} where
   map {_α} {_β} {f} := map f
   bind {_α} {_β} {x} {f} := lift f x
 
-@[to_additive (attr := elab_as_elim)]
+@[to_additive (attr := elab_as_elim, induction_eliminator)]
 protected theorem induction_on {C : FreeGroup α → Prop} (z : FreeGroup α) (C1 : C 1)
     (Cp : ∀ x, C <| pure x) (Ci : ∀ x, C (pure x) → C (pure x)⁻¹)
     (Cm : ∀ x y, C x → C y → C (x * y)) : C z :=

Mathlib/RingTheory/FreeCommRing.lean

@@ -95,7 +95,7 @@ lemma of_cons (a : α) (m : Multiset α) : (FreeAbelianGroup.of (Multiplicative.
   rw [← Multiset.singleton_add, ofAdd_add,
     of, FreeAbelianGroup.of_mul_of]
 
-@[elab_as_elim]
+@[elab_as_elim, induction_eliminator]
 protected theorem induction_on {C : FreeCommRing α → Prop} (z : FreeCommRing α) (hn1 : C (-1))
     (hb : ∀ b, C (of b)) (ha : ∀ x y, C x → C y → C (x + y)) (hm : ∀ x y, C x → C y → C (x * y)) :
     C z :=
@@ -360,7 +360,7 @@ protected theorem coe_mul (x y : FreeRing α) : ↑(x * y) = (x : FreeCommRing 
 variable (α)
 
 protected theorem coe_surjective : Surjective ((↑) : FreeRing α → FreeCommRing α) := fun x => by
-  induction x using FreeCommRing.induction_on with
+  induction x with
   | hn1 =>
     use -1
     rfl

Mathlib/RingTheory/FreeRing.lean

@@ -56,7 +56,7 @@ theorem of_injective : Function.Injective (of : α → FreeRing α) :=
   FreeAbelianGroup.of_injective.comp FreeMonoid.of_injective
 #align free_ring.of_injective FreeRing.of_injective
 
-@[elab_as_elim]
+@[elab_as_elim, induction_eliminator]
 protected theorem induction_on {C : FreeRing α → Prop} (z : FreeRing α) (hn1 : C (-1))
     (hb : ∀ b, C (of b)) (ha : ∀ x y, C x → C y → C (x + y)) (hm : ∀ x y, C x → C y → C (x * y)) :
     C z :=