-- Mathlib/Algebra/Polynomial/EraseLead.lean
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

Proof state:
case succ.zero
R : Type u_1
inst✝ : Semiring R
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]
df : f.natDegree ≤ N
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = 0 → P f
f0 : #f.support = 0 + 1
⊢ f.leadingCoeff ≠ 0

Tactic:
rw [leadingCoeff_ne_zero, Ne, ← card_support_eq_zero, f0]

Result:
case succ.zero
R : Type u_1
inst✝ : Semiring R
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]
df : f.natDegree ≤ N
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = 0 → P f
f0 : #f.support = 0 + 1
⊢ ¬0 + 1 = 0

Proof state:
case succ.zero
R : Type u_1
inst✝ : Semiring R
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]
df : f.natDegree ≤ N
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = 0 → P f
f0 : #f.support = 0 + 1
⊢ ¬0 + 1 = 0

Tactic:
exact zero_ne_one.symm

Result:
no goals

Proof state:
case succ.zero
R : Type u_1
inst✝ : Semiring R
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]
df : f.natDegree ≤ N
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = 0 → P f
f0 : #f.support = 0 + 1
⊢ P (f.eraseLead + C f.leadingCoeff * X ^ f.natDegree)

Tactic:
convert P_C_mul_pow f.natDegree f.leadingCoeff ?_ df using 1

Result:
case h.e'_1
R : Type u_1
inst✝ : Semiring R
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]
df : f.natDegree ≤ N
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = 0 → P f
f0 : #f.support = 0 + 1
⊢ f.eraseLead + C f.leadingCoeff * X ^ f.natDegree = C f.leadingCoeff * X ^ f.natDegree

case succ.zero
R : Type u_1
inst✝ : Semiring R
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]
df : f.natDegree ≤ N
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = 0 → P f
f0 : #f.support = 0 + 1
⊢ f.leadingCoeff ≠ 0

Proof state:
case succ.succ
R : Type u_1
inst✝ : Semiring R
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]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → P f
f0 : #f.support = n✝ + 1 + 1
⊢ P (f.eraseLead + C f.leadingCoeff * X ^ f.natDegree)

Tactic:
refine P_C_add f.eraseLead _ ?_ ?_ ?_ ?_

Result:
case succ.succ.refine_1
R : Type u_1
inst✝ : Semiring R
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]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → P f
f0 : #f.support = n✝ + 1 + 1
⊢ f.eraseLead.natDegree < (C f.leadingCoeff * X ^ f.natDegree).natDegree

case succ.succ.refine_2
R : Type u_1
inst✝ : Semiring R
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]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → P f
f0 : #f.support = n✝ + 1 + 1
⊢ (C f.leadingCoeff * X ^ f.natDegree).natDegree ≤ N

case succ.succ.refine_3
R : Type u_1
inst✝ : Semiring R
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]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → P f
f0 : #f.support = n✝ + 1 + 1
⊢ P f.eraseLead

case succ.succ.refine_4
R : Type u_1
inst✝ : Semiring R
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]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → P f
f0 : #f.support = n✝ + 1 + 1
⊢ P (C f.leadingCoeff * X ^ f.natDegree)

Proof state:
R : Type u_1
inst✝ : Semiring R
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

Tactic:
intro f df

Result:
R : Type u_1
inst✝ : Semiring R
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]
df : f.natDegree ≤ N
⊢ P f

Proof state:
case zero
R : Type u_1
inst✝ : Semiring R
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 → #f.support = 0 → P f

Tactic:
intro f _ f0

Result:
case zero
R : Type u_1
inst✝ : Semiring R
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]
df✝ : f.natDegree ≤ N
f0 : #f.support = 0
⊢ P f

Proof state:
case succ.succ.refine_1.refine_2
R : Type u_1
inst✝ : Semiring R
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]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → P f
f0 : #f.support = n✝ + 1 + 1
⊢ f.natDegree = (C f.leadingCoeff * X ^ f.natDegree).natDegree

Tactic:
rw [natDegree_C_mul_X_pow _ _ (leadingCoeff_ne_zero.mpr _)]

Result:
R : Type u_1
inst✝ : Semiring R
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]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → P f
f0 : #f.support = n✝ + 1 + 1
⊢ f ≠ 0