[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
⊢ support (eraseLead f) = Finset.erase (support f) (natDegree f)
[PROOFSTEP]
simp only [eraseLead, support_erase]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
i : ℕ
⊢ coeff (eraseLead f) i = if i = natDegree f then 0 else coeff f i
[PROOFSTEP]
simp only [eraseLead, coeff_erase]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ coeff (eraseLead f) (natDegree f) = 0
[PROOFSTEP]
simp [eraseLead_coeff]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
i : ℕ
hi : i ≠ natDegree f
⊢ coeff (eraseLead f) i = coeff f i
[PROOFSTEP]
simp [eraseLead_coeff, hi]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ eraseLead 0 = 0
[PROOFSTEP]
simp only [eraseLead, erase_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
⊢ eraseLead f + ↑C (leadingCoeff f) * X ^ natDegree f = f
[PROOFSTEP]
rw [C_mul_X_pow_eq_monomial, eraseLead_add_monomial_natDegree_leadingCoeff]
[GOAL]
R✝ : Type u_1
inst✝¹ : Semiring R✝
f✝ : R✝[X]
R : Type u_2
inst✝ : Ring R
f : R[X]
⊢ f - ↑C (leadingCoeff f) * X ^ natDegree f = eraseLead f
[PROOFSTEP]
rw [C_mul_X_pow_eq_monomial, self_sub_monomial_natDegree_leadingCoeff]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
f0 : 2 ≤ card (support f)
⊢ eraseLead f ≠ 0
[PROOFSTEP]
rw [Ne, ← card_support_eq_zero, eraseLead_support]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
f0 : 2 ≤ card (support f)
⊢ ¬card (Finset.erase (support f) (natDegree f)) = 0
[PROOFSTEP]
exact (zero_lt_one.trans_le <| (tsub_le_tsub_right f0 1).trans Finset.pred_card_le_card_erase).ne.symm
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
a : ℕ
h : a ∈ support (eraseLead f)
⊢ a < natDegree f
[PROOFSTEP]
rw [eraseLead_support, mem_erase] at h
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
a : ℕ
h : a ≠ natDegree f ∧ a ∈ support f
⊢ a < natDegree f
[PROOFSTEP]
exact (le_natDegree_of_mem_supp a h.2).lt_of_ne h.1
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
⊢ card (support (eraseLead f)) < card (support f)
[PROOFSTEP]
rw [eraseLead_support]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
⊢ card (Finset.erase (support f) (natDegree f)) < card (support f)
[PROOFSTEP]
exact card_lt_card (erase_ssubset <| natDegree_mem_support_of_nonzero h)
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
c : ℕ
fc : card (support f) = c
⊢ card (support (eraseLead f)) = c - 1
[PROOFSTEP]
by_cases f0 : f = 0
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
c : ℕ
fc : card (support f) = c
f0 : f = 0
⊢ card (support (eraseLead f)) = c - 1
[PROOFSTEP]
rw [← fc, f0, eraseLead_zero, support_zero, card_empty]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
c : ℕ
fc : card (support f) = c
f0 : ¬f = 0
⊢ card (support (eraseLead f)) = c - 1
[PROOFSTEP]
rw [eraseLead_support, card_erase_of_mem (natDegree_mem_support_of_nonzero f0), fc]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
i : ℕ
r : R
⊢ eraseLead (↑(monomial i) r) = 0
[PROOFSTEP]
by_cases hr : r = 0
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
i : ℕ
r : R
hr : r = 0
⊢ eraseLead (↑(monomial i) r) = 0
[PROOFSTEP]
subst r
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
i : ℕ
⊢ eraseLead (↑(monomial i) 0) = 0
[PROOFSTEP]
simp only [monomial_zero_right, eraseLead_zero]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
i : ℕ
r : R
hr : ¬r = 0
⊢ eraseLead (↑(monomial i) r) = 0
[PROOFSTEP]
rw [eraseLead, natDegree_monomial, if_neg hr, erase_monomial]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
⊢ eraseLead (X ^ n) = 0
[PROOFSTEP]
rw [X_pow_eq_monomial, eraseLead_monomial]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
r : R
n : ℕ
⊢ eraseLead (↑C r * X ^ n) = 0
[PROOFSTEP]
rw [C_mul_X_pow_eq_monomial, eraseLead_monomial]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree q < natDegree p
⊢ eraseLead (p + q) = eraseLead p + q
[PROOFSTEP]
ext n
[GOAL]
case a
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree q < natDegree p
n : ℕ
⊢ coeff (eraseLead (p + q)) n = coeff (eraseLead p + q) n
[PROOFSTEP]
by_cases nd : n = p.natDegree
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree q < natDegree p
n : ℕ
nd : n = natDegree p
⊢ coeff (eraseLead (p + q)) n = coeff (eraseLead p + q) n
[PROOFSTEP]
rw [nd, eraseLead_coeff, if_pos (natDegree_add_eq_left_of_natDegree_lt pq).symm]
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree q < natDegree p
n : ℕ
nd : n = natDegree p
⊢ 0 = coeff (eraseLead p + q) (natDegree p)
[PROOFSTEP]
simpa using (coeff_eq_zero_of_natDegree_lt pq).symm
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree q < natDegree p
n : ℕ
nd : ¬n = natDegree p
⊢ coeff (eraseLead (p + q)) n = coeff (eraseLead p + q) n
[PROOFSTEP]
rw [eraseLead_coeff, coeff_add, coeff_add, eraseLead_coeff, if_neg, if_neg nd]
[GOAL]
case neg.hnc
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree q < natDegree p
n : ℕ
nd : ¬n = natDegree p
⊢ ¬n = natDegree (p + q)
[PROOFSTEP]
rintro rfl
[GOAL]
case neg.hnc
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree q < natDegree p
nd : ¬natDegree (p + q) = natDegree p
⊢ False
[PROOFSTEP]
exact nd (natDegree_add_eq_left_of_natDegree_lt pq)
[GOAL]
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree p < natDegree q
⊢ eraseLead (p + q) = p + eraseLead q
[PROOFSTEP]
ext n
[GOAL]
case a
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree p < natDegree q
n : ℕ
⊢ coeff (eraseLead (p + q)) n = coeff (p + eraseLead q) n
[PROOFSTEP]
by_cases nd : n = q.natDegree
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree p < natDegree q
n : ℕ
nd : n = natDegree q
⊢ coeff (eraseLead (p + q)) n = coeff (p + eraseLead q) n
[PROOFSTEP]
rw [nd, eraseLead_coeff, if_pos (natDegree_add_eq_right_of_natDegree_lt pq).symm]
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree p < natDegree q
n : ℕ
nd : n = natDegree q
⊢ 0 = coeff (p + eraseLead q) (natDegree q)
[PROOFSTEP]
simpa using (coeff_eq_zero_of_natDegree_lt pq).symm
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree p < natDegree q
n : ℕ
nd : ¬n = natDegree q
⊢ coeff (eraseLead (p + q)) n = coeff (p + eraseLead q) n
[PROOFSTEP]
rw [eraseLead_coeff, coeff_add, coeff_add, eraseLead_coeff, if_neg, if_neg nd]
[GOAL]
case neg.hnc
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree p < natDegree q
n : ℕ
nd : ¬n = natDegree q
⊢ ¬n = natDegree (p + q)
[PROOFSTEP]
rintro rfl
[GOAL]
case neg.hnc
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree p < natDegree q
nd : ¬natDegree (p + q) = natDegree q
⊢ False
[PROOFSTEP]
exact nd (natDegree_add_eq_right_of_natDegree_lt pq)
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
⊢ natDegree (eraseLead f) < natDegree f ∨ eraseLead f = 0
[PROOFSTEP]
by_cases h : f.support.card ≤ 1
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
h : card (support f) ≤ 1
⊢ natDegree (eraseLead f) < natDegree f ∨ eraseLead f = 0
[PROOFSTEP]
right
[GOAL]
case pos.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
h : card (support f) ≤ 1
⊢ eraseLead f = 0
[PROOFSTEP]
rw [← C_mul_X_pow_eq_self h]
[GOAL]
case pos.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
h : card (support f) ≤ 1
⊢ eraseLead (↑C (leadingCoeff f) * X ^ natDegree f) = 0
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
h : ¬card (support f) ≤ 1
⊢ natDegree (eraseLead f) < natDegree f ∨ eraseLead f = 0
[PROOFSTEP]
left
[GOAL]
case neg.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
h : ¬card (support f) ≤ 1
⊢ natDegree (eraseLead f) < natDegree f
[PROOFSTEP]
apply eraseLead_natDegree_lt (lt_of_not_ge h)
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
⊢ natDegree (eraseLead f) ≤ natDegree f - 1
[PROOFSTEP]
rcases f.eraseLead_natDegree_lt_or_eraseLead_eq_zero with (h | h)
[GOAL]
case inl
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
h : natDegree (eraseLead f) < natDegree f
⊢ natDegree (eraseLead f) ≤ natDegree f - 1
[PROOFSTEP]
exact Nat.le_pred_of_lt h
[GOAL]
case inr
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
h : eraseLead f = 0
⊢ natDegree (eraseLead f) ≤ natDegree f - 1
[PROOFSTEP]
simp only [h, natDegree_zero, zero_le]
[GOAL]
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
[PROOFSTEP]
intro f df
[GOAL]
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
[PROOFSTEP]
generalize hd : card f.support = c
[GOAL]
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
[PROOFSTEP]
revert f
[GOAL]
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
[PROOFSTEP]
induction' c with c hc
[GOAL]
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
[PROOFSTEP]
intro f _ f0
[GOAL]
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
[PROOFSTEP]
convert P_0
[GOAL]
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
[PROOFSTEP]
simpa [support_eq_empty, card_eq_zero] using f0
[GOAL]
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
[PROOFSTEP]
intro f df f0
[GOAL]
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
[PROOFSTEP]
rw [← eraseLead_add_C_mul_X_pow f]
[GOAL]
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)
[PROOFSTEP]
cases c
[GOAL]
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)
[PROOFSTEP]
convert P_C_mul_pow f.natDegree f.leadingCoeff ?_ df using 1
[GOAL]
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
[PROOFSTEP]
convert zero_add (C (leadingCoeff f) * X ^ f.natDegree)
[GOAL]
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
[PROOFSTEP]
rw [← card_support_eq_zero, eraseLead_card_support f0]
[GOAL]
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
[PROOFSTEP]
rw [leadingCoeff_ne_zero, Ne.def, ← card_support_eq_zero, f0]
[GOAL]
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
[PROOFSTEP]
exact zero_ne_one.symm
[GOAL]
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)
[PROOFSTEP]
refine' P_C_add f.eraseLead _ _ _ _ _
[GOAL]
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)
[PROOFSTEP]
refine' (eraseLead_natDegree_lt _).trans_le (le_of_eq _)
[GOAL]
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)
[PROOFSTEP]
exact (Nat.succ_le_succ (Nat.succ_le_succ (Nat.zero_le _))).trans f0.ge
[GOAL]
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)
[PROOFSTEP]
rw [natDegree_C_mul_X_pow _ _ (leadingCoeff_ne_zero.mpr _)]
[GOAL]
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
[PROOFSTEP]
rintro rfl
[GOAL]
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
[PROOFSTEP]
simp at f0
[GOAL]
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
[PROOFSTEP]
exact (natDegree_C_mul_X_pow_le f.leadingCoeff f.natDegree).trans df
[GOAL]
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)
[PROOFSTEP]
exact hc _ (eraseLead_natDegree_le_aux.trans df) (eraseLead_card_support f0)
[GOAL]
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)
[PROOFSTEP]
refine' P_C_mul_pow _ _ _ df
[GOAL]
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
[PROOFSTEP]
rw [Ne.def, leadingCoeff_eq_zero, ← card_support_eq_zero, f0]
[GOAL]
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
[PROOFSTEP]
exact Nat.succ_ne_zero _
[GOAL]
R : Type u_1
inst✝² : Semiring R
f : R[X]
S : Type u_2
F : Type u_3
inst✝¹ : Semiring S
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, natDegree f < k → ↑φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑φ (↑(monomial n) c)) = fu n
⊢ natDegree (↑φ p) = fu (natDegree p)
[PROOFSTEP]
refine' induction_with_natDegree_le (fun p => (φ p).natDegree = fu p.natDegree) p.natDegree (by simp [fu0]) _ _ _ rfl.le
[GOAL]
R : Type u_1
inst✝² : Semiring R
f : R[X]
S : Type u_2
F : Type u_3
inst✝¹ : Semiring S
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, natDegree f < k → ↑φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑φ (↑(monomial n) c)) = fu n
⊢ (fun p => natDegree (↑φ p) = fu (natDegree p)) 0
[PROOFSTEP]
simp [fu0]
[GOAL]
case refine'_1
R : Type u_1
inst✝² : Semiring R
f : R[X]
S : Type u_2
F : Type u_3
inst✝¹ : Semiring S
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, natDegree f < k → ↑φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑φ (↑(monomial n) c)) = fu n
⊢ ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ natDegree p → (fun p => natDegree (↑φ p) = fu (natDegree p)) (↑C r * X ^ n)
[PROOFSTEP]
intro n r r0 _
[GOAL]
case refine'_1
R : Type u_1
inst✝² : Semiring R
f : R[X]
S : Type u_2
F : Type u_3
inst✝¹ : Semiring S
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, natDegree f < k → ↑φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑φ (↑(monomial n) c)) = fu n
n : ℕ
r : R
r0 : r ≠ 0
a✝ : n ≤ natDegree p
⊢ natDegree (↑φ (↑C r * X ^ n)) = fu (natDegree (↑C r * X ^ n))
[PROOFSTEP]
rw [natDegree_C_mul_X_pow _ _ r0, C_mul_X_pow_eq_monomial, φ_mon_nat _ _ r0]
[GOAL]
case refine'_2
R : Type u_1
inst✝² : Semiring R
f : R[X]
S : Type u_2
F : Type u_3
inst✝¹ : Semiring S
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, natDegree f < k → ↑φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑φ (↑(monomial n) c)) = fu n
⊢ ∀ (f g : R[X]),
    natDegree f < natDegree g →
      natDegree g ≤ natDegree p →
        (fun p => natDegree (↑φ p) = fu (natDegree p)) f →
          (fun p => natDegree (↑φ p) = fu (natDegree p)) g → (fun p => natDegree (↑φ p) = fu (natDegree p)) (f + g)
[PROOFSTEP]
intro f g fg _ fk gk
[GOAL]
case refine'_2
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
F : Type u_3
inst✝¹ : Semiring S
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, natDegree f < k → ↑φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑φ (↑(monomial n) c)) = fu n
f g : R[X]
fg : natDegree f < natDegree g
a✝ : natDegree g ≤ natDegree p
fk : natDegree (↑φ f) = fu (natDegree f)
gk : natDegree (↑φ g) = fu (natDegree g)
⊢ natDegree (↑φ (f + g)) = fu (natDegree (f + g))
[PROOFSTEP]
rw [natDegree_add_eq_right_of_natDegree_lt fg, _root_.map_add]
[GOAL]
case refine'_2
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
F : Type u_3
inst✝¹ : Semiring S
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, natDegree f < k → ↑φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑φ (↑(monomial n) c)) = fu n
f g : R[X]
fg : natDegree f < natDegree g
a✝ : natDegree g ≤ natDegree p
fk : natDegree (↑φ f) = fu (natDegree f)
gk : natDegree (↑φ g) = fu (natDegree g)
⊢ natDegree (↑φ f + ↑φ g) = fu (natDegree g)
[PROOFSTEP]
by_cases FG : k ≤ f.natDegree
[GOAL]
case pos
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
F : Type u_3
inst✝¹ : Semiring S
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, natDegree f < k → ↑φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑φ (↑(monomial n) c)) = fu n
f g : R[X]
fg : natDegree f < natDegree g
a✝ : natDegree g ≤ natDegree p
fk : natDegree (↑φ f) = fu (natDegree f)
gk : natDegree (↑φ g) = fu (natDegree g)
FG : k ≤ natDegree f
⊢ natDegree (↑φ f + ↑φ g) = fu (natDegree g)
[PROOFSTEP]
rw [natDegree_add_eq_right_of_natDegree_lt, gk]
[GOAL]
case pos
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
F : Type u_3
inst✝¹ : Semiring S
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, natDegree f < k → ↑φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑φ (↑(monomial n) c)) = fu n
f g : R[X]
fg : natDegree f < natDegree g
a✝ : natDegree g ≤ natDegree p
fk : natDegree (↑φ f) = fu (natDegree f)
gk : natDegree (↑φ g) = fu (natDegree g)
FG : k ≤ natDegree f
⊢ natDegree (↑φ f) < natDegree (↑φ g)
[PROOFSTEP]
rw [fk, gk]
[GOAL]
case pos
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
F : Type u_3
inst✝¹ : Semiring S
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, natDegree f < k → ↑φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑φ (↑(monomial n) c)) = fu n
f g : R[X]
fg : natDegree f < natDegree g
a✝ : natDegree g ≤ natDegree p
fk : natDegree (↑φ f) = fu (natDegree f)
gk : natDegree (↑φ g) = fu (natDegree g)
FG : k ≤ natDegree f
⊢ fu (natDegree f) < fu (natDegree g)
[PROOFSTEP]
exact fc FG fg
[GOAL]
case neg
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
F : Type u_3
inst✝¹ : Semiring S
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, natDegree f < k → ↑φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑φ (↑(monomial n) c)) = fu n
f g : R[X]
fg : natDegree f < natDegree g
a✝ : natDegree g ≤ natDegree p
fk : natDegree (↑φ f) = fu (natDegree f)
gk : natDegree (↑φ g) = fu (natDegree g)
FG : ¬k ≤ natDegree f
⊢ natDegree (↑φ f + ↑φ g) = fu (natDegree g)
[PROOFSTEP]
cases k
[GOAL]
case neg.zero
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
F : Type u_3
inst✝¹ : Semiring S
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
fu : ℕ → ℕ
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑φ (↑(monomial n) c)) = fu n
f g : R[X]
fg : natDegree f < natDegree g
a✝ : natDegree g ≤ natDegree p
fk : natDegree (↑φ f) = fu (natDegree f)
gk : natDegree (↑φ g) = fu (natDegree g)
fu0 : ∀ {n : ℕ}, n ≤ Nat.zero → fu n = 0
fc : ∀ {n m : ℕ}, Nat.zero ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, natDegree f < Nat.zero → ↑φ f = 0
FG : ¬Nat.zero ≤ natDegree f
⊢ natDegree (↑φ f + ↑φ g) = fu (natDegree g)
[PROOFSTEP]
exact (FG (Nat.zero_le _)).elim
[GOAL]
case neg.succ
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
F : Type u_3
inst✝¹ : Semiring S
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
fu : ℕ → ℕ
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑φ (↑(monomial n) c)) = fu n
f g : R[X]
fg : natDegree f < natDegree g
a✝ : natDegree g ≤ natDegree p
fk : natDegree (↑φ f) = fu (natDegree f)
gk : natDegree (↑φ g) = fu (natDegree g)
n✝ : ℕ
fu0 : ∀ {n : ℕ}, n ≤ Nat.succ n✝ → fu n = 0
fc : ∀ {n m : ℕ}, Nat.succ n✝ ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, natDegree f < Nat.succ n✝ → ↑φ f = 0
FG : ¬Nat.succ n✝ ≤ natDegree f
⊢ natDegree (↑φ f + ↑φ g) = fu (natDegree g)
[PROOFSTEP]
rwa [φ_k (not_le.mp FG), zero_add]
[GOAL]
R : Type u_1
inst✝² : Semiring R
f : R[X]
S : Type u_2
F : Type u_3
inst✝¹ : Semiring S
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
φ_k : ∀ (f : R[X]), natDegree f < k → ↑φ f = 0
φ_mon : ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑φ (↑(monomial n) c)) = n - k
⊢ ∀ {n : ℕ}, n ≤ k → (fun j => j - k) n = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : Semiring R
f : R[X]
S : Type u_2
F : Type u_3
inst✝¹ : Semiring S
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑φ (↑(monomial n) c)) = n
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑φ (↑(monomial n) c)) = n - 0
[PROOFSTEP]
simpa
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
⊢ card (support (∑ i : Fin n, ↑C (x i) * X ^ k i)) = n
[PROOFSTEP]
suffices (∑ i, C (x i) * X ^ k i).support = image k univ by rw [this, univ.card_image_of_injective hk, card_fin]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
this : support (∑ i : Fin n, ↑C (x i) * X ^ k i) = image k univ
⊢ card (support (∑ i : Fin n, ↑C (x i) * X ^ k i)) = n
[PROOFSTEP]
rw [this, univ.card_image_of_injective hk, card_fin]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
⊢ support (∑ i : Fin n, ↑C (x i) * X ^ k i) = image k univ
[PROOFSTEP]
simp_rw [Finset.ext_iff, mem_support_iff, finset_sum_coeff, coeff_C_mul_X_pow, mem_image, mem_univ, true_and]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
⊢ ∀ (a : ℕ), (∑ x_1 : Fin n, if a = k x_1 then x x_1 else 0) ≠ 0 ↔ ∃ a_1, k a_1 = a
[PROOFSTEP]
refine' fun i => ⟨fun h => _, _⟩
[GOAL]
case refine'_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
i : ℕ
h : (∑ x_1 : Fin n, if i = k x_1 then x x_1 else 0) ≠ 0
⊢ ∃ a, k a = i
[PROOFSTEP]
obtain ⟨j, _, h⟩ := exists_ne_zero_of_sum_ne_zero h
[GOAL]
case refine'_1.intro.intro
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
i : ℕ
h✝ : (∑ x_1 : Fin n, if i = k x_1 then x x_1 else 0) ≠ 0
j : Fin n
left✝ : j ∈ univ
h : (if i = k j then x j else 0) ≠ 0
⊢ ∃ a, k a = i
[PROOFSTEP]
exact ⟨j, (ite_ne_right_iff.mp h).1.symm⟩
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
i : ℕ
⊢ (∃ a, k a = i) → (∑ x_1 : Fin n, if i = k x_1 then x x_1 else 0) ≠ 0
[PROOFSTEP]
rintro ⟨j, _, rfl⟩
[GOAL]
case refine'_2.intro.refl
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
j : Fin n
⊢ (∑ x_1 : Fin n, if k j = k x_1 then x x_1 else 0) ≠ 0
[PROOFSTEP]
rw [sum_eq_single_of_mem j (mem_univ j), if_pos rfl]
[GOAL]
case refine'_2.intro.refl
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
j : Fin n
⊢ x j ≠ 0
[PROOFSTEP]
exact hx j
[GOAL]
case refine'_2.intro.refl
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
j : Fin n
⊢ ∀ (b : Fin n), b ∈ univ → b ≠ j → (if k j = k b then x b else 0) = 0
[PROOFSTEP]
exact fun m _ hmj => if_neg fun h => hmj.symm (hk h)
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
⊢ card (support f) = n ↔ ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
[PROOFSTEP]
refine' ⟨_, fun ⟨k, x, hk, hx, hf⟩ => hf.symm ▸ card_support_eq' k x hk.injective hx⟩
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
⊢ card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
[PROOFSTEP]
induction' n with n hn generalizing f
[GOAL]
case zero
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
⊢ card (support f) = Nat.zero → ∃ k x hk hx, f = ∑ i : Fin Nat.zero, ↑C (x i) * X ^ k i
[PROOFSTEP]
exact fun hf => ⟨0, 0, fun x => x.elim0, fun x => x.elim0, card_support_eq_zero.mp hf⟩
[GOAL]
case succ
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
⊢ card (support f) = Nat.succ n → ∃ k x hk hx, f = ∑ i : Fin (Nat.succ n), ↑C (x i) * X ^ k i
[PROOFSTEP]
intro h
[GOAL]
case succ
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
⊢ ∃ k x hk hx, f = ∑ i : Fin (Nat.succ n), ↑C (x i) * X ^ k i
[PROOFSTEP]
obtain ⟨k, x, hk, hx, hf⟩ := hn (eraseLead_card_support' h)
[GOAL]
case succ.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
⊢ ∃ k x hk hx, f = ∑ i : Fin (Nat.succ n), ↑C (x i) * X ^ k i
[PROOFSTEP]
have H : ¬∃ k : Fin n, Fin.castSucc k = Fin.last n :=
  by
  rintro ⟨i, hi⟩
  exact i.castSucc_lt_last.ne hi
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
⊢ ¬∃ k, Fin.castSucc k = Fin.last n
[PROOFSTEP]
rintro ⟨i, hi⟩
[GOAL]
case intro
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
i : Fin n
hi : Fin.castSucc i = Fin.last n
⊢ False
[PROOFSTEP]
exact i.castSucc_lt_last.ne hi
[GOAL]
case succ.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
⊢ ∃ k x hk hx, f = ∑ i : Fin (Nat.succ n), ↑C (x i) * X ^ k i
[PROOFSTEP]
refine'
  ⟨Function.extend Fin.castSucc k fun _ => f.natDegree, Function.extend Fin.castSucc x fun _ => f.leadingCoeff, _, _, _⟩
[GOAL]
case succ.intro.intro.intro.intro.refine'_1
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
⊢ StrictMono (Function.extend Fin.castSucc k fun x => natDegree f)
[PROOFSTEP]
intro i j hij
[GOAL]
case succ.intro.intro.intro.intro.refine'_1
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
i j : Fin (Nat.succ n)
hij : i < j
⊢ Function.extend Fin.castSucc k (fun x => natDegree f) i < Function.extend Fin.castSucc k (fun x => natDegree f) j
[PROOFSTEP]
have hi : i ∈ Set.range (Fin.castSucc : Fin n → Fin (n + 1)) :=
  by
  rw [Fin.range_castSucc, Set.mem_def]
  exact lt_of_lt_of_le hij (Nat.lt_succ_iff.mp j.2)
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
i j : Fin (Nat.succ n)
hij : i < j
⊢ i ∈ Set.range Fin.castSucc
[PROOFSTEP]
rw [Fin.range_castSucc, Set.mem_def]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
i j : Fin (Nat.succ n)
hij : i < j
⊢ setOf (fun i => ↑i < n) i
[PROOFSTEP]
exact lt_of_lt_of_le hij (Nat.lt_succ_iff.mp j.2)
[GOAL]
case succ.intro.intro.intro.intro.refine'_1
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
i j : Fin (Nat.succ n)
hij : i < j
hi : i ∈ Set.range Fin.castSucc
⊢ Function.extend Fin.castSucc k (fun x => natDegree f) i < Function.extend Fin.castSucc k (fun x => natDegree f) j
[PROOFSTEP]
obtain ⟨i, rfl⟩ := hi
[GOAL]
case succ.intro.intro.intro.intro.refine'_1.intro
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
j : Fin (Nat.succ n)
i : Fin n
hij : Fin.castSucc i < j
⊢ Function.extend Fin.castSucc k (fun x => natDegree f) (Fin.castSucc i) <
    Function.extend Fin.castSucc k (fun x => natDegree f) j
[PROOFSTEP]
rw [Fin.strictMono_castSucc.injective.extend_apply]
[GOAL]
case succ.intro.intro.intro.intro.refine'_1.intro
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
j : Fin (Nat.succ n)
i : Fin n
hij : Fin.castSucc i < j
⊢ k i < Function.extend Fin.castSucc k (fun x => natDegree f) j
[PROOFSTEP]
by_cases hj : ∃ j₀, Fin.castSucc j₀ = j
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
j : Fin (Nat.succ n)
i : Fin n
hij : Fin.castSucc i < j
hj : ∃ j₀, Fin.castSucc j₀ = j
⊢ k i < Function.extend Fin.castSucc k (fun x => natDegree f) j
[PROOFSTEP]
obtain ⟨j, rfl⟩ := hj
[GOAL]
case pos.intro
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
i j : Fin n
hij : Fin.castSucc i < Fin.castSucc j
⊢ k i < Function.extend Fin.castSucc k (fun x => natDegree f) (Fin.castSucc j)
[PROOFSTEP]
rwa [Fin.strictMono_castSucc.injective.extend_apply, hk.lt_iff_lt, ← Fin.castSucc_lt_castSucc_iff]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
j : Fin (Nat.succ n)
i : Fin n
hij : Fin.castSucc i < j
hj : ¬∃ j₀, Fin.castSucc j₀ = j
⊢ k i < Function.extend Fin.castSucc k (fun x => natDegree f) j
[PROOFSTEP]
rw [Function.extend_apply' _ _ _ hj]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
j : Fin (Nat.succ n)
i : Fin n
hij : Fin.castSucc i < j
hj : ¬∃ j₀, Fin.castSucc j₀ = j
⊢ k i < natDegree f
[PROOFSTEP]
apply lt_natDegree_of_mem_eraseLead_support
[GOAL]
case neg.h
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
j : Fin (Nat.succ n)
i : Fin n
hij : Fin.castSucc i < j
hj : ¬∃ j₀, Fin.castSucc j₀ = j
⊢ k i ∈ support (eraseLead f)
[PROOFSTEP]
rw [mem_support_iff, hf, finset_sum_coeff]
[GOAL]
case neg.h
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
j : Fin (Nat.succ n)
i : Fin n
hij : Fin.castSucc i < j
hj : ¬∃ j₀, Fin.castSucc j₀ = j
⊢ ∑ b : Fin n, coeff (↑C (x b) * X ^ k b) (k i) ≠ 0
[PROOFSTEP]
rw [sum_eq_single, coeff_C_mul, coeff_X_pow_self, mul_one]
[GOAL]
case neg.h
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
j : Fin (Nat.succ n)
i : Fin n
hij : Fin.castSucc i < j
hj : ¬∃ j₀, Fin.castSucc j₀ = j
⊢ x i ≠ 0
[PROOFSTEP]
exact hx i
[GOAL]
case neg.h.h₀
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
j : Fin (Nat.succ n)
i : Fin n
hij : Fin.castSucc i < j
hj : ¬∃ j₀, Fin.castSucc j₀ = j
⊢ ∀ (b : Fin n), b ∈ univ → b ≠ i → coeff (↑C (x b) * X ^ k b) (k i) = 0
[PROOFSTEP]
intro j _ hji
[GOAL]
case neg.h.h₀
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
j✝ : Fin (Nat.succ n)
i : Fin n
hij : Fin.castSucc i < j✝
hj : ¬∃ j₀, Fin.castSucc j₀ = j✝
j : Fin n
a✝ : j ∈ univ
hji : j ≠ i
⊢ coeff (↑C (x j) * X ^ k j) (k i) = 0
[PROOFSTEP]
rw [coeff_C_mul, coeff_X_pow, if_neg (hk.injective.ne hji.symm), mul_zero]
[GOAL]
case neg.h.h₁
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
j : Fin (Nat.succ n)
i : Fin n
hij : Fin.castSucc i < j
hj : ¬∃ j₀, Fin.castSucc j₀ = j
⊢ ¬i ∈ univ → coeff (↑C (x i) * X ^ k i) (k i) = 0
[PROOFSTEP]
exact fun hi => (hi (mem_univ i)).elim
[GOAL]
case succ.intro.intro.intro.intro.refine'_2
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
⊢ ∀ (i : Fin (Nat.succ n)), Function.extend Fin.castSucc x (fun x => leadingCoeff f) i ≠ 0
[PROOFSTEP]
intro i
[GOAL]
case succ.intro.intro.intro.intro.refine'_2
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
i : Fin (Nat.succ n)
⊢ Function.extend Fin.castSucc x (fun x => leadingCoeff f) i ≠ 0
[PROOFSTEP]
by_cases hi : ∃ i₀, Fin.castSucc i₀ = i
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
i : Fin (Nat.succ n)
hi : ∃ i₀, Fin.castSucc i₀ = i
⊢ Function.extend Fin.castSucc x (fun x => leadingCoeff f) i ≠ 0
[PROOFSTEP]
obtain ⟨i, rfl⟩ := hi
[GOAL]
case pos.intro
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
i : Fin n
⊢ Function.extend Fin.castSucc x (fun x => leadingCoeff f) (Fin.castSucc i) ≠ 0
[PROOFSTEP]
rw [Fin.strictMono_castSucc.injective.extend_apply]
[GOAL]
case pos.intro
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
i : Fin n
⊢ x i ≠ 0
[PROOFSTEP]
exact hx i
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
i : Fin (Nat.succ n)
hi : ¬∃ i₀, Fin.castSucc i₀ = i
⊢ Function.extend Fin.castSucc x (fun x => leadingCoeff f) i ≠ 0
[PROOFSTEP]
rw [Function.extend_apply' _ _ _ hi, Ne, leadingCoeff_eq_zero, ← card_support_eq_zero, h]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
i : Fin (Nat.succ n)
hi : ¬∃ i₀, Fin.castSucc i₀ = i
⊢ ¬Nat.succ n = 0
[PROOFSTEP]
exact n.succ_ne_zero
[GOAL]
case succ.intro.intro.intro.intro.refine'_3
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
⊢ f =
    ∑ i : Fin (Nat.succ n),
      ↑C (Function.extend Fin.castSucc x (fun x => leadingCoeff f) i) *
        X ^ Function.extend Fin.castSucc k (fun x => natDegree f) i
[PROOFSTEP]
rw [Fin.sum_univ_castSucc]
[GOAL]
case succ.intro.intro.intro.intro.refine'_3
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
⊢ f =
    ∑ i : Fin n,
        ↑C (Function.extend Fin.castSucc x (fun x => leadingCoeff f) (Fin.castSucc i)) *
          X ^ Function.extend Fin.castSucc k (fun x => natDegree f) (Fin.castSucc i) +
      ↑C (Function.extend Fin.castSucc x (fun x => leadingCoeff f) (Fin.last n)) *
        X ^ Function.extend Fin.castSucc k (fun x => natDegree f) (Fin.last n)
[PROOFSTEP]
simp only [Fin.strictMono_castSucc.injective.extend_apply]
[GOAL]
case succ.intro.intro.intro.intro.refine'_3
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
⊢ f =
    ∑ x_1 : Fin n, ↑C (x x_1) * X ^ k x_1 +
      ↑C (Function.extend Fin.castSucc x (fun x => leadingCoeff f) (Fin.last n)) *
        X ^ Function.extend Fin.castSucc k (fun x => natDegree f) (Fin.last n)
[PROOFSTEP]
rw [← hf, Function.extend_apply', Function.extend_apply', eraseLead_add_C_mul_X_pow]
[GOAL]
case succ.intro.intro.intro.intro.refine'_3.hb
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
⊢ ¬∃ a, Fin.castSucc a = Fin.last n
case succ.intro.intro.intro.intro.refine'_3.hb
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
⊢ ¬∃ a, Fin.castSucc a = Fin.last n
[PROOFSTEP]
all_goals exact H
[GOAL]
case succ.intro.intro.intro.intro.refine'_3.hb
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
⊢ ¬∃ a, Fin.castSucc a = Fin.last n
[PROOFSTEP]
exact H
[GOAL]
case succ.intro.intro.intro.intro.refine'_3.hb
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
n : ℕ
hn : ∀ {f : R[X]}, card (support f) = n → ∃ k x hk hx, f = ∑ i : Fin n, ↑C (x i) * X ^ k i
f : R[X]
h : card (support f) = Nat.succ n
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : eraseLead f = ∑ i : Fin n, ↑C (x i) * X ^ k i
H : ¬∃ k, Fin.castSucc k = Fin.last n
⊢ ¬∃ a, Fin.castSucc a = Fin.last n
[PROOFSTEP]
exact H
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ card (support f) = 1 ↔ ∃ k x hx, f = ↑C x * X ^ k
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : card (support f) = 1
⊢ ∃ k x hx, f = ↑C x * X ^ k
[PROOFSTEP]
obtain ⟨k, x, _, hx, rfl⟩ := card_support_eq.mp h
[GOAL]
case refine'_1.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
k : Fin 1 → ℕ
x : Fin 1 → R
w✝ : StrictMono k
hx : ∀ (i : Fin 1), x i ≠ 0
h : card (support (∑ i : Fin 1, ↑C (x i) * X ^ k i)) = 1
⊢ ∃ k_1 x_1 hx, ∑ i : Fin 1, ↑C (x i) * X ^ k i = ↑C x_1 * X ^ k_1
[PROOFSTEP]
exact ⟨k 0, x 0, hx 0, Fin.sum_univ_one _⟩
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k x hx, f = ↑C x * X ^ k) → card (support f) = 1
[PROOFSTEP]
rintro ⟨k, x, hx, rfl⟩
[GOAL]
case refine'_2.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
k : ℕ
x : R
hx : x ≠ 0
⊢ card (support (↑C x * X ^ k)) = 1
[PROOFSTEP]
rw [support_C_mul_X_pow k hx, card_singleton]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ card (support f) = 2 ↔ ∃ k m hkm x y hx hy, f = ↑C x * X ^ k + ↑C y * X ^ m
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : card (support f) = 2
⊢ ∃ k m hkm x y hx hy, f = ↑C x * X ^ k + ↑C y * X ^ m
[PROOFSTEP]
obtain ⟨k, x, hk, hx, rfl⟩ := card_support_eq.mp h
[GOAL]
case refine'_1.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
k : Fin 2 → ℕ
x : Fin 2 → R
hk : StrictMono k
hx : ∀ (i : Fin 2), x i ≠ 0
h : card (support (∑ i : Fin 2, ↑C (x i) * X ^ k i)) = 2
⊢ ∃ k_1 m hkm x_1 y hx hy, ∑ i : Fin 2, ↑C (x i) * X ^ k i = ↑C x_1 * X ^ k_1 + ↑C y * X ^ m
[PROOFSTEP]
refine' ⟨k 0, k 1, hk Nat.zero_lt_one, x 0, x 1, hx 0, hx 1, _⟩
[GOAL]
case refine'_1.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
k : Fin 2 → ℕ
x : Fin 2 → R
hk : StrictMono k
hx : ∀ (i : Fin 2), x i ≠ 0
h : card (support (∑ i : Fin 2, ↑C (x i) * X ^ k i)) = 2
⊢ ∑ i : Fin 2, ↑C (x i) * X ^ k i = ↑C (x 0) * X ^ k 0 + ↑C (x 1) * X ^ k 1
[PROOFSTEP]
rw [Fin.sum_univ_castSucc, Fin.sum_univ_one]
[GOAL]
case refine'_1.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
k : Fin 2 → ℕ
x : Fin 2 → R
hk : StrictMono k
hx : ∀ (i : Fin 2), x i ≠ 0
h : card (support (∑ i : Fin 2, ↑C (x i) * X ^ k i)) = 2
⊢ ↑C (x (Fin.castSucc 0)) * X ^ k (Fin.castSucc 0) + ↑C (x (Fin.last 1)) * X ^ k (Fin.last 1) =
    ↑C (x 0) * X ^ k 0 + ↑C (x 1) * X ^ k 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k m hkm x y hx hy, f = ↑C x * X ^ k + ↑C y * X ^ m) → card (support f) = 2
[PROOFSTEP]
rintro ⟨k, m, hkm, x, y, hx, hy, rfl⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
k m : ℕ
hkm : k < m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ card (support (↑C x * X ^ k + ↑C y * X ^ m)) = 2
[PROOFSTEP]
exact card_support_binomial hkm.ne hx hy
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ card (support f) = 3 ↔ ∃ k m n hkm hmn x y z hx hy hz, f = ↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : card (support f) = 3
⊢ ∃ k m n hkm hmn x y z hx hy hz, f = ↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n
[PROOFSTEP]
obtain ⟨k, x, hk, hx, rfl⟩ := card_support_eq.mp h
[GOAL]
case refine'_1.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
k : Fin 3 → ℕ
x : Fin 3 → R
hk : StrictMono k
hx : ∀ (i : Fin 3), x i ≠ 0
h : card (support (∑ i : Fin 3, ↑C (x i) * X ^ k i)) = 3
⊢ ∃ k_1 m n hkm hmn x_1 y z hx hy hz, ∑ i : Fin 3, ↑C (x i) * X ^ k i = ↑C x_1 * X ^ k_1 + ↑C y * X ^ m + ↑C z * X ^ n
[PROOFSTEP]
refine' ⟨k 0, k 1, k 2, hk Nat.zero_lt_one, hk (Nat.lt_succ_self 1), x 0, x 1, x 2, hx 0, hx 1, hx 2, _⟩
[GOAL]
case refine'_1.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
k : Fin 3 → ℕ
x : Fin 3 → R
hk : StrictMono k
hx : ∀ (i : Fin 3), x i ≠ 0
h : card (support (∑ i : Fin 3, ↑C (x i) * X ^ k i)) = 3
⊢ ∑ i : Fin 3, ↑C (x i) * X ^ k i = ↑C (x 0) * X ^ k 0 + ↑C (x 1) * X ^ k 1 + ↑C (x 2) * X ^ k 2
[PROOFSTEP]
rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc, Fin.sum_univ_one]
[GOAL]
case refine'_1.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
k : Fin 3 → ℕ
x : Fin 3 → R
hk : StrictMono k
hx : ∀ (i : Fin 3), x i ≠ 0
h : card (support (∑ i : Fin 3, ↑C (x i) * X ^ k i)) = 3
⊢ ↑C (x (Fin.castSucc (Fin.castSucc 0))) * X ^ k (Fin.castSucc (Fin.castSucc 0)) +
        ↑C (x (Fin.castSucc (Fin.last 1))) * X ^ k (Fin.castSucc (Fin.last 1)) +
      ↑C (x (Fin.last 2)) * X ^ k (Fin.last 2) =
    ↑C (x 0) * X ^ k 0 + ↑C (x 1) * X ^ k 1 + ↑C (x 2) * X ^ k 2
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k m n hkm hmn x y z hx hy hz, f = ↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) → card (support f) = 3
[PROOFSTEP]
rintro ⟨k, m, n, hkm, hmn, x, y, z, hx, hy, hz, rfl⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ card (support (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)) = 3
[PROOFSTEP]
exact card_support_trinomial hkm hmn hx hy hz


[GOAL]
R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
⊢ (x + y) ^ 0 = x ^ 0 + ↑0 * x ^ (0 - 1) * y + 0 * y ^ 2
[PROOFSTEP]
simp
[GOAL]
R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
⊢ (x + y) ^ 1 = x ^ 1 + ↑1 * x ^ (1 - 1) * y + 0 * y ^ 2
[PROOFSTEP]
simp
[GOAL]
R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n✝ : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
n : ℕ
⊢ { k // (x + y) ^ (n + 2) = x ^ (n + 2) + ↑(n + 2) * x ^ (n + 2 - 1) * y + k * y ^ 2 }
[PROOFSTEP]
cases' (powAddExpansion x y (n + 1)) with z hz
[GOAL]
case mk
R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n✝ : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2
⊢ { k // (x + y) ^ (n + 2) = x ^ (n + 2) + ↑(n + 2) * x ^ (n + 2 - 1) * y + k * y ^ 2 }
[PROOFSTEP]
exists x * z + (n + 1) * x ^ n + z * y
[GOAL]
case mk
R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n✝ : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2
⊢ (x + y) ^ (n + 2) = x ^ (n + 2) + ↑(n + 2) * x ^ (n + 2 - 1) * y + (x * z + (↑n + 1) * x ^ n + z * y) * y ^ 2
[PROOFSTEP]
calc
  (x + y) ^ (n + 2) = (x + y) * (x + y) ^ (n + 1) := by ring
  _ = (x + y) * (x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2) := by rw [hz]
  _ = x ^ (n + 2) + ↑(n + 2) * x ^ (n + 1) * y + (x * z + (n + 1) * x ^ n + z * y) * y ^ 2 :=
    by
    push_cast
    ring!
[GOAL]
R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n✝ : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2
⊢ (x + y) ^ (n + 2) = (x + y) * (x + y) ^ (n + 1)
[PROOFSTEP]
ring
[GOAL]
R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n✝ : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2
⊢ (x + y) * (x + y) ^ (n + 1) = (x + y) * (x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2)
[PROOFSTEP]
rw [hz]
[GOAL]
R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n✝ : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2
⊢ (x + y) * (x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2) =
    x ^ (n + 2) + ↑(n + 2) * x ^ (n + 1) * y + (x * z + (↑n + 1) * x ^ n + z * y) * y ^ 2
[PROOFSTEP]
push_cast
[GOAL]
R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n✝ : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2
⊢ (x + y) * (x ^ (n + 1) + (↑n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2) =
    x ^ (n + 2) + (↑n + 2) * x ^ (n + 1) * y + (x * z + (↑n + 1) * x ^ n + z * y) * y ^ 2
[PROOFSTEP]
ring!
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a✝ b : R
m n : ℕ
inst✝ : CommRing R
x y : R
e : ℕ
a : R
⊢ { k // a * (x + y) ^ e = a * (x ^ e + ↑e * x ^ (e - 1) * y + k * y ^ 2) }
[PROOFSTEP]
exists (powAddExpansion x y e).val
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a✝ b : R
m n : ℕ
inst✝ : CommRing R
x y : R
e : ℕ
a : R
⊢ a * (x + y) ^ e = a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(powAddExpansion x y e) * y ^ 2)
[PROOFSTEP]
congr
[GOAL]
case e_a
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a✝ b : R
m n : ℕ
inst✝ : CommRing R
x y : R
e : ℕ
a : R
⊢ (x + y) ^ e = x ^ e + ↑e * x ^ (e - 1) * y + ↑(powAddExpansion x y e) * y ^ 2
[PROOFSTEP]
apply (powAddExpansion _ _ _).property
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ eval (x + y) f = sum f fun e a => a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2)
[PROOFSTEP]
unfold eval
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ eval₂ (RingHom.id R) (x + y) f =
    sum f fun e a => a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2)
[PROOFSTEP]
rw [eval₂_eq_sum]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ (sum f fun e a => ↑(RingHom.id R) a * (x + y) ^ e) =
    sum f fun e a => a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2)
[PROOFSTEP]
congr with (n z)
[GOAL]
case e_f.h.h
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
n : ℕ
z : R
⊢ ↑(RingHom.id R) z * (x + y) ^ n = z * (x ^ n + ↑n * x ^ (n - 1) * y + ↑(Polynomial.polyBinomAux1 x y n z) * y ^ 2)
[PROOFSTEP]
apply (polyBinomAux1 x y _ _).property
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ eval (x + y) f =
    ((sum f fun e a => a * x ^ e) + sum f fun e a => a * ↑e * x ^ (e - 1) * y) +
      sum f fun e a => a * ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2
[PROOFSTEP]
rw [poly_binom_aux2]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ (sum f fun e a => a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2)) =
    ((sum f fun e a => a * x ^ e) + sum f fun e a => a * ↑e * x ^ (e - 1) * y) +
      sum f fun e a => a * ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2
[PROOFSTEP]
simp [left_distrib, sum_add, mul_assoc]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ { k // eval (x + y) f = eval x f + eval x (↑derivative f) * y + k * y ^ 2 }
[PROOFSTEP]
exists f.sum fun e a => a * (polyBinomAux1 x y e a).val
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ eval (x + y) f =
    eval x f + eval x (↑derivative f) * y + (sum f fun e a => a * ↑(Polynomial.polyBinomAux1 x y e a)) * y ^ 2
[PROOFSTEP]
rw [poly_binom_aux3]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ (((sum f fun e a => a * x ^ e) + sum f fun e a => a * ↑e * x ^ (e - 1) * y) +
      sum f fun e a => a * ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2) =
    eval x f + eval x (↑derivative f) * y + (sum f fun e a => a * ↑(Polynomial.polyBinomAux1 x y e a)) * y ^ 2
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ (sum f fun e a => a * x ^ e) = eval x f
[PROOFSTEP]
rw [← eval_eq_sum]
[GOAL]
case e_a.e_a
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ (sum f fun e a => a * ↑e * x ^ (e - 1) * y) = eval x (↑derivative f) * y
[PROOFSTEP]
rw [derivative_eval]
[GOAL]
case e_a.e_a
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ (sum f fun e a => a * ↑e * x ^ (e - 1) * y) = (sum f fun n a => a * ↑n * x ^ (n - 1)) * y
[PROOFSTEP]
exact Finset.sum_mul.symm
[GOAL]
case e_a
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ (sum f fun e a => a * ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2) =
    (sum f fun e a => a * ↑(Polynomial.polyBinomAux1 x y e a)) * y ^ 2
[PROOFSTEP]
exact Finset.sum_mul.symm
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
x y : R
⊢ x ^ 0 - y ^ 0 = 0 * (x - y)
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
x y : R
⊢ x ^ 1 - y ^ 1 = 1 * (x - y)
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k✝ : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
x y : R
k : ℕ
⊢ { z // x ^ (k + 2) - y ^ (k + 2) = z * (x - y) }
[PROOFSTEP]
cases' @powSubPowFactor x y (k + 1) with z hz
[GOAL]
case mk
R : Type u
S : Type v
T : Type w
ι : Type x
k✝ : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
x y : R
k : ℕ
z : R
hz : x ^ (k + 1) - y ^ (k + 1) = z * (x - y)
⊢ { z // x ^ (k + 2) - y ^ (k + 2) = z * (x - y) }
[PROOFSTEP]
exists z * x + y ^ (k + 1)
[GOAL]
case mk
R : Type u
S : Type v
T : Type w
ι : Type x
k✝ : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
x y : R
k : ℕ
z : R
hz : x ^ (k + 1) - y ^ (k + 1) = z * (x - y)
⊢ x ^ (k + 2) - y ^ (k + 2) = (z * x + y ^ (k + 1)) * (x - y)
[PROOFSTEP]
linear_combination (norm := ring) x * hz
[GOAL]
case a
R : Type u
S : Type v
T : Type w
ι : Type x
k✝ : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
x y : R
k : ℕ
z : R
hz : x ^ (k + 1) - y ^ (k + 1) = z * (x - y)
⊢ x ^ (k + 2) - y ^ (k + 2) - (z * x + y ^ (k + 1)) * (x - y) - (x * (x ^ (k + 1) - y ^ (k + 1)) - x * (z * (x - y))) =
    0
[PROOFSTEP]
ring
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ { z // eval x f - eval y f = z * (x - y) }
[PROOFSTEP]
refine' ⟨f.sum fun i r => r * (powSubPowFactor x y i).val, _⟩
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ eval x f - eval y f = (sum f fun i r => r * ↑(powSubPowFactor x y i)) * (x - y)
[PROOFSTEP]
delta eval
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ eval₂ (RingHom.id R) x f - eval₂ (RingHom.id R) y f = (sum f fun i r => r * ↑(powSubPowFactor x y i)) * (x - y)
[PROOFSTEP]
rw [eval₂_eq_sum, eval₂_eq_sum]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ ((sum f fun e a => ↑(RingHom.id R) a * x ^ e) - sum f fun e a => ↑(RingHom.id R) a * y ^ e) =
    (sum f fun i r => r * ↑(powSubPowFactor x y i)) * (x - y)
[PROOFSTEP]
simp only [sum, ← Finset.sum_sub_distrib, Finset.sum_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ (Finset.sum (support f) fun x_1 =>
      ↑(RingHom.id R) (coeff f x_1) * x ^ x_1 - ↑(RingHom.id R) (coeff f x_1) * y ^ x_1) =
    Finset.sum (support f) fun x_1 => coeff f x_1 * ↑(powSubPowFactor x y x_1) * (x - y)
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ (Finset.sum (support f) fun x_1 => coeff f x_1 * x ^ x_1 - coeff f x_1 * y ^ x_1) =
    Finset.sum (support f) fun x_1 => coeff f x_1 * ↑(powSubPowFactor x y x_1) * (x - y)
[PROOFSTEP]
congr with i
[GOAL]
case e_f.h
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
i : ℕ
⊢ coeff f i * x ^ i - coeff f i * y ^ i = coeff f i * ↑(powSubPowFactor x y i) * (x - y)
[PROOFSTEP]
rw [mul_assoc, ← (powSubPowFactor x y _).prop, mul_sub]