chore: better recursor names for ℤ (#25555)

Also modify `Int.le_induction` and `Int.le_induction_down` to be like `Nat.le_induction` – `induction n, hn using` syntax can now be used with the first two recursors.

See [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Naming.20of.20.60Int.60.20recursors/near/522863583).

Author: Parcly-Taxel

Mathlib/Algebra/Group/Basic.lean

@@ -833,9 +833,9 @@ lemma zpow_sub_one (a : G) (n : ℤ) : a ^ (n - 1) = a ^ n * a⁻¹ :=
 @[to_additive add_zsmul]
 lemma zpow_add (a : G) (m n : ℤ) : a ^ (m + n) = a ^ m * a ^ n := by
   induction n with
-  | hz => simp
-  | hp n ihn => simp only [← Int.add_assoc, zpow_add_one, ihn, mul_assoc]
-  | hn n ihn => rw [zpow_sub_one, ← mul_assoc, ← ihn, ← zpow_sub_one, Int.add_sub_assoc]
+  | zero => simp
+  | succ n ihn => simp only [← Int.add_assoc, zpow_add_one, ihn, mul_assoc]
+  | pred n ihn => rw [zpow_sub_one, ← mul_assoc, ← ihn, ← zpow_sub_one, Int.add_sub_assoc]
 
 @[to_additive one_add_zsmul]
 lemma zpow_one_add (a : G) (n : ℤ) : a ^ (1 + n) = a * a ^ n := by rw [zpow_add, zpow_one]
@@ -888,11 +888,11 @@ addition by `g` and `-g` on the left. For additive subgroups generated by more t
 lemma zpow_induction_left {g : G} {P : G → Prop} (h_one : P (1 : G))
     (h_mul : ∀ a, P a → P (g * a)) (h_inv : ∀ a, P a → P (g⁻¹ * a)) (n : ℤ) : P (g ^ n) := by
   induction n with
-  | hz => rwa [zpow_zero]
-  | hp n ih =>
+  | zero => rwa [zpow_zero]
+  | succ n ih =>
     rw [Int.add_comm, zpow_add, zpow_one]
     exact h_mul _ ih
-  | hn n ih =>
+  | pred n ih =>
     rw [Int.sub_eq_add_neg, Int.add_comm, zpow_add, zpow_neg_one]
     exact h_inv _ ih
 
@@ -905,11 +905,11 @@ see `AddSubgroup.closure_induction_right`."]
 lemma zpow_induction_right {g : G} {P : G → Prop} (h_one : P (1 : G))
     (h_mul : ∀ a, P a → P (a * g)) (h_inv : ∀ a, P a → P (a * g⁻¹)) (n : ℤ) : P (g ^ n) := by
   induction n with
-  | hz => rwa [zpow_zero]
-  | hp n ih =>
+  | zero => rwa [zpow_zero]
+  | succ n ih =>
     rw [zpow_add_one]
     exact h_mul _ ih
-  | hn n ih =>
+  | pred n ih =>
     rw [zpow_sub_one]
     exact h_inv _ ih
 

Mathlib/Algebra/GroupWithZero/Basic.lean

@@ -420,9 +420,9 @@ lemma zpow_sub_one₀ (ha : a ≠ 0) (n : ℤ) : a ^ (n - 1) = a ^ n * a⁻¹ :=
 
 lemma zpow_add₀ (ha : a ≠ 0) (m n : ℤ) : a ^ (m + n) = a ^ m * a ^ n := by
   induction n with
-  | hz => simp
-  | hp n ihn => simp only [← Int.add_assoc, zpow_add_one₀ ha, ihn, mul_assoc]
-  | hn n ihn => rw [zpow_sub_one₀ ha, ← mul_assoc, ← ihn, ← zpow_sub_one₀ ha, Int.add_sub_assoc]
+  | zero => simp
+  | succ n ihn => simp only [← Int.add_assoc, zpow_add_one₀ ha, ihn, mul_assoc]
+  | pred n ihn => rw [zpow_sub_one₀ ha, ← mul_assoc, ← ihn, ← zpow_sub_one₀ ha, Int.add_sub_assoc]
 
 lemma zpow_add' {m n : ℤ} (h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0) :
     a ^ (m + n) = a ^ m * a ^ n := by

Mathlib/Algebra/Module/LinearMap/Defs.lean

@@ -580,9 +580,9 @@ instance CompatibleSMul.intModule {S : Type*} [Semiring S] [Module S M] [Module
     CompatibleSMul M M₂ ℤ S :=
   ⟨fun fₗ c x ↦ by
     induction c with
-    | hz => simp
-    | hp n ih => simp [add_smul, ih]
-    | hn n ih => simp [sub_smul, ih]⟩
+    | zero => simp
+    | succ n ih => simp [add_smul, ih]
+    | pred n ih => simp [sub_smul, ih]⟩
 
 instance CompatibleSMul.units {R S : Type*} [Monoid R] [MulAction R M] [MulAction R M₂]
     [Semiring S] [Module S M] [Module S M₂] [CompatibleSMul M M₂ R S] : CompatibleSMul M M₂ Rˣ S :=

Mathlib/Data/Int/Init.lean

@@ -71,51 +71,52 @@ the upwards induction step `p i → p (i + 1)` and the downwards induction step
 
 It is used as the default induction principle for the `induction` tactic.
 -/
-@[elab_as_elim, induction_eliminator] protected lemma induction_on {p : ℤ → Prop} (i : ℤ)
-    (hz : p 0) (hp : ∀ i : ℕ, p i → p (i + 1)) (hn : ∀ i : ℕ, p (-i) → p (-i - 1)) : p i := by
+@[elab_as_elim, induction_eliminator] protected lemma induction_on {motive : ℤ → Prop} (i : ℤ)
+    (zero : motive 0) (succ : ∀ i : ℕ, motive i → motive (i + 1))
+    (pred : ∀ i : ℕ, motive (-i) → motive (-i - 1)) : motive i := by
   cases i with
   | ofNat i =>
     induction i with
-    | zero => exact hz
-    | succ i ih => exact hp _ ih
+    | zero => exact zero
+    | succ i ih => exact succ _ ih
   | negSucc i =>
-    suffices ∀ n : ℕ, p (-n) from this (i + 1)
+    suffices ∀ n : ℕ, motive (-n) from this (i + 1)
     intro n; induction n with
-    | zero => simp [hz]
-    | succ n ih => simpa [natCast_succ, Int.neg_add, Int.sub_eq_add_neg] using hn _ ih
+    | zero => simp [zero]
+    | succ n ih => simpa [natCast_succ, Int.neg_add, Int.sub_eq_add_neg] using pred _ ih
 
 section inductionOn'
 
-variable {C : ℤ → Sort*} (z b : ℤ)
-  (H0 : C b) (Hs : ∀ k, b ≤ k → C k → C (k + 1)) (Hp : ∀ k ≤ b, C k → C (k - 1))
+variable {motive : ℤ → Sort*} (z b : ℤ) (zero : motive b)
+  (succ : ∀ k, b ≤ k → motive k → motive (k + 1)) (pred : ∀ k ≤ b, motive k → motive (k - 1))
 
 /-- Inductively define a function on `ℤ` by defining it at `b`, for the `succ` of a number greater
 than `b`, and the `pred` of a number less than `b`. -/
-@[elab_as_elim] protected def inductionOn' : C z :=
-  cast (congrArg C <| show b + (z - b) = z by rw [Int.add_comm, z.sub_add_cancel b]) <|
+@[elab_as_elim] protected def inductionOn' : motive z :=
+  cast (congrArg motive <| show b + (z - b) = z by rw [Int.add_comm, z.sub_add_cancel b]) <|
   match z - b with
   | .ofNat n => pos n
   | .negSucc n => neg n
 where
   /-- The positive case of `Int.inductionOn'`. -/
-  pos : ∀ n : ℕ, C (b + n)
-  | 0 => cast (by simp) H0
+  pos : ∀ n : ℕ, motive (b + n)
+  | 0 => cast (by simp) zero
   | n+1 => cast (by rw [Int.add_assoc]; rfl) <|
-    Hs _ (Int.le_add_of_nonneg_right (natCast_nonneg _)) (pos n)
+    succ _ (Int.le_add_of_nonneg_right (natCast_nonneg _)) (pos n)
   /-- The negative case of `Int.inductionOn'`. -/
-  neg : ∀ n : ℕ, C (b + -[n+1])
-  | 0 => Hp _ Int.le_rfl H0
+  neg : ∀ n : ℕ, motive (b + -[n+1])
+  | 0 => pred _ Int.le_rfl zero
   | n+1 => by
-    refine cast (by rw [Int.add_sub_assoc]; rfl) (Hp _ (Int.le_of_lt ?_) (neg n))
+    refine cast (by rw [Int.add_sub_assoc]; rfl) (pred _ (Int.le_of_lt ?_) (neg n))
     omega
 
-variable {z b H0 Hs Hp}
+variable {z b zero succ pred}
 
-lemma inductionOn'_self : b.inductionOn' b H0 Hs Hp = H0 :=
+lemma inductionOn'_self : b.inductionOn' b zero succ pred = zero :=
   cast_eq_iff_heq.mpr <| .symm <| by rw [b.sub_self, ← cast_eq_iff_heq]; rfl
 
 lemma inductionOn'_sub_one (hz : z ≤ b) :
-    (z - 1).inductionOn' b H0 Hs Hp = Hp z hz (z.inductionOn' b H0 Hs Hp) := by
+    (z - 1).inductionOn' b zero succ pred = pred z hz (z.inductionOn' b zero succ pred) := by
   apply cast_eq_iff_heq.mpr
   obtain ⟨n, hn⟩ := Int.eq_negSucc_of_lt_zero (show z - 1 - b < 0 by omega)
   rw [hn]
@@ -133,35 +134,38 @@ lemma inductionOn'_sub_one (hz : z ≤ b) :
 end inductionOn'
 
 /-- Inductively define a function on `ℤ` by defining it on `ℕ` and extending it from `n` to `-n`. -/
-@[elab_as_elim] protected def negInduction {C : ℤ → Sort*} (nat : ∀ n : ℕ, C n)
-    (neg : (∀ n : ℕ, C n) → ∀ n : ℕ, C (-n)) : ∀ n : ℤ, C n
+@[elab_as_elim] protected def negInduction {motive : ℤ → Sort*} (nat : ∀ n : ℕ, motive n)
+    (neg : (∀ n : ℕ, motive n) → ∀ n : ℕ, motive (-n)) : ∀ n : ℤ, motive n
   | .ofNat n => nat n
   | .negSucc n => neg nat <| n + 1
 
 /-- See `Int.inductionOn'` for an induction in both directions. -/
-protected lemma le_induction {P : ℤ → Prop} {m : ℤ} (h0 : P m)
-    (h1 : ∀ n : ℤ, m ≤ n → P n → P (n + 1)) (n : ℤ) : m ≤ n → P n := by
-  refine Int.inductionOn' n m ?_ ?_ ?_
+@[elab_as_elim]
+protected lemma le_induction {m : ℤ} {motive : ∀ n, m ≤ n → Prop} (base : motive m m.le_refl)
+    (succ : ∀ n hmn, motive n hmn → motive (n + 1) (le_add_one hmn)) : ∀ n hmn, motive n hmn := by
+  refine fun n ↦ Int.inductionOn' n m ?_ ?_ ?_
   · intro
-    exact h0
+    exact base
   · intro k hle hi _
-    exact h1 k hle (hi hle)
+    exact succ k hle (hi hle)
   · intro k hle _ hle'
     omega
 
 /-- See `Int.inductionOn'` for an induction in both directions. -/
-protected theorem le_induction_down {P : ℤ → Prop} {m : ℤ} (h0 : P m)
-    (h1 : ∀ n : ℤ, n ≤ m → P n → P (n - 1)) (n : ℤ) : n ≤ m → P n :=
-  Int.inductionOn' n m (fun _ ↦ h0) (fun k hle _ hle' ↦ by omega)
-    fun k hle hi _ ↦ h1 k hle (hi hle)
+@[elab_as_elim]
+protected lemma le_induction_down {m : ℤ} {motive : ∀ n, n ≤ m → Prop} (base : motive m m.le_refl)
+    (pred : ∀ n hmn, motive n hmn → motive (n - 1) (by omega)) : ∀ n hmn, motive n hmn := fun n ↦
+  Int.inductionOn' n m (fun _ ↦ base) (fun k hle _ hle' ↦ by omega)
+    fun k hle hi _ ↦ pred k hle (hi hle)
 
 section strongRec
 
-variable {P : ℤ → Sort*} (lt : ∀ n < m, P n) (ge : ∀ n ≥ m, (∀ k < n, P k) → P n)
+variable {motive : ℤ → Sort*} (lt : ∀ n < m, motive n)
+  (ge : ∀ n ≥ m, (∀ k < n, motive k) → motive n)
 
 /-- A strong recursor for `Int` that specifies explicit values for integers below a threshold,
 and is analogous to `Nat.strongRec` for integers on or above the threshold. -/
-@[elab_as_elim] protected def strongRec (n : ℤ) : P n := by
+@[elab_as_elim] protected def strongRec (n : ℤ) : motive n := by
   refine if hnm : n < m then lt n hnm else ge n (by omega) (n.inductionOn' m lt ?_ ?_)
   · intro _n _ ih l _
     exact if hlm : l < m then lt l hlm else ge l (by omega) fun k _ ↦ ih k (by omega)

Mathlib/GroupTheory/CoprodI.lean

@@ -1031,12 +1031,9 @@ theorem _root_.FreeGroup.injective_lift_of_ping_pong : Function.Injective (FreeG
           smul_set_mono ((hXYdisj j i).union_left <| hYdisj hij.symm).subset_compl_right
         _ ⊆ X i := by
           clear hnne0 hlt
-          refine Int.le_induction (P := fun n => a i ^ n • (Y i)ᶜ ⊆ X i) ?_ ?_ n h1n
-          · dsimp
-            rw [zpow_one]
-            exact hX i
-          · dsimp
-            intro n _hle hi
+          induction n, h1n using Int.le_induction with
+          | base => rw [zpow_one]; exact hX i
+          | succ n _hle hi =>
             calc
               a i ^ (n + 1) • (Y i)ᶜ = (a i ^ n * a i) • (Y i)ᶜ := by rw [zpow_add, zpow_one]
               _ = a i ^ n • a i • (Y i)ᶜ := MulAction.mul_smul _ _ _
@@ -1051,12 +1048,10 @@ theorem _root_.FreeGroup.injective_lift_of_ping_pong : Function.Injective (FreeG
         a i ^ n • X' j ⊆ a i ^ n • (X i)ᶜ :=
           smul_set_mono ((hXdisj hij.symm).union_left (hXYdisj i j).symm).subset_compl_right
         _ ⊆ Y i := by
-          refine Int.le_induction_down (P := fun n => a i ^ n • (X i)ᶜ ⊆ Y i) ?_ ?_ _ h1n
-          · dsimp
-            rw [zpow_neg, zpow_one]
-            exact hY i
-          · dsimp
-            intro n _ hi
+          clear hnne0 hgt
+          induction n, h1n using Int.le_induction_down with
+          | base => rw [zpow_neg, zpow_one]; exact hY i
+          | pred n hle hi =>
             calc
               a i ^ (n - 1) • (X i)ᶜ = (a i ^ n * (a i)⁻¹) • (X i)ᶜ := by rw [zpow_sub, zpow_one]
               _ = a i ^ n • (a i)⁻¹ • (X i)ᶜ := MulAction.mul_smul _ _ _

Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean

@@ -224,10 +224,10 @@ private lemma prop_red_T_pow (hS : ∀ B, C B → C (S • B)) (hT : ∀ B, C B
      ∀ B (n : ℤ), C (T^n • B) ↔ C B := by
   intro B n
   induction n with
-  | hz => simp only [zpow_zero, one_smul, imp_self]
-  | hp n hn =>
+  | zero => simp only [zpow_zero, one_smul, imp_self]
+  | succ n hn =>
     simpa only [add_comm (n:ℤ), zpow_add _ 1, ← smul_eq_mul, zpow_one, smul_assoc, prop_red_T hS hT]
-  | hn m hm =>
+  | pred m hm =>
     rwa [sub_eq_neg_add, zpow_add, zpow_neg_one, ← prop_red_T hS hT, mul_smul, smul_inv_smul]
 
 @[elab_as_elim]

Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean

@@ -468,12 +468,12 @@ theorem coe_T_inv : ↑(T⁻¹) = !![1, -1; 0, 1] := by simp [coe_inv, coe_T, ad
 
 theorem coe_T_zpow (n : ℤ) : (T ^ n).1 = !![1, n; 0, 1] := by
   induction n with
-  | hz => rw [zpow_zero, coe_one, Matrix.one_fin_two]
-  | hp n h =>
+  | zero => rw [zpow_zero, coe_one, Matrix.one_fin_two]
+  | succ n h =>
     simp_rw [zpow_add, zpow_one, coe_mul, h, coe_T, Matrix.mul_fin_two]
     congrm !![_, ?_; _, _]
     rw [mul_one, mul_one, add_comm]
-  | hn n h =>
+  | pred n h =>
     simp_rw [zpow_sub, zpow_one, coe_mul, h, coe_T_inv, Matrix.mul_fin_two]
     congrm !![?_, ?_; _, _] <;> ring
 

Mathlib/LinearAlgebra/Matrix/ZPow.lean

@@ -109,12 +109,12 @@ theorem _root_.IsUnit.det_zpow {A : M} (h : IsUnit A.det) (n : ℤ) : IsUnit (A
 
 theorem isUnit_det_zpow_iff {A : M} {z : ℤ} : IsUnit (A ^ z).det ↔ IsUnit A.det ∨ z = 0 := by
   induction z with
-  | hz => simp
-  | hp z =>
+  | zero => simp
+  | succ z =>
     rw [← Int.natCast_succ, zpow_natCast, det_pow, isUnit_pow_succ_iff, ← Int.ofNat_zero,
       Int.ofNat_inj]
     simp
-  | hn z =>
+  | pred z =>
     rw [← neg_add', ← Int.natCast_succ, zpow_neg_natCast, isUnit_nonsing_inv_det_iff, det_pow,
       isUnit_pow_succ_iff, neg_eq_zero, ← Int.ofNat_zero, Int.ofNat_inj]
     simp
@@ -148,9 +148,9 @@ theorem zpow_sub_one {A : M} (h : IsUnit A.det) (n : ℤ) : A ^ (n - 1) = A ^ n
 
 theorem zpow_add {A : M} (ha : IsUnit A.det) (m n : ℤ) : A ^ (m + n) = A ^ m * A ^ n := by
   induction n with
-  | hz => simp
-  | hp n ihn => simp only [← add_assoc, zpow_add_one ha, ihn, mul_assoc]
-  | hn n ihn => rw [zpow_sub_one ha, ← mul_assoc, ← ihn, ← zpow_sub_one ha, add_sub_assoc]
+  | zero => simp
+  | succ n ihn => simp only [← add_assoc, zpow_add_one ha, ihn, mul_assoc]
+  | pred n ihn => rw [zpow_sub_one ha, ← mul_assoc, ← ihn, ← zpow_sub_one ha, add_sub_assoc]
 
 theorem zpow_add_of_nonpos {A : M} {m n : ℤ} (hm : m ≤ 0) (hn : n ≤ 0) :
     A ^ (m + n) = A ^ m * A ^ n := by

Mathlib/LinearAlgebra/Reflection.lean

@@ -279,8 +279,8 @@ lemma reflection_mul_reflection_zpow_apply_self (m : ℤ)
       (S R (k - 2)).eval t = (f y * g x - 2) * (S R (k - 1)).eval t - (S R k).eval t := by
     simp [S_sub_two, ht]
   induction m with
-  | hz => simp
-  | hp m ih =>
+  | zero => simp
+  | succ m ih =>
     -- Apply the inductive hypothesis.
     rw [add_comm (m : ℤ) 1, zpow_one_add, LinearEquiv.mul_apply, LinearEquiv.mul_apply, ih]
     -- Expand out all the reflections and use `hf`, `hg`.
@@ -289,7 +289,7 @@ lemma reflection_mul_reflection_zpow_apply_self (m : ℤ)
     match_scalars
     · linear_combination (norm := ring_nf) -S_eval_t_sub_two (m + 1)
     · ring_nf
-  | hn m ih =>
+  | pred m ih =>
     -- Apply the inductive hypothesis.
     rw [sub_eq_add_neg (-m : ℤ) 1, add_comm (-m : ℤ) (-1), zpow_add, zpow_neg_one, mul_inv_rev,
       reflection_inv, reflection_inv, LinearEquiv.mul_apply, LinearEquiv.mul_apply, ih]

Mathlib/RingTheory/Polynomial/Chebyshev.lean

@@ -498,11 +498,11 @@ theorem S_comp_two_mul_X (n : ℤ) : (S R n).comp (2 * X) = U R n := by
 
 theorem S_sq_add_S_sq (n : ℤ) : S R n ^ 2 + S R (n + 1) ^ 2 - X * S R n * S R (n + 1) = 1 := by
   induction n with
-  | hz => simp; ring
-  | hp n ih =>
+  | zero => simp; ring
+  | succ n ih =>
     have h₁ := S_add_two R n
     linear_combination (norm := ring_nf) (S R (2 + n) - S R n) * h₁ + ih
-  | hn n ih =>
+  | pred n ih =>
     have h₁ := S_sub_one R (-n)
     linear_combination (norm := ring_nf) (S R (-1 - n) - S R (1 - n)) * h₁ + ih