chore: @[elab_as_elim] additions (#5147)

This adds `@[elab_as_elim]` to `Quot.rec`, `Nat.strongInductionOn` and
`Nat.casesStrongInductionOn`, and also renames the latter two to
`Nat.strongRecOn` and `Nat.casesStrongRecOn`.

The first change resolves the todos in
[`Mathlib.Init.Quot`](ca6a6fdc07/Mathlib/Init/Quot.lean)
while the other two are based on a suggestion of @YaelDillies on [the
Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Technical.20Debt.20Counters/near/464804567)
and related to
https://github.com/leanprover-community/mathlib4/pull/16096.

src/Init/Core.lean

@@ -1564,7 +1564,7 @@ so you should consider the simpler versions if they apply:
 * `Quot.recOnSubsingleton`, when the target type is a `Subsingleton`
 * `Quot.hrecOn`, which uses `HEq (f a) (f b)` instead of a `sound p ▸ f a = f b` assummption
 -/
-protected abbrev rec
+@[elab_as_elim] protected abbrev rec
     (f : (a : α) → motive (Quot.mk r a))
     (h : (a b : α) → (p : r a b) → Eq.ndrec (f a) (sound p) = f b)
     (q : Quot r) : motive q :=

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -40,7 +40,7 @@ An induction principal that works on divison by two.
 -/
 noncomputable def div2Induction {motive : Nat → Sort u}
     (n : Nat) (ind : ∀(n : Nat), (n > 0 → motive (n/2)) → motive n) : motive n := by
-  induction n using Nat.strongInductionOn with
+  induction n using Nat.strongRecOn with
   | ind n hyp =>
     apply ind
     intro n_pos
@@ -258,7 +258,7 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
 
 @[simp] theorem testBit_mod_two_pow (x j i : Nat) :
     testBit (x % 2^j) i = (decide (i < j) && testBit x i) := by
-  induction x using Nat.strongInductionOn generalizing j i with
+  induction x using Nat.strongRecOn generalizing j i with
   | ind x hyp =>
     rw [mod_eq]
     rcases Nat.lt_or_ge x (2^j) with x_lt_j | x_ge_j
@@ -337,10 +337,9 @@ theorem testBit_one_eq_true_iff_self_eq_zero {i : Nat} :
 
 /-! ### bitwise -/
 
-theorem testBit_bitwise
-  (false_false_axiom : f false false = false) (x y i : Nat)
-: (bitwise f x y).testBit i = f (x.testBit i) (y.testBit i) := by
-  induction i using Nat.strongInductionOn generalizing x y with
+theorem testBit_bitwise (false_false_axiom : f false false = false) (x y i : Nat) :
+    (bitwise f x y).testBit i = f (x.testBit i) (y.testBit i) := by
+  induction i using Nat.strongRecOn generalizing x y with
   | ind i hyp =>
     unfold bitwise
     if x_zero : x = 0 then

src/Init/Data/Nat/Div.lean

@@ -48,7 +48,7 @@ def div.inductionOn.{u}
 decreasing_by apply div_rec_lemma; assumption
 
 theorem div_le_self (n k : Nat) : n / k ≤ n := by
-  induction n using Nat.strongInductionOn with
+  induction n using Nat.strongRecOn with
   | ind n ih =>
     rw [div_eq]
     -- Note: manual split to avoid Classical.em which is not yet defined
@@ -334,7 +334,7 @@ theorem mul_mod_mul_left (z x y : Nat) : (z * x) % (z * y) = z * (x % y) :=
   else if z0 : z = 0 then by
     rw [z0, Nat.zero_mul, Nat.zero_mul, Nat.zero_mul, mod_zero]
   else by
-    induction x using Nat.strongInductionOn with
+    induction x using Nat.strongRecOn with
     | _ n IH =>
       have y0 : y > 0 := Nat.pos_of_ne_zero y0
       have z0 : z > 0 := Nat.pos_of_ne_zero z0

src/Init/Data/Nat/Gcd.lean

@@ -75,7 +75,7 @@ theorem gcd_rec (m n : Nat) : gcd m n = gcd (n % m) m :=
 
 @[elab_as_elim] theorem gcd.induction {P : Nat → Nat → Prop} (m n : Nat)
     (H0 : ∀n, P 0 n) (H1 : ∀ m n, 0 < m → P (n % m) m → P m n) : P m n :=
-  Nat.strongInductionOn (motive := fun m => ∀ n, P m n) m
+  Nat.strongRecOn (motive := fun m => ∀ n, P m n) m
     (fun
     | 0, _ => H0
     | _+1, IH => fun _ => H1 _ _ (succ_pos _) (IH _ (mod_lt _ (succ_pos _)) _) )

src/Init/WF.lean

@@ -190,18 +190,18 @@ def lt_wfRel : WellFoundedRelation Nat where
       | Or.inl e => subst e; assumption
       | Or.inr e => exact Acc.inv ih e
 
-protected noncomputable def strongInductionOn
+@[elab_as_elim] protected noncomputable def strongRecOn
     {motive : Nat → Sort u}
     (n : Nat)
     (ind : ∀ n, (∀ m, m < n → motive m) → motive n) : motive n :=
   Nat.lt_wfRel.wf.fix ind n
 
-protected noncomputable def caseStrongInductionOn
+@[elab_as_elim] protected noncomputable def caseStrongRecOn
     {motive : Nat → Sort u}
     (a : Nat)
     (zero : motive 0)
     (ind : ∀ n, (∀ m, m ≤ n → motive m) → motive (succ n)) : motive a :=
-  Nat.strongInductionOn a fun n =>
+  Nat.strongRecOn a fun n =>
     match n with
     | 0   => fun _  => zero
     | n+1 => fun h₁ => ind n (λ _ h₂ => h₁ _ (lt_succ_of_le h₂))