chore: add cases_eliminator and induction_eliminator to some simple types (#14205)

Namely:

* `AList`
* `Cycle`
* `ConjAct`
* `Projectivization`
* `Lex`
* `NatOrdinal`
* `WithLawson`
* `WithLower`
* `WithUpper`
* `WithScott`
* `WithUpperSet`
* `WithLowerSet`
* `Speicalization` (which had an incorrectly-stated induction principle)

These are just for the cases which have docstrings of the form "Use as `induction .* using .*`".

Inspired by #12605.

Author: eric-wieser

Mathlib/Data/List/AList.lean

@@ -362,8 +362,8 @@ theorem mk_cons_eq_insert (c : Sigma β) (l : List (Sigma β)) (h : (c :: l).Nod
   simpa [insert] using (kerase_of_not_mem_keys <| not_mem_keys_of_nodupKeys_cons h).symm
 #align alist.mk_cons_eq_insert AList.mk_cons_eq_insert
 
-/-- Recursion on an `AList`, using `insert`. Use as `induction l using AList.insertRec`. -/
-@[elab_as_elim]
+/-- Recursion on an `AList`, using `insert`. Use as `induction l`. -/
+@[elab_as_elim, induction_eliminator]
 def insertRec {C : AList β → Sort*} (H0 : C ∅)
     (IH : ∀ (a : α) (b : β a) (l : AList β), a ∉ l → C l → C (l.insert a b)) :
     ∀ l : AList β, C l
@@ -374,8 +374,8 @@ def insertRec {C : AList β → Sort*} (H0 : C ∅)
     exact not_mem_keys_of_nodupKeys_cons h
 #align alist.insert_rec AList.insertRec
 
--- Test that the `induction` tactic works on `insert_rec`.
-example (l : AList β) : True := by induction l using AList.insertRec <;> trivial
+-- Test that the `induction` tactic works on `insertRec`.
+example (l : AList β) : True := by induction l <;> trivial
 
 @[simp]
 theorem insertRec_empty {C : AList β → Sort*} (H0 : C ∅)

Mathlib/Data/List/Cycle.lean

@@ -505,8 +505,8 @@ theorem empty_eq : ∅ = @nil α :=
 instance : Inhabited (Cycle α) :=
   ⟨nil⟩
 
-/-- An induction principle for `Cycle`. Use as `induction s using Cycle.induction_on`. -/
-@[elab_as_elim]
+/-- An induction principle for `Cycle`. Use as `induction s`. -/
+@[elab_as_elim, induction_eliminator]
 theorem induction_on {C : Cycle α → Prop} (s : Cycle α) (H0 : C nil)
     (HI : ∀ (a) (l : List α), C ↑l → C ↑(a :: l)) : C s :=
   Quotient.inductionOn' s fun l => by
@@ -964,7 +964,7 @@ variable {r : α → α → Prop} {s : Cycle α}
 
 theorem Chain.imp {r₁ r₂ : α → α → Prop} (H : ∀ a b, r₁ a b → r₂ a b) (p : Chain r₁ s) :
     Chain r₂ s := by
-  induction s using Cycle.induction_on
+  induction s
   · trivial
   · rw [chain_coe_cons] at p ⊢
     exact p.imp H
@@ -976,7 +976,7 @@ theorem chain_mono : Monotone (Chain : (α → α → Prop) → Cycle α → Pro
 #align cycle.chain_mono Cycle.chain_mono
 
 theorem chain_of_pairwise : (∀ a ∈ s, ∀ b ∈ s, r a b) → Chain r s := by
-  induction' s using Cycle.induction_on with a l _
+  induction' s with a l _
   · exact fun _ => Cycle.Chain.nil r
   intro hs
   have Ha : a ∈ (a :: l : Cycle α) := by simp
@@ -1002,7 +1002,7 @@ theorem chain_of_pairwise : (∀ a ∈ s, ∀ b ∈ s, r a b) → Chain r s := b
 
 theorem chain_iff_pairwise [IsTrans α r] : Chain r s ↔ ∀ a ∈ s, ∀ b ∈ s, r a b :=
   ⟨by
-    induction' s using Cycle.induction_on with a l _
+    induction' s with a l _
     · exact fun _ b hb => (not_mem_nil _ hb).elim
     intro hs b hb c hc
     rw [Cycle.chain_coe_cons, List.chain_iff_pairwise] at hs
@@ -1017,7 +1017,7 @@ theorem chain_iff_pairwise [IsTrans α r] : Chain r s ↔ ∀ a ∈ s, ∀ b ∈
 #align cycle.chain_iff_pairwise Cycle.chain_iff_pairwise
 
 theorem Chain.eq_nil_of_irrefl [IsTrans α r] [IsIrrefl α r] (h : Chain r s) : s = Cycle.nil := by
-  induction' s using Cycle.induction_on with a l _ h
+  induction' s with a l _ h
   · rfl
   · have ha := mem_cons_self a l
     exact (irrefl_of r a <| chain_iff_pairwise.1 h a ha a ha).elim

Mathlib/GroupTheory/GroupAction/ConjAct.lean

@@ -81,7 +81,8 @@ def toConjAct : G ≃* ConjAct G :=
   ofConjAct.symm
 #align conj_act.to_conj_act ConjAct.toConjAct
 
-/-- A recursor for `ConjAct`, for use as `induction x using ConjAct.rec` when `x : ConjAct G`. -/
+/-- A recursor for `ConjAct`, for use as `induction x` when `x : ConjAct G`. -/
+@[elab_as_elim, cases_eliminator, induction_eliminator]
 protected def rec {C : ConjAct G → Sort*} (h : ∀ g, C (toConjAct g)) : ∀ g, C g :=
   h
 #align conj_act.rec ConjAct.rec

Mathlib/LinearAlgebra/Projectivization/Basic.lean

@@ -122,9 +122,8 @@ theorem exists_smul_eq_mk_rep (v : V) (hv : v ≠ 0) : ∃ a : Kˣ, a • v = (m
 
 variable {K}
 
-/-- An induction principle for `Projectivization`.
-Use as `induction v using Projectivization.ind`. -/
-@[elab_as_elim]
+/-- An induction principle for `Projectivization`. Use as `induction v`. -/
+@[elab_as_elim, cases_eliminator, induction_eliminator]
 theorem ind {P : ℙ K V → Prop} (h : ∀ (v : V) (h : v ≠ 0), P (mk K v h)) : ∀ p, P p :=
   Quotient.ind' <| Subtype.rec <| h
 #align projectivization.ind Projectivization.ind

Mathlib/Order/Synonym.lean

@@ -202,7 +202,8 @@ theorem ofLex_inj {a b : Lex α} : ofLex a = ofLex b ↔ a = b :=
   Iff.rfl
 #align of_lex_inj ofLex_inj
 
-/-- A recursor for `Lex`. Use as `induction x using Lex.rec`. -/
+/-- A recursor for `Lex`. Use as `induction x`. -/
+@[elab_as_elim, induction_eliminator, cases_eliminator]
 protected def Lex.rec {β : Lex α → Sort*} (h : ∀ a, β (toLex a)) : ∀ a, β a := fun a => h (ofLex a)
 #align lex.rec Lex.rec
 

Mathlib/SetTheory/Ordinal/NaturalOps.lean

@@ -133,7 +133,8 @@ theorem succ_def (a : NatOrdinal) : succ a = toNatOrdinal (toOrdinal a + 1) :=
   rfl
 #align nat_ordinal.succ_def NatOrdinal.succ_def
 
-/-- A recursor for `NatOrdinal`. Use as `induction x using NatOrdinal.rec`. -/
+/-- A recursor for `NatOrdinal`. Use as `induction x`. -/
+@[elab_as_elim, cases_eliminator, induction_eliminator]
 protected def rec {β : NatOrdinal → Sort*} (h : ∀ a, β (toNatOrdinal a)) : ∀ a, β a := fun a =>
   h (toOrdinal a)
 #align nat_ordinal.rec NatOrdinal.rec

Mathlib/Topology/Order/LawsonTopology.lean

@@ -127,7 +127,8 @@ lemma toLawson_inj {a b : α} : toLawson a = toLawson b ↔ a = b := Iff.rfl
 @[simp, nolint simpNF]
 lemma ofLawson_inj {a b : WithLawson α} : ofLawson a = ofLawson b ↔ a = b := Iff.rfl
 
-/-- A recursor for `WithLawson`. Use as `induction' x using WithLawson.rec`. -/
+/-- A recursor for `WithLawson`. Use as `induction' x`. -/
+@[elab_as_elim, cases_eliminator, induction_eliminator]
 protected def rec {β : WithLawson α → Sort*}
     (h : ∀ a, β (toLawson a)) : ∀ a, β a := fun a => h (ofLawson a)
 

Mathlib/Topology/Order/LowerUpperTopology.lean

@@ -103,7 +103,8 @@ theorem ofLower_inj {a b : WithLower α} : ofLower a = ofLower b ↔ a = b :=
   Iff.rfl
 #align with_lower_topology.of_lower_inj Topology.WithLower.ofLower_inj
 
-/-- A recursor for `WithLower`. Use as `induction x using WithLower.rec`. -/
+/-- A recursor for `WithLower`. Use as `induction x`. -/
+@[elab_as_elim, cases_eliminator, induction_eliminator]
 protected def rec {β : WithLower α → Sort*} (h : ∀ a, β (toLower a)) : ∀ a, β a := fun a =>
   h (ofLower a)
 #align with_lower_topology.rec Topology.WithLower.rec
@@ -142,7 +143,8 @@ namespace WithUpper
 lemma toUpper_inj {a b : α} : toUpper a = toUpper b ↔ a = b := Iff.rfl
 lemma ofUpper_inj {a b : WithUpper α} : ofUpper a = ofUpper b ↔ a = b := Iff.rfl
 
-/-- A recursor for `WithUpper`. Use as `induction x using WithUpper.rec`. -/
+/-- A recursor for `WithUpper`. Use as `induction x`. -/
+@[elab_as_elim, cases_eliminator, induction_eliminator]
 protected def rec {β : WithUpper α → Sort*} (h : ∀ a, β (toUpper a)) : ∀ a, β a := fun a =>
   h (ofUpper a)
 

Mathlib/Topology/Order/ScottTopology.lean

@@ -317,7 +317,8 @@ lemma toScott_inj {a b : α} : toScott a = toScott b ↔ a = b := Iff.rfl
 @[simp, nolint simpNF]
 lemma ofScott_inj {a b : WithScott α} : ofScott a = ofScott b ↔ a = b := Iff.rfl
 
-/-- A recursor for `WithScott`. Use as `induction x using WithScott.rec`. -/
+/-- A recursor for `WithScott`. Use as `induction x`. -/
+@[elab_as_elim, cases_eliminator, induction_eliminator]
 protected def rec {β : WithScott α → Sort _}
     (h : ∀ a, β (toScott a)) : ∀ a, β a := fun a ↦ h (ofScott a)
 

Mathlib/Topology/Order/UpperLowerSetTopology.lean

@@ -87,7 +87,8 @@ namespace WithUpperSet
 lemma toUpperSet_inj {a b : α} : toUpperSet a = toUpperSet b ↔ a = b := Iff.rfl
 lemma ofUpperSet_inj {a b : WithUpperSet α} : ofUpperSet a = ofUpperSet b ↔ a = b := Iff.rfl
 
-/-- A recursor for `WithUpperSet`. Use as `induction x using WithUpperSet.rec`. -/
+/-- A recursor for `WithUpperSet`. Use as `induction x`. -/
+@[elab_as_elim, cases_eliminator, induction_eliminator]
 protected def rec {β : WithUpperSet α → Sort*} (h : ∀ a, β (toUpperSet a)) : ∀ a, β a :=
   fun a => h (ofUpperSet a)
 
@@ -132,7 +133,8 @@ namespace WithLowerSet
 lemma toLowerSet_inj {a b : α} : toLowerSet a = toLowerSet b ↔ a = b := Iff.rfl
 lemma ofLowerSet_inj {a b : WithLowerSet α} : ofLowerSet a = ofLowerSet b ↔ a = b := Iff.rfl
 
-/-- A recursor for `WithLowerSet`. Use as `induction x using WithLowerSet.rec`. -/
+/-- A recursor for `WithLowerSet`. Use as `induction x`. -/
+@[elab_as_elim, cases_eliminator, induction_eliminator]
 protected def rec {β : WithLowerSet α → Sort*} (h : ∀ a, β (toLowerSet a)) : ∀ a, β a :=
   fun a => h (ofLowerSet a)
 

Mathlib/Topology/Specialization.lean

@@ -38,9 +38,11 @@ variable {α β γ : Type*}
 @[simp, nolint simpNF] lemma ofEquiv_inj {a b : Specialization α} : ofEquiv a = ofEquiv b ↔ a = b :=
 Iff.rfl
 
-/-- A recursor for `Specialization`. Use as `induction x using Specialization.rec`. -/
-protected def rec {β : Specialization α → Sort*} (h : ∀ a, β (toEquiv a)) (a : α) : β a :=
-h (ofEquiv a)
+/-- A recursor for `Specialization`. Use as `induction x`. -/
+@[elab_as_elim, cases_eliminator, induction_eliminator]
+protected def rec {β : Specialization α → Sort*} (h : ∀ a, β (toEquiv a)) (a : Specialization α) :
+    β a :=
+  h (ofEquiv a)
 
 variable [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ]