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

Tactic:
by_cases hj : ∃ j₀, Fin.castSucc j₀ = j

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

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

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

Tactic:
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)

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

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 j : Fin n
hij : i.castSucc < j.castSucc
⊢ k i < Function.extend Fin.castSucc k (fun x => f.natDegree) j.castSucc

Tactic:
rwa [Fin.strictMono_castSucc.injective.extend_apply, hk.lt_iff_lt,
  ← Fin.castSucc_lt_castSucc_iff]

Result:
no goals

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
⊢ k i ∈ f.eraseLead.support

Tactic:
rw [mem_support_iff, hf, finset_sum_coeff]

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
⊢ ∑ b : Fin n, (C (x b) * X ^ k b).coeff (k i) ≠ 0

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

Tactic:
intro i j hij

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
i j : Fin (n + 1)
hij : i < j
⊢ Function.extend Fin.castSucc k (fun x => f.natDegree) i < Function.extend Fin.castSucc k (fun x => f.natDegree) j

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

Tactic:
intro h

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

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

Tactic:
obtain ⟨k, x, hk, hx, hf⟩ := hn (card_support_eraseLead' h)

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