chore: fix more induction/recursor branch names (#25770)

These were found using the regex `\| h. =>` and `def.*rec.*\(h. :`.

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>

Author: Parcly-Taxel

Mathlib/Analysis/Convolution.lean

@@ -1185,10 +1185,10 @@ theorem contDiffOn_convolution_right_with_param_aux {G : Type uP} {E' : Type uP}
     universe, which is why we make the assumption in the lemma that all the relevant spaces
     come from the same universe). -/
   induction n using ENat.nat_induction generalizing g E' F with
-  | h0 =>
+  | zero =>
     rw [WithTop.coe_zero, contDiffOn_zero] at hg ⊢
     exact continuousOn_convolution_right_with_param L hk hgs hf hg
-  | hsuc n ih =>
+  | succ n ih =>
     simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, WithTop.coe_add,
       WithTop.coe_natCast, WithTop.coe_one] at hg ⊢
     let f' : P → G → P × G →L[𝕜] F := fun p a =>
@@ -1215,7 +1215,7 @@ theorem contDiffOn_convolution_right_with_param_aux {G : Type uP} {E' : Type uP}
         exact hgs p y hp hy
       apply ih (L.precompR (P × G) :) B
       convert hg.2.2
-  | htop ih =>
+  | top ih =>
     rw [contDiffOn_infty] at hg ⊢
     exact fun n ↦ ih n L hgs (hg n)
 

Mathlib/Data/ENat/Basic.lean

@@ -301,11 +301,12 @@ lemma coe_lt_coe {n m : ℕ} : (n : ℕ∞) < (m : ℕ∞) ↔ n < m := by simp
 lemma coe_le_coe {n m : ℕ} : (n : ℕ∞) ≤ (m : ℕ∞) ↔ n ≤ m := by simp
 
 @[elab_as_elim]
-theorem nat_induction {P : ℕ∞ → Prop} (a : ℕ∞) (h0 : P 0) (hsuc : ∀ n : ℕ, P n → P n.succ)
-    (htop : (∀ n : ℕ, P n) → P ⊤) : P a := by
-  have A : ∀ n : ℕ, P n := fun n => Nat.recOn n h0 hsuc
+theorem nat_induction {motive : ℕ∞ → Prop} (a : ℕ∞) (zero : motive 0)
+    (succ : ∀ n : ℕ, motive n → motive n.succ)
+    (top : (∀ n : ℕ, motive n) → motive ⊤) : motive a := by
+  have A : ∀ n : ℕ, motive n := fun n => Nat.recOn n zero succ
   cases a
-  · exact htop A
+  · exact top A
   · exact A _
 
 lemma add_one_pos : 0 < n + 1 :=

Mathlib/Data/Fin/Tuple/Basic.lean

@@ -186,10 +186,11 @@ theorem consCases_cons {P : (∀ i : Fin n.succ, α i) → Sort v} (h : ∀ x₀
 
 /-- Recurse on a tuple by splitting into `Fin.elim0` and `Fin.cons`. -/
 @[elab_as_elim]
-def consInduction {α : Sort*} {P : ∀ {n : ℕ}, (Fin n → α) → Sort v} (h0 : P Fin.elim0)
-    (h : ∀ {n} (x₀) (x : Fin n → α), P x → P (Fin.cons x₀ x)) : ∀ {n : ℕ} (x : Fin n → α), P x
-  | 0, x => by convert h0
-  | _ + 1, x => consCases (fun _ _ ↦ h _ _ <| consInduction h0 h _) x
+def consInduction {α : Sort*} {motive : ∀ {n : ℕ}, (Fin n → α) → Sort v} (elim0 : motive Fin.elim0)
+    (cons : ∀ {n} (x₀) (x : Fin n → α), motive x → motive (Fin.cons x₀ x)) :
+    ∀ {n : ℕ} (x : Fin n → α), motive x
+  | 0, x => by convert elim0
+  | _ + 1, x => consCases (fun _ _ ↦ cons _ _ <| consInduction elim0 cons _) x
 
 theorem cons_injective_of_injective {α} {x₀ : α} {x : Fin n → α} (hx₀ : x₀ ∉ Set.range x)
     (hx : Function.Injective x) : Function.Injective (cons x₀ x : Fin n.succ → α) := by

Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean

@@ -74,11 +74,11 @@ theorem antidiagonalTuple_zero_succ (n : ℕ) : antidiagonalTuple 0 (n + 1) = []
 theorem mem_antidiagonalTuple {n : ℕ} {k : ℕ} {x : Fin k → ℕ} :
     x ∈ antidiagonalTuple k n ↔ ∑ i, x i = n := by
   induction x using Fin.consInduction generalizing n with
-  | h0 =>
+  | elim0 =>
     cases n
     · decide
     · simp
-  | h x₀ x ih =>
+  | cons x₀ x ih =>
     simp_rw [Fin.sum_cons, antidiagonalTuple, List.mem_flatMap, List.mem_map,
       List.Nat.mem_antidiagonal, Fin.cons_inj, exists_eq_right_right, ih,
       @eq_comm _ _ (Prod.snd _), and_comm (a := Prod.snd _ = _),

Mathlib/Data/Seq/Computation.lean

@@ -159,16 +159,17 @@ theorem think_empty : empty α = think (empty α) :=
   destruct_eq_think destruct_empty
 
 /-- Recursion principle for computations, compare with `List.recOn`. -/
-def recOn {C : Computation α → Sort v} (s : Computation α) (h1 : ∀ a, C (pure a))
-    (h2 : ∀ s, C (think s)) : C s :=
+@[elab_as_elim]
+def recOn {motive : Computation α → Sort v} (s : Computation α) (pure : ∀ a, motive (pure a))
+    (think : ∀ s, motive (think s)) : motive s :=
   match H : destruct s with
   | Sum.inl v => by
     rw [destruct_eq_pure H]
-    apply h1
+    apply pure
   | Sum.inr v => match v with
     | ⟨a, s'⟩ => by
       rw [destruct_eq_think H]
-      apply h2
+      apply think
 
 /-- Corecursor constructor for `corec` -/
 def Corec.f (f : β → α ⊕ β) : α ⊕ β → Option α × (α ⊕ β)
@@ -255,7 +256,7 @@ theorem eq_of_bisim (bisim : IsBisimulation R) {s₁ s₂} (r : s₁ ~ s₂) : s
       suffices head s = head s' ∧ R (tail s) (tail s') from
         And.imp id (fun r => ⟨tail s, tail s', by cases s; rfl, by cases s'; rfl, r⟩) this
       have h := bisim r; revert r h
-      apply recOn s _ _ <;> intro r' <;> apply recOn s' _ _ <;> intro a' r h
+      refine recOn s ?_ ?_ <;> intro r' <;> refine recOn s' ?_ ?_ <;> intro a' r h
       · constructor <;> dsimp at h
         · rw [h]
         · rw [h] at r
@@ -502,9 +503,8 @@ theorem length_thinkN (s : Computation α) [_h : Terminates s] (n) :
   (results_thinkN n (results_of_terminates _)).length
 
 theorem eq_thinkN {s : Computation α} {a n} (h : Results s a n) : s = thinkN (pure a) n := by
-  revert s
-  induction n with | zero => _ | succ n IH => _ <;>
-  (intro s; apply recOn s (fun a' => _) fun s => _) <;> intro a h
+  induction n generalizing s with | zero | succ n IH <;>
+  induction s using recOn with | pure a' | think s
   · rw [← eq_of_pure_mem h.mem]
     rfl
   · obtain ⟨n, h⟩ := of_results_think h
@@ -582,7 +582,7 @@ theorem map_think (f : α → β) : ∀ s, map f (think s) = think (map f s)
 
 @[simp]
 theorem destruct_map (f : α → β) (s) : destruct (map f s) = lmap f (rmap (map f) (destruct s)) := by
-  apply s.recOn <;> intro <;> simp
+  induction s using recOn <;> simp
 
 @[simp]
 theorem map_id : ∀ s : Computation α, map id s = s
@@ -623,9 +623,9 @@ theorem bind_pure (f : α → β) (s) : bind s (pure ∘ f) = map f s := by
     match c₁, c₂, h with
     | _, c₂, Or.inl (Eq.refl _) => rcases destruct c₂ with b | cb <;> simp
     | _, _, Or.inr ⟨s, rfl, rfl⟩ =>
-      apply recOn s <;> intro s
-      · simp
-      · simpa using Or.inr ⟨s, rfl, rfl⟩
+      induction s using recOn with
+      | pure s => simp
+      | think s => simpa using Or.inr ⟨s, rfl, rfl⟩
   · exact Or.inr ⟨s, rfl, rfl⟩
 
 @[simp]
@@ -642,11 +642,13 @@ theorem bind_assoc (s : Computation α) (f : α → Computation β) (g : β →
     match c₁, c₂, h with
     | _, c₂, Or.inl (Eq.refl _) => rcases destruct c₂ with b | cb <;> simp
     | _, _, Or.inr ⟨s, rfl, rfl⟩ =>
-      apply recOn s <;> intro s
-      · simp only [BisimO, ret_bind]; generalize f s = fs
-        apply recOn fs <;> intro t <;> simp
-        · rcases destruct (g t) with b | cb <;> simp
-      · simpa  [BisimO] using Or.inr ⟨s, rfl, rfl⟩
+      induction s using recOn with
+      | pure s =>
+        simp only [BisimO, ret_bind]; generalize f s = fs
+        induction fs using recOn with
+        | pure t => rw [ret_bind]; rcases destruct (g t) with b | cb <;> simp
+        | think => simp
+      | think s => simpa [BisimO] using Or.inr ⟨s, rfl, rfl⟩
   · exact Or.inr ⟨s, rfl, rfl⟩
 
 theorem results_bind {s : Computation α} {f : α → Computation β} {a b m n} (h1 : Results s a m)
@@ -687,14 +689,14 @@ theorem length_bind (s : Computation α) (f : α → Computation β) [_T1 : Term
 
 theorem of_results_bind {s : Computation α} {f : α → Computation β} {b k} :
     Results (bind s f) b k → ∃ a m n, Results s a m ∧ Results (f a) b n ∧ k = n + m := by
-  induction k generalizing s with | zero => _ | succ n IH => _
-    <;> apply recOn s (fun a => _) fun s' => _ <;> intro e h
+  induction k generalizing s with | zero | succ n IH <;>
+  induction s using recOn with intro h | pure a | think s'
   · simp only [ret_bind] at h
-    exact ⟨e, _, _, results_pure _, h, rfl⟩
+    exact ⟨_, _, _, results_pure _, h, rfl⟩
   · have := congr_arg head (eq_thinkN h)
     contradiction
   · simp only [ret_bind] at h
-    exact ⟨e, _, n + 1, results_pure _, h, rfl⟩
+    exact ⟨_, _, n + 1, results_pure _, h, rfl⟩
   · simp only [think_bind, results_think_iff] at h
     let ⟨a, m, n', h1, h2, e'⟩ := IH h
     rw [e']
@@ -796,19 +798,17 @@ theorem orElse_think (c₁ c₂ : Computation α) : (think c₁ <|> think c₂)
 theorem empty_orElse (c) : (empty α <|> c) = c := by
   apply eq_of_bisim (fun c₁ c₂ => (empty α <|> c₂) = c₁) _ rfl
   intro s' s h; rw [← h]
-  apply recOn s <;> intro s <;> rw [think_empty]
-  · simp
-  simp only [BisimO, orElse_think, destruct_think]
-  rw [← think_empty]
+  induction s using recOn with rw [think_empty]
+  | pure s => simp
+  | think s => simp only [BisimO, orElse_think, destruct_think]; rw [← think_empty]
 
 @[simp]
 theorem orElse_empty (c : Computation α) : (c <|> empty α) = c := by
   apply eq_of_bisim (fun c₁ c₂ => (c₂ <|> empty α) = c₁) _ rfl
   intro s' s h; rw [← h]
-  apply recOn s <;> intro s <;> rw [think_empty]
-  · simp
-  simp only [BisimO, orElse_think, destruct_think]
-  rw [← think_empty]
+  induction s using recOn with rw [think_empty]
+  | pure s => simp
+  | think s => simp only [BisimO, orElse_think, destruct_think]; rw [← think_empty]
 
 /-- `c₁ ~ c₂` asserts that `c₁` and `c₂` either both terminate with the same result,
   or both loop forever. -/
@@ -1045,11 +1045,11 @@ variable {R : α → β → Prop} {C : Computation α → Computation β → Pro
 @[simp]
 theorem LiftRelAux.ret_left (R : α → β → Prop) (C : Computation α → Computation β → Prop) (a cb) :
     LiftRelAux R C (Sum.inl a) (destruct cb) ↔ ∃ b, b ∈ cb ∧ R a b := by
-  apply cb.recOn (fun b => _) fun cb => _
-  · intro b
+  induction cb using recOn with
+  | pure b =>
     exact
       ⟨fun h => ⟨_, ret_mem _, h⟩, fun ⟨b', mb, h⟩ => by rw [mem_unique (ret_mem _) mb]; exact h⟩
-  · intro
+  | think cb =>
     rw [destruct_think]
     exact ⟨fun ⟨b, h, r⟩ => ⟨b, think_mem h, r⟩, fun ⟨b, h, r⟩ => ⟨b, of_think_mem h, r⟩⟩
 
@@ -1071,10 +1071,9 @@ theorem LiftRelRec.lem {R : α → β → Prop} (C : Computation α → Computat
   · simp only [destruct_pure, LiftRelAux.ret_left] at h
     simp [h]
   · simp only [liftRel_think_left]
-    revert h
-    apply cb.recOn (fun b => _) fun cb' => _ <;> intro _ h
-    · simpa using h
-    · simpa [h] using IH _ h
+    induction cb using recOn with
+    | pure b => simpa using h
+    | think cb => simpa [h] using IH _ h
 
 theorem liftRel_rec {R : α → β → Prop} (C : Computation α → Computation β → Prop)
     (H : ∀ {ca cb}, C ca cb → LiftRelAux R C (destruct ca) (destruct cb)) (ca cb) (Hc : C ca cb) :

Mathlib/Data/Set/Card.lean

@@ -393,16 +393,16 @@ theorem Finite.eq_insert_of_subset_of_encard_eq_succ (hs : s.Finite) (h : s ⊆
   obtain ⟨x, hx⟩ := hst; use x; rw [← diff_union_of_subset h, hx, singleton_union]
 
 theorem exists_subset_encard_eq {k : ℕ∞} (hk : k ≤ s.encard) : ∃ t, t ⊆ s ∧ t.encard = k := by
-  revert hk
-  refine ENat.nat_induction k (fun _ ↦ ⟨∅, empty_subset _, by simp⟩) (fun n IH hle ↦ ?_) ?_
-  · obtain ⟨t₀, ht₀s, ht₀⟩ := IH (le_trans (by simp) hle)
+  induction k using ENat.nat_induction with
+  | zero => exact ⟨∅, empty_subset _, by simp⟩
+  | succ n IH =>
+    obtain ⟨t₀, ht₀s, ht₀⟩ := IH (le_trans (by simp) hk)
     simp only [Nat.cast_succ] at *
     have hne : t₀ ≠ s := by
-      rintro rfl; rw [ht₀, ← Nat.cast_one, ← Nat.cast_add, Nat.cast_le] at hle; simp at hle
+      rintro rfl; rw [ht₀, ← Nat.cast_one, ← Nat.cast_add, Nat.cast_le] at hk; simp at hk
     obtain ⟨x, hx⟩ := exists_of_ssubset (ht₀s.ssubset_of_ne hne)
     exact ⟨insert x t₀, insert_subset hx.1 ht₀s, by rw [encard_insert_of_notMem hx.2, ht₀]⟩
-  simp only [top_le_iff, encard_eq_top_iff]
-  exact fun _ hi ↦ ⟨s, Subset.rfl, hi⟩
+  | top => rw [top_le_iff] at hk; exact ⟨s, Subset.rfl, hk⟩
 
 theorem exists_superset_subset_encard_eq {k : ℕ∞}
     (hst : s ⊆ t) (hsk : s.encard ≤ k) (hkt : k ≤ t.encard) :

Mathlib/Data/WSeq/Basic.lean

@@ -86,9 +86,10 @@ def destruct : WSeq α → Computation (Option (α × WSeq α)) :=
     | some (some a, s') => Sum.inl (some (a, s'))
 
 /-- Recursion principle for weak sequences, compare with `List.recOn`. -/
-def recOn {C : WSeq α → Sort v} (s : WSeq α) (h1 : C nil) (h2 : ∀ x s, C (cons x s))
-    (h3 : ∀ s, C (think s)) : C s :=
-  Seq.recOn s h1 fun o => Option.recOn o h3 h2
+@[elab_as_elim]
+def recOn {motive : WSeq α → Sort v} (s : WSeq α) (nil : motive nil)
+    (cons : ∀ x s, motive (cons x s)) (think : ∀ s, motive (think s)) : motive s :=
+  Seq.recOn s nil fun o => Option.recOn o think cons
 
 /-- membership for weak sequences -/
 protected def Mem (s : WSeq α) (a : α) :=

Mathlib/Logic/Function/Iterate.lean

@@ -177,14 +177,15 @@ theorem comp_iterate_pred_of_pos {n : ℕ} (hn : 0 < n) : f ∘ f^[n.pred] = f^[
   rw [← iterate_succ', Nat.succ_pred_eq_of_pos hn]
 
 /-- A recursor for the iterate of a function. -/
-def Iterate.rec (p : α → Sort*) {f : α → α} (h : ∀ a, p a → p (f a)) {a : α} (ha : p a) (n : ℕ) :
-    p (f^[n] a) :=
+@[elab_as_elim]
+def Iterate.rec (motive : α → Sort*) {a : α} (arg : motive a)
+    {f : α → α} (app : ∀ a, motive a → motive (f a)) (n : ℕ) : motive (f^[n] a) :=
   match n with
-  | 0 => ha
-  | m+1 => Iterate.rec p h (h _ ha) m
+  | 0 => arg
+  | m + 1 => Iterate.rec motive (app _ arg) app m
 
-theorem Iterate.rec_zero (p : α → Sort*) {f : α → α} (h : ∀ a, p a → p (f a)) {a : α} (ha : p a) :
-    Iterate.rec p h ha 0 = ha :=
+theorem Iterate.rec_zero (motive : α → Sort*) {f : α → α} (app : ∀ a, motive a → motive (f a))
+    {a : α} (arg : motive a) : Iterate.rec motive arg app 0 = arg :=
   rfl
 
 variable {f} {m n : ℕ} {a : α}

Mathlib/NumberTheory/ArithmeticFunction.lean

@@ -1090,8 +1090,10 @@ open UniqueFactorizationMonoid
 @[simp]
 theorem moebius_mul_coe_zeta : (μ * ζ : ArithmeticFunction ℤ) = 1 := by
   ext n
-  refine recOnPosPrimePosCoprime ?_ ?_ ?_ ?_ n
-  · intro p n hp hn
+  induction n using recOnPosPrimePosCoprime with
+  | zero => rw [ZeroHom.map_zero, ZeroHom.map_zero]
+  | one => simp
+  | prime_pow p n hp hn =>
     rw [coe_mul_zeta_apply, sum_divisors_prime_pow hp, sum_range_succ']
     simp_rw [Nat.pow_zero, moebius_apply_one,
       moebius_apply_prime_pow hp (Nat.succ_ne_zero _), Nat.succ_inj, sum_ite_eq', mem_range,
@@ -1100,9 +1102,7 @@ theorem moebius_mul_coe_zeta : (μ * ζ : ArithmeticFunction ℤ) = 1 := by
     rw [Ne, pow_eq_one_iff]
     · exact hp.ne_one
     · exact hn.ne'
-  · rw [ZeroHom.map_zero, ZeroHom.map_zero]
-  · simp
-  · intro a b _ha _hb hab ha' hb'
+  | coprime a b _ha _hb hab ha' hb' =>
     rw [IsMultiplicative.map_mul_of_coprime _ hab, ha', hb',
       IsMultiplicative.map_mul_of_coprime isMultiplicative_one hab]
     exact isMultiplicative_moebius.mul isMultiplicative_zeta.natCast

Mathlib/Order/SuccPred/Archimedean.lean

@@ -67,7 +67,7 @@ theorem Succ.rec {P : α → Prop} {m : α} (h0 : P m) (h1 : ∀ n, m ≤ n →
 theorem Succ.rec_iff {p : α → Prop} (hsucc : ∀ a, p a ↔ p (succ a)) {a b : α} (h : a ≤ b) :
     p a ↔ p b := by
   obtain ⟨n, rfl⟩ := h.exists_succ_iterate
-  exact Iterate.rec (fun b => p a ↔ p b) (fun c hc => hc.trans (hsucc _)) Iff.rfl n
+  exact Iterate.rec (fun b => p a ↔ p b) Iff.rfl (fun c hc => hc.trans (hsucc _)) n
 
 lemma le_total_of_codirected {r v₁ v₂ : α} (h₁ : r ≤ v₁) (h₂ : r ≤ v₂) : v₁ ≤ v₂ ∨ v₂ ≤ v₁ := by
   obtain ⟨n, rfl⟩ := h₁.exists_succ_iterate