R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
⊢ P f
R : Type u_1
inst✝ : Semiring R
f : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
⊢ ∀ (f : R[X]), natDegree f ≤ N → P f
intro f df
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
c : ℕ
hd : card (support f) = c
⊢ P f
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
⊢ P f
generalize hd : card f.support = c
R : Type u_1
inst✝ : Semiring R
f : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
c : ℕ
⊢ ∀ (f : R[X]), natDegree f ≤ N → card (support f) = c → P f
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
c : ℕ
hd : card (support f) = c
⊢ P f
revert f
case zero
R : Type u_1
inst✝ : Semiring R
f : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
⊢ ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.zero → P f

case succ
R : Type u_1
inst✝ : Semiring R
f : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
c : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = c → P f
⊢ ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.succ c → P f
R : Type u_1
inst✝ : Semiring R
f : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
c : ℕ
⊢ ∀ (f : R[X]), natDegree f ≤ N → card (support f) = c → P f
induction' c with c hc
case zero
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df✝ : natDegree f ≤ N
f0 : card (support f) = Nat.zero
⊢ P f
case zero
R : Type u_1
inst✝ : Semiring R
f : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
⊢ ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.zero → P f
intro f _ f0
case h.e'_1
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df✝ : natDegree f ≤ N
f0 : card (support f) = Nat.zero
⊢ f = 0
case zero
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df✝ : natDegree f ≤ N
f0 : card (support f) = Nat.zero
⊢ P f
convert P_0
no goals
case h.e'_1
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df✝ : natDegree f ≤ N
f0 : card (support f) = Nat.zero
⊢ f = 0
simpa [support_eq_empty, card_eq_zero] using f0
case succ
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
c : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = c → P f
f : R[X]
df : natDegree f ≤ N
f0 : card (support f) = Nat.succ c
⊢ P f
case succ
R : Type u_1
inst✝ : Semiring R
f : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
c : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = c → P f
⊢ ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.succ c → P f
intro f df f0
case succ
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
c : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = c → P f
f : R[X]
df : natDegree f ≤ N
f0 : card (support f) = Nat.succ c
⊢ P (eraseLead f + ↑C (leadingCoeff f) * X ^ natDegree f)
case succ
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
c : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = c → P f
f : R[X]
df : natDegree f ≤ N
f0 : card (support f) = Nat.succ c
⊢ P f
rw [← eraseLead_add_C_mul_X_pow f]
case succ.zero
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.zero → P f
f0 : card (support f) = Nat.succ Nat.zero
⊢ P (eraseLead f + ↑C (leadingCoeff f) * X ^ natDegree f)

case succ.succ
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.succ n✝ → P f
f0 : card (support f) = Nat.succ (Nat.succ n✝)
⊢ P (eraseLead f + ↑C (leadingCoeff f) * X ^ natDegree f)
case succ
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
c : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = c → P f
f : R[X]
df : natDegree f ≤ N
f0 : card (support f) = Nat.succ c
⊢ P (eraseLead f + ↑C (leadingCoeff f) * X ^ natDegree f)
cases c
case succ.succ.refine'_1
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.succ n✝ → P f
f0 : card (support f) = Nat.succ (Nat.succ n✝)
⊢ natDegree (eraseLead f) < natDegree (↑C (leadingCoeff f) * X ^ natDegree f)

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

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

case succ.succ.refine'_4
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.succ n✝ → P f
f0 : card (support f) = Nat.succ (Nat.succ n✝)
⊢ P (↑C (leadingCoeff f) * X ^ natDegree f)
case succ.succ
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.succ n✝ → P f
f0 : card (support f) = Nat.succ (Nat.succ n✝)
⊢ P (eraseLead f + ↑C (leadingCoeff f) * X ^ natDegree f)
refine' P_C_add f.eraseLead _ _ _ _ _
case h.e'_1
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.zero → P f
f0 : card (support f) = Nat.succ Nat.zero
⊢ eraseLead f + ↑C (leadingCoeff f) * X ^ natDegree f = ↑C (leadingCoeff f) * X ^ natDegree f

case succ.zero
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.zero → P f
f0 : card (support f) = Nat.succ Nat.zero
⊢ leadingCoeff f ≠ 0
case succ.zero
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.zero → P f
f0 : card (support f) = Nat.succ Nat.zero
⊢ P (eraseLead f + ↑C (leadingCoeff f) * X ^ natDegree f)
convert P_C_mul_pow f.natDegree f.leadingCoeff ?_ df using 1
case h.e'_2.h.e'_5
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.zero → P f
f0 : card (support f) = Nat.succ Nat.zero
⊢ eraseLead f = 0
case h.e'_1
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.zero → P f
f0 : card (support f) = Nat.succ Nat.zero
⊢ eraseLead f + ↑C (leadingCoeff f) * X ^ natDegree f = ↑C (leadingCoeff f) * X ^ natDegree f
convert zero_add (C (leadingCoeff f) * X ^ f.natDegree)
no goals
case h.e'_2.h.e'_5
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.zero → P f
f0 : card (support f) = Nat.succ Nat.zero
⊢ eraseLead f = 0
rw [← card_support_eq_zero, eraseLead_card_support f0]
case succ.zero
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.zero → P f
f0 : card (support f) = Nat.succ Nat.zero
⊢ ¬Nat.succ Nat.zero = 0
case succ.zero
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.zero → P f
f0 : card (support f) = Nat.succ Nat.zero
⊢ leadingCoeff f ≠ 0
rw [leadingCoeff_ne_zero, Ne.def, ← card_support_eq_zero, f0]
no goals
case succ.zero
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.zero → P f
f0 : card (support f) = Nat.succ Nat.zero
⊢ ¬Nat.succ Nat.zero = 0
exact zero_ne_one.symm
case succ.succ.refine'_1.refine'_1
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.succ n✝ → P f
f0 : card (support f) = Nat.succ (Nat.succ n✝)
⊢ 2 ≤ card (support f)

case succ.succ.refine'_1.refine'_2
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.succ n✝ → P f
f0 : card (support f) = Nat.succ (Nat.succ n✝)
⊢ natDegree f = natDegree (↑C (leadingCoeff f) * X ^ natDegree f)
case succ.succ.refine'_1
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.succ n✝ → P f
f0 : card (support f) = Nat.succ (Nat.succ n✝)
⊢ natDegree (eraseLead f) < natDegree (↑C (leadingCoeff f) * X ^ natDegree f)
refine' (eraseLead_natDegree_lt _).trans_le (le_of_eq _)
no goals
case succ.succ.refine'_1.refine'_1
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.succ n✝ → P f
f0 : card (support f) = Nat.succ (Nat.succ n✝)
⊢ 2 ≤ card (support f)
exact (Nat.succ_le_succ (Nat.succ_le_succ (Nat.zero_le _))).trans f0.ge
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.succ n✝ → P f
f0 : card (support f) = Nat.succ (Nat.succ n✝)
⊢ f ≠ 0
case succ.succ.refine'_1.refine'_2
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.succ n✝ → P f
f0 : card (support f) = Nat.succ (Nat.succ n✝)
⊢ natDegree f = natDegree (↑C (leadingCoeff f) * X ^ natDegree f)
rw [natDegree_C_mul_X_pow _ _ (leadingCoeff_ne_zero.mpr _)]
R : Type u_1
inst✝ : Semiring R
f : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
n✝ : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.succ n✝ → P f
df : natDegree 0 ≤ N
f0 : card (support 0) = Nat.succ (Nat.succ n✝)
⊢ False
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.succ n✝ → P f
f0 : card (support f) = Nat.succ (Nat.succ n✝)
⊢ f ≠ 0
rintro rfl
no goals
R : Type u_1
inst✝ : Semiring R
f : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
n✝ : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.succ n✝ → P f
df : natDegree 0 ≤ N
f0 : card (support 0) = Nat.succ (Nat.succ n✝)
⊢ False
simp at f0
no goals
case succ.succ.refine'_2
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.succ n✝ → P f
f0 : card (support f) = Nat.succ (Nat.succ n✝)
⊢ natDegree (↑C (leadingCoeff f) * X ^ natDegree f) ≤ N
exact (natDegree_C_mul_X_pow_le f.leadingCoeff f.natDegree).trans df
no goals
case succ.succ.refine'_3
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.succ n✝ → P f
f0 : card (support f) = Nat.succ (Nat.succ n✝)
⊢ P (eraseLead f)
exact hc _ (eraseLead_natDegree_le_aux.trans df) (eraseLead_card_support f0)
case succ.succ.refine'_4
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.succ n✝ → P f
f0 : card (support f) = Nat.succ (Nat.succ n✝)
⊢ leadingCoeff f ≠ 0
case succ.succ.refine'_4
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.succ n✝ → P f
f0 : card (support f) = Nat.succ (Nat.succ n✝)
⊢ P (↑C (leadingCoeff f) * X ^ natDegree f)
refine' P_C_mul_pow _ _ _ df
case succ.succ.refine'_4
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.succ n✝ → P f
f0 : card (support f) = Nat.succ (Nat.succ n✝)
⊢ ¬Nat.succ (Nat.succ n✝) = 0
case succ.succ.refine'_4
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.succ n✝ → P f
f0 : card (support f) = Nat.succ (Nat.succ n✝)
⊢ leadingCoeff f ≠ 0
rw [Ne.def, leadingCoeff_eq_zero, ← card_support_eq_zero, f0]
no goals
case succ.succ.refine'_4
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
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]), natDegree f < natDegree g → natDegree g ≤ N → P f → P g → P (f + g)
f : R[X]
df : natDegree f ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), natDegree f ≤ N → card (support f) = Nat.succ n✝ → P f
f0 : card (support f) = Nat.succ (Nat.succ n✝)
⊢ ¬Nat.succ (Nat.succ n✝) = 0
exact Nat.succ_ne_zero _