chore: fix two sets of induction recursor names (#29537)

Both in `Algebra.Polynomial`. We also deprime `induction` in the same files.

These were split off from #29291.

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>

Author: Parcly-Taxel

Mathlib/Algebra/Polynomial/EraseLead.lean

@@ -259,38 +259,35 @@ theorem nextCoeff_eq_zero_of_eraseLead_eq_zero (h : f.eraseLead = 0) : f.nextCoe
 end EraseLead
 
 /-- An induction lemma for polynomials. It takes a natural number `N` as a parameter, that is
-required to be at least as big as the `nat_degree` of the polynomial.  This is useful to prove
+required to be at least as big as the `natDegree` of the polynomial.  This is useful to prove
 results where you want to change each term in a polynomial to something else depending on the
-`nat_degree` of the polynomial itself and not on the specific `nat_degree` of each term. -/
-theorem induction_with_natDegree_le (P : R[X] → Prop) (N : ℕ) (P_0 : P 0)
-    (P_C_mul_pow : ∀ n : ℕ, ∀ r : R, r ≠ 0 → n ≤ N → P (C r * X ^ n))
-    (P_C_add : ∀ f g : R[X], f.natDegree < g.natDegree → g.natDegree ≤ N → P f → P g → P (f + g)) :
-    ∀ f : R[X], f.natDegree ≤ N → P f := by
-  intro f df
-  generalize hd : #f.support = c
-  revert f
-  induction' c with c hc
-  · intro f _ f0
-    convert P_0
-    simpa [support_eq_empty, card_eq_zero] using f0
-  · intro f df f0
+`natDegree` of the polynomial itself and not on the specific `natDegree` of each term. -/
+theorem induction_with_natDegree_le (motive : R[X] → Prop) (N : ℕ) (zero : motive 0)
+    (C_mul_pow : ∀ n : ℕ, ∀ r : R, r ≠ 0 → n ≤ N → motive (C r * X ^ n))
+    (add : ∀ f g : R[X], f.natDegree < g.natDegree → g.natDegree ≤ N →
+      motive f → motive g → motive (f + g)) (f : R[X]) (df : f.natDegree ≤ N) : motive f := by
+  induction hf : #f.support generalizing f with
+  | zero =>
+    convert zero
+    simpa [support_eq_empty, card_eq_zero] using hf
+  | succ c hc =>
     rw [← eraseLead_add_C_mul_X_pow f]
     cases c
-    · convert P_C_mul_pow f.natDegree f.leadingCoeff ?_ df using 1
+    · convert C_mul_pow f.natDegree f.leadingCoeff ?_ df using 1
       · convert zero_add (C (leadingCoeff f) * X ^ f.natDegree)
-        rw [← card_support_eq_zero, card_support_eraseLead' f0]
-      · rw [leadingCoeff_ne_zero, Ne, ← card_support_eq_zero, f0]
+        rw [← card_support_eq_zero, card_support_eraseLead' hf]
+      · rw [leadingCoeff_ne_zero, Ne, ← card_support_eq_zero, hf]
         exact zero_ne_one.symm
-    refine P_C_add f.eraseLead _ ?_ ?_ ?_ ?_
+    refine add f.eraseLead _ ?_ ?_ ?_ ?_
     · refine (eraseLead_natDegree_lt ?_).trans_le (le_of_eq ?_)
-      · exact (Nat.succ_le_succ (Nat.succ_le_succ (Nat.zero_le _))).trans f0.ge
+      · exact (Nat.succ_le_succ (Nat.succ_le_succ (Nat.zero_le _))).trans hf.ge
       · rw [natDegree_C_mul_X_pow _ _ (leadingCoeff_ne_zero.mpr _)]
         rintro rfl
-        simp at f0
+        simp at hf
     · exact (natDegree_C_mul_X_pow_le f.leadingCoeff f.natDegree).trans df
-    · exact hc _ (eraseLead_natDegree_le_aux.trans df) (card_support_eraseLead' f0)
-    · refine P_C_mul_pow _ _ ?_ df
-      rw [Ne, leadingCoeff_eq_zero, ← card_support_eq_zero, f0]
+    · exact hc _ (eraseLead_natDegree_le_aux.trans df) (card_support_eraseLead' hf)
+    · refine C_mul_pow _ _ ?_ df
+      rw [Ne, leadingCoeff_eq_zero, ← card_support_eq_zero, hf]
       exact Nat.succ_ne_zero _
 
 /-- Let `φ : R[x] → S[x]` be an additive map, `k : ℕ` a bound, and `fu : ℕ → ℕ` a

Mathlib/Algebra/Polynomial/Laurent.lean

@@ -354,20 +354,20 @@ theorem exists_T_pow (f : R[T;T⁻¹]) : ∃ (n : ℕ) (f' : R[X]), toLaurent f'
 
 /-- This is a version of `exists_T_pow` stated as an induction principle. -/
 @[elab_as_elim]
-theorem induction_on_mul_T {Q : R[T;T⁻¹] → Prop} (f : R[T;T⁻¹])
-    (Qf : ∀ {f : R[X]} {n : ℕ}, Q (toLaurent f * T (-n))) : Q f := by
+theorem induction_on_mul_T {motive : R[T;T⁻¹] → Prop} (f : R[T;T⁻¹])
+    (mul_T : ∀ (f : R[X]) (n : ℕ), motive (toLaurent f * T (-n))) : motive f := by
   rcases f.exists_T_pow with ⟨n, f', hf⟩
   rw [← mul_one f, ← T_zero, ← Nat.cast_zero, ← Nat.sub_self n, Nat.cast_sub rfl.le, T_sub,
     ← mul_assoc, ← hf]
-  exact Qf
+  exact mul_T ..
 
 /-- Suppose that `Q` is a statement about Laurent polynomials such that
 * `Q` is true on *ordinary* polynomials;
 * `Q (f * T)` implies `Q f`;
 it follow that `Q` is true on all Laurent polynomials. -/
 theorem reduce_to_polynomial_of_mul_T (f : R[T;T⁻¹]) {Q : R[T;T⁻¹] → Prop}
     (Qf : ∀ f : R[X], Q (toLaurent f)) (QT : ∀ f, Q (f * T 1) → Q f) : Q f := by
-  induction' f using LaurentPolynomial.induction_on_mul_T with f n
+  induction f using LaurentPolynomial.induction_on_mul_T with | _ f n
   induction n with
   | zero => simpa only [Nat.cast_zero, neg_zero, T_zero, mul_one] using Qf _
   | succ n hn => convert QT _ _; simpa using hn
@@ -501,8 +501,8 @@ instance isLocalization : IsLocalization.Away (X : R[X]) R[T;T⁻¹] :=
       obtain ⟨n, rfl⟩ := ht
       rw [algebraMap_eq_toLaurent, toLaurent_X_pow]
       exact isUnit_T ↑n
-    surj' := fun f => by
-      induction' f using LaurentPolynomial.induction_on_mul_T with f n
+    surj' f := by
+      induction f using LaurentPolynomial.induction_on_mul_T with | _ f n
       have : X ^ n ∈ Submonoid.powers (X : R[X]) := ⟨n, rfl⟩
       refine ⟨(f, ⟨_, this⟩), ?_⟩
       simp only [algebraMap_eq_toLaurent, toLaurent_X_pow, mul_T_assoc, neg_add_cancel, T_zero,