-- 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_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 =
    ∑ x_1 : Fin n, C (x x_1) * X ^ k x_1 +
      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)

Tactic:
rw [← hf, Function.extend_apply', Function.extend_apply', eraseLead_add_C_mul_X_pow]

Result:
case succ.intro.intro.intro.intro.refine_3.hb
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
⊢ ¬∃ a, a.castSucc = Fin.last n

case succ.intro.intro.intro.intro.refine_3.hb
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
⊢ ¬∃ a, a.castSucc = Fin.last n

Proof state:
case succ.intro.intro.intro.intro.refine_3.hb
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
⊢ ¬∃ a, a.castSucc = Fin.last n

Tactic:
exact H

Result:
no goals

Proof state:
case succ.intro.intro.intro.intro.refine_3.hb
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
⊢ ¬∃ a, a.castSucc = Fin.last n

case succ.intro.intro.intro.intro.refine_3.hb
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
⊢ ¬∃ a, a.castSucc = Fin.last n

Tactic:
all_goals exact H

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
⊢ x i ≠ 0

Tactic:
exact hx i

Result:
no goals

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

Tactic:
simp only [Fin.strictMono_castSucc.injective.extend_apply]

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 =
    ∑ x_1 : Fin n, C (x x_1) * X ^ k x_1 +
      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 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

Tactic:
by_cases hi : ∃ i₀, Fin.castSucc i₀ = i

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
i : Fin (n + 1)
hi : ∃ i₀, i₀.castSucc = i
⊢ Function.extend Fin.castSucc x (fun x => f.leadingCoeff) i ≠ 0

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

Proof state:
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
⊢ i ∈ Set.range Fin.castSucc

Tactic:
rw [Fin.range_castSucc, Set.mem_def]

Result:
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
⊢ {i | ↑i < n} i