-- 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.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)

Tactic:
refine P_C_mul_pow _ _ ?_ df

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

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

Tactic:
exact hc _ (eraseLead_natDegree_le_aux.trans df) (card_support_eraseLead' f0)

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

Tactic:
intro f df f0

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

Proof state:
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
f0 : #f.support = 0
⊢ f = 0

Tactic:
simpa [support_eq_empty, card_eq_zero] using 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)
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

Tactic:
simp at 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
⊢ P f

Tactic:
generalize hd : #f.support = c

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
c : ℕ
hd : #f.support = c
⊢ P f

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

Tactic:
refine (eraseLead_natDegree_lt ?_).trans_le (le_of_eq ?_)

Result:
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

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

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]
df✝ : f.natDegree ≤ N
f0 : #f.support = 0
⊢ P f

Tactic:
convert P_0

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
f0 : #f.support = 0
⊢ f = 0

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

Tactic:
convert zero_add (C (leadingCoeff f) * X ^ f.natDegree)

Result:
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

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
c : ℕ
hd : #f.support = c
⊢ P f

Tactic:
revert f

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