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
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
refine' ⟨_, fun ⟨k, x, hk, hx, hf⟩ => hf.symm ▸ card_support_eq' k x hk.injective hx⟩
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

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
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
induction' n with n hn generalizing f
no goals
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
exact fun hf => ⟨0, 0, fun x => x.elim0, fun x => x.elim0, card_support_eq_zero.mp hf⟩
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
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
intro h
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
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
obtain ⟨k, x, hk, hx, hf⟩ := hn (eraseLead_card_support' h)
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
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
have H : ¬∃ k : Fin n, Fin.castSucc k = Fin.last n := by
  rintro ⟨i, hi⟩
  exact i.castSucc_lt_last.ne hi
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)

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

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
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
refine'
  ⟨Function.extend Fin.castSucc k fun _ => f.natDegree,
    Function.extend Fin.castSucc x fun _ => f.leadingCoeff, _, _, _⟩
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
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
rintro ⟨i, hi⟩
no goals
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
exact i.castSucc_lt_last.ne hi
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
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)
intro i j hij
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
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
have hi : i ∈ Set.range (Fin.castSucc : Fin n ↪o 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)
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
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
obtain ⟨i, rfl⟩ := hi
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
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
rw [Fin.castSucc.injective.extend_apply]
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

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
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
by_cases hj : ∃ j₀, Fin.castSucc j₀ = j
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
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
rw [Fin.range_castSucc, Set.mem_def]
no goals
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
exact lt_of_lt_of_le hij (Nat.lt_succ_iff.mp j.2)
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)
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
obtain ⟨j, rfl⟩ := hj
no goals
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)
rwa [Fin.castSucc.injective.extend_apply, hk.lt_iff_lt, ← Fin.castSucc_lt_castSucc_iff]
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
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
rw [Function.extend_apply' _ _ _ hj]
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)
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
apply lt_natDegree_of_mem_eraseLead_support
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
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)
rw [mem_support_iff, hf, finset_sum_coeff]
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

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

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
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
rw [sum_eq_single, coeff_C_mul, coeff_X_pow_self, mul_one]
no goals
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
exact hx i
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
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
intro j _ hji
no goals
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
rw [coeff_C_mul, coeff_X_pow, if_neg (hk.injective.ne hji.symm), mul_zero]
no goals
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
exact fun hi => (hi (mem_univ i)).elim
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
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
intro i
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

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
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
by_cases hi : ∃ i₀, Fin.castSucc i₀ = i
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
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
obtain ⟨i, rfl⟩ := hi
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
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
rw [Fin.castSucc.injective.extend_apply]
no goals
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
exact hx i
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
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
rw [Function.extend_apply' _ _ _ hi, Ne, leadingCoeff_eq_zero, ← card_support_eq_zero, h]
no goals
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
exact n.succ_ne_zero
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)
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
rw [Fin.sum_univ_castSucc]
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)
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)
simp only [Fin.castSucc.injective.extend_apply]
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
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)
rw [← hf, Function.extend_apply', Function.extend_apply', eraseLead_add_C_mul_X_pow]
no goals
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
all_goals exact H
no goals
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
exact H