-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem card_support_eq {n : ℕ} :
    #f.support = n ↔
      ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ i, x i ≠ 0),
        f = ∑ i, C (x i) * X ^ k i

Proof state:
case neg.h
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i : Fin n, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i : Fin n, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ x i ≠ 0

Tactic:
exact hx i

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i : Fin n, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i : Fin n, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
i : Fin (n + 1)
hi : ¬∃ i₀, i₀.castSucc = i
⊢ Function.extend Fin.castSucc x (fun x => f.leadingCoeff) i ≠ 0

Tactic:
rw [Function.extend_apply' _ _ _ hi, Ne, leadingCoeff_eq_zero, ← card_support_eq_zero, h]

Result:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i : Fin n, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i : Fin n, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
i : Fin (n + 1)
hi : ¬∃ i₀, i₀.castSucc = i
⊢ ¬n + 1 = 0

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i : Fin n, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i : Fin n, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ∃ j₀, j₀.castSucc = j
⊢ k i < Function.extend Fin.castSucc k (fun x => f.natDegree) j

Tactic:
obtain ⟨j, rfl⟩ := hj

Result:
case pos.intro
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i : Fin n, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i : Fin n, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
i j : Fin n
hij : i.castSucc < j.castSucc
⊢ k i < Function.extend Fin.castSucc k (fun x => f.natDegree) j.castSucc

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
⊢ #f.support = n ↔ ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i : Fin n, C (x i) * X ^ k i

Tactic:
refine ⟨?_, fun ⟨k, x, hk, hx, hf⟩ => hf.symm ▸ card_support_eq' k x hk.injective hx⟩

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
⊢ #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i : Fin n, C (x i) * X ^ k i

Proof state:
case neg.h.h₀
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i : Fin n, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i : Fin n, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j✝ : Fin (n + 1)
i : Fin n
hij : i.castSucc < j✝
hj : ¬∃ j₀, j₀.castSucc = j✝
j : Fin n
a✝ : j ∈ univ
hji : j ≠ i
⊢ (C (x j) * X ^ k j).coeff (k i) = 0

Tactic:
rw [coeff_C_mul, coeff_X_pow, if_neg (hk.injective.ne hji.symm), mul_zero]

Result:
no goals

Proof state:
case succ.intro.intro.intro.intro.refine_1
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i : Fin n, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i : Fin n, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
i j : Fin (n + 1)
hij : i < j
hi : i ∈ Set.range Fin.castSucc
⊢ Function.extend Fin.castSucc k (fun x => f.natDegree) i < Function.extend Fin.castSucc k (fun x => f.natDegree) j

Tactic:
obtain ⟨i, rfl⟩ := hi

Result:
case succ.intro.intro.intro.intro.refine_1.intro
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i : Fin n, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i : Fin n, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
⊢ Function.extend Fin.castSucc k (fun x => f.natDegree) i.castSucc <
    Function.extend Fin.castSucc k (fun x => f.natDegree) j

Proof state:
case intro
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i : Fin n, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i : Fin n, C (x i) * X ^ k i
i : Fin n
hi : i.castSucc = Fin.last n
⊢ False

Tactic:
exact i.castSucc_lt_last.ne hi

Result:
no goals

Proof state:
case pos.intro
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i : Fin n, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i : Fin n, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
i : Fin n
⊢ Function.extend Fin.castSucc x (fun x => f.leadingCoeff) i.castSucc ≠ 0

Tactic:
rw [Fin.strictMono_castSucc.injective.extend_apply]

Result:
case pos.intro
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i : Fin n, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i : Fin n, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
i : Fin n
⊢ x i ≠ 0

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i : Fin n, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i : Fin n, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ k i < f.natDegree

Tactic:
apply lt_natDegree_of_mem_eraseLead_support

Result:
case neg.h
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i : Fin n, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i : Fin n, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ k i ∈ f.eraseLead.support