chore: register MulOpposite.rec with induction and cases (#14136)

Split from #12605.

Co-authored-by: negiizhao [email protected]

Author: eric-wieser

Mathlib/Algebra/Algebra/Operations.lean

@@ -128,7 +128,7 @@ protected theorem map_one {A'} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A')
 theorem map_op_one :
     map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (1 : Submodule R A) = 1 := by
   ext x
-  induction x using MulOpposite.rec'
+  induction x
   simp
 #align submodule.map_op_one Submodule.map_op_one
 

Mathlib/Algebra/Group/Action/Defs.lean

@@ -282,7 +282,7 @@ class IsCentralScalar (M α : Type*) [SMul M α] [SMul Mᵐᵒᵖ α] : Prop whe
 @[to_additive]
 lemma IsCentralScalar.unop_smul_eq_smul {M α : Type*} [SMul M α] [SMul Mᵐᵒᵖ α]
     [IsCentralScalar M α] (m : Mᵐᵒᵖ) (a : α) : MulOpposite.unop m • a = m • a := by
-  induction m using MulOpposite.rec'; exact (IsCentralScalar.op_smul_eq_smul _ a).symm
+  induction m; exact (IsCentralScalar.op_smul_eq_smul _ a).symm
 #align is_central_scalar.unop_smul_eq_smul IsCentralScalar.unop_smul_eq_smul
 #align is_central_vadd.unop_vadd_eq_vadd IsCentralVAdd.unop_vadd_eq_vadd
 

Mathlib/Algebra/Opposites.lean

@@ -110,9 +110,9 @@ theorem unop_comp_op : (unop : αᵐᵒᵖ → α) ∘ op = id :=
 #align mul_opposite.unop_comp_op MulOpposite.unop_comp_op
 #align add_opposite.unop_comp_op AddOpposite.unop_comp_op
 
-/-- A recursor for `MulOpposite`. Use as `induction x using MulOpposite.rec'`. -/
-@[to_additive (attr := simp, elab_as_elim)
-  "A recursor for `AddOpposite`. Use as `induction x using AddOpposite.rec'`."]
+/-- A recursor for `MulOpposite`. Use as `induction x`. -/
+@[to_additive (attr := simp, elab_as_elim, induction_eliminator, cases_eliminator)
+  "A recursor for `AddOpposite`. Use as `induction x`."]
 protected def rec' {F : αᵐᵒᵖ → Sort*} (h : ∀ X, F (op X)) : ∀ X, F X := fun X ↦ h (unop X)
 #align mul_opposite.rec MulOpposite.rec'
 #align add_opposite.rec AddOpposite.rec'

Mathlib/Algebra/Quandle.lean

@@ -259,9 +259,9 @@ instance oppositeRack : Rack Rᵐᵒᵖ where
   act x y := op (invAct (unop x) (unop y))
   self_distrib := by
     intro x y z
-    induction x using MulOpposite.rec'
-    induction y using MulOpposite.rec'
-    induction z using MulOpposite.rec'
+    induction x
+    induction y
+    induction z
     simp only [op_inj, unop_op, op_unop]
     rw [self_distrib_inv]
   invAct x y := op (Shelf.act (unop x) (unop y))
@@ -416,7 +416,7 @@ theorem fix_inv {x : Q} : x ◃⁻¹ x = x := by
 instance oppositeQuandle : Quandle Qᵐᵒᵖ where
   fix := by
     intro x
-    induction' x using MulOpposite.rec'
+    induction' x
     simp
 #align quandle.opposite_quandle Quandle.oppositeQuandle
 

Mathlib/GroupTheory/GroupAction/Opposite.lean

@@ -229,7 +229,7 @@ instance IsScalarTower.opposite_mid {M N} [Mul N] [SMul M N] [SMulCommClass M N
 instance SMulCommClass.opposite_mid {M N} [Mul N] [SMul M N] [IsScalarTower M N N] :
     SMulCommClass M Nᵐᵒᵖ N :=
   ⟨fun x y z => by
-    induction y using MulOpposite.rec'
+    induction y
     simp only [smul_mul_assoc, MulOpposite.smul_eq_mul_unop]⟩
 #align smul_comm_class.opposite_mid SMulCommClass.opposite_mid
 #align vadd_comm_class.opposite_mid VAddCommClass.opposite_mid

Mathlib/RingTheory/Polynomial/Opposites.lean

@@ -94,14 +94,14 @@ set_option linter.uppercaseLean3 false in
 @[simp]
 theorem coeff_opRingEquiv (p : R[X]ᵐᵒᵖ) (n : ℕ) :
     (opRingEquiv R p).coeff n = op ((unop p).coeff n) := by
-  induction' p using MulOpposite.rec' with p
+  induction' p with p
   cases p
   rfl
 #align polynomial.coeff_op_ring_equiv Polynomial.coeff_opRingEquiv
 
 @[simp]
 theorem support_opRingEquiv (p : R[X]ᵐᵒᵖ) : (opRingEquiv R p).support = (unop p).support := by
-  induction' p using MulOpposite.rec' with p
+  induction' p with p
   cases p
   exact Finsupp.support_mapRange_of_injective (map_zero _) _ op_injective
 #align polynomial.support_op_ring_equiv Polynomial.support_opRingEquiv