-- 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:
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)
c : ℕ
⊢ ∀ (f : R[X]), f.natDegree ≤ N → #f.support = c → P f

Tactic:
induction' c with c hc

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]), f.natDegree ≤ N → #f.support = 0 → P f

case 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)
c : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = c → P f
⊢ ∀ (f : R[X]), f.natDegree ≤ N → #f.support = c + 1 → P f

Proof state:
case h.e'_2.h.e'_5
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 = 0

Tactic:
rw [← card_support_eq_zero, card_support_eraseLead' f0]

Result:
no goals

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]
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

Tactic:
rintro rfl

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

Proof state:
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
⊢ ¬n✝ + 1 + 1 = 0

Tactic:
exact Nat.succ_ne_zero _

Result:
no goals

Proof state:
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

Tactic:
exact (natDegree_C_mul_X_pow_le f.leadingCoeff f.natDegree).trans df

Result:
no goals

Proof state:
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
⊢ f.leadingCoeff ≠ 0

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

Result:
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
⊢ ¬n✝ + 1 + 1 = 0

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

Tactic:
cases c

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
⊢ P (f.eraseLead + C f.leadingCoeff * X ^ f.natDegree)

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)

Proof state:
case succ.succ.refine_1.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
⊢ 2 ≤ #f.support

Tactic:
exact (Nat.succ_le_succ (Nat.succ_le_succ (Nat.zero_le _))).trans f0.ge

Result:
no goals

Proof state:
case 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)
c : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = c → P f
f : R[X]
df : f.natDegree ≤ N
f0 : #f.support = c + 1
⊢ P f

Tactic:
rw [← eraseLead_add_C_mul_X_pow f]

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