-- 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 succ.intro.intro.intro.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
⊢ ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin (n + 1)), x i ≠ 0), f = ∑ i : Fin (n + 1), C (x i) * X ^ k i

Tactic:
refine
  ⟨Function.extend Fin.castSucc k fun _ => f.natDegree,
    Function.extend Fin.castSucc x fun _ => f.leadingCoeff, ?_, ?_, ?_⟩

Result:
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
⊢ StrictMono (Function.extend Fin.castSucc k fun x => f.natDegree)

case succ.intro.intro.intro.intro.refine_2
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)), Function.extend Fin.castSucc x (fun x => f.leadingCoeff) i ≠ 0

case succ.intro.intro.intro.intro.refine_3
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
⊢ f =
    ∑ i : Fin (n + 1),
      C (Function.extend Fin.castSucc x (fun x => f.leadingCoeff) i) *
        X ^ Function.extend Fin.castSucc k (fun x => f.natDegree) i

Proof state:
case succ.intro.intro.intro.intro.refine_3
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
⊢ f =
    ∑ i : Fin (n + 1),
      C (Function.extend Fin.castSucc x (fun x => f.leadingCoeff) i) *
        X ^ Function.extend Fin.castSucc k (fun x => f.natDegree) i

Tactic:
rw [Fin.sum_univ_castSucc]

Result:
case succ.intro.intro.intro.intro.refine_3
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
⊢ f =
    ∑ i : Fin n,
        C (Function.extend Fin.castSucc x (fun x => f.leadingCoeff) i.castSucc) *
          X ^ Function.extend Fin.castSucc k (fun x => f.natDegree) i.castSucc +
      C (Function.extend Fin.castSucc x (fun x => f.leadingCoeff) (Fin.last n)) *
        X ^ Function.extend Fin.castSucc k (fun x => f.natDegree) (Fin.last n)

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
⊢ ¬n + 1 = 0

Tactic:
exact n.succ_ne_zero

Result:
no goals

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
⊢ ∀ b ∈ univ, b ≠ i → (C (x b) * X ^ k b).coeff (k i) = 0

Tactic:
intro j _ hji

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

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
⊢ i ∉ univ → (C (x i) * X ^ k i).coeff (k i) = 0

Tactic:
exact fun hi => (hi (mem_univ i)).elim

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
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:
rw [Function.extend_apply' _ _ _ hj]

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
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ k i < f.natDegree