-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem card_support_eq_two :
    #f.support = 2 ↔
      ∃ (k m : ℕ) (_ : k < m) (x y : R) (_ : x ≠ 0) (_ : y ≠ 0),
        f = C x * X ^ k + C y * X ^ m

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ #f.support = 2 ↔ ∃ k m, ∃ (_ : k < m), ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), f = C x * X ^ k + C y * X ^ m

Tactic:
refine ⟨fun h => ?_, ?_⟩

Result:
case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support = 2
⊢ ∃ k m, ∃ (_ : k < m), ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), f = C x * X ^ k + C y * X ^ m

case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k m, ∃ (_ : k < m), ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), f = C x * X ^ k + C y * X ^ m) → #f.support = 2

Proof state:
case refine_1.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
k : Fin 2 → ℕ
x : Fin 2 → R
hk : StrictMono k
hx : ∀ (i : Fin 2), x i ≠ 0
h : #(∑ i : Fin 2, C (x i) * X ^ k i).support = 2
⊢ C (x (Fin.castSucc 0)) * X ^ k (Fin.castSucc 0) + C (x (Fin.last 1)) * X ^ k (Fin.last 1) =
    C (x 0) * X ^ k 0 + C (x 1) * X ^ k 1

Tactic:
rfl

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
k : Fin 2 → ℕ
x : Fin 2 → R
hk : StrictMono k
hx : ∀ (i : Fin 2), x i ≠ 0
h : #(∑ i : Fin 2, C (x i) * X ^ k i).support = 2
⊢ ∃ k_1 m,
    ∃ (_ : k_1 < m),
      ∃ x_2 y, ∃ (_ : x_2 ≠ 0) (_ : y ≠ 0), ∑ i : Fin 2, C (x i) * X ^ k i = C x_2 * X ^ k_1 + C y * X ^ m

Tactic:
refine ⟨k 0, k 1, hk Nat.zero_lt_one, x 0, x 1, hx 0, hx 1, ?_⟩

Result:
case refine_1.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
k : Fin 2 → ℕ
x : Fin 2 → R
hk : StrictMono k
hx : ∀ (i : Fin 2), x i ≠ 0
h : #(∑ i : Fin 2, C (x i) * X ^ k i).support = 2
⊢ ∑ i : Fin 2, C (x i) * X ^ k i = C (x 0) * X ^ k 0 + C (x 1) * X ^ k 1

Proof state:
case refine_1.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
k : Fin 2 → ℕ
x : Fin 2 → R
hk : StrictMono k
hx : ∀ (i : Fin 2), x i ≠ 0
h : #(∑ i : Fin 2, C (x i) * X ^ k i).support = 2
⊢ ∑ i : Fin 2, C (x i) * X ^ k i = C (x 0) * X ^ k 0 + C (x 1) * X ^ k 1

Tactic:
rw [Fin.sum_univ_castSucc, Fin.sum_univ_one]

Result:
case refine_1.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
k : Fin 2 → ℕ
x : Fin 2 → R
hk : StrictMono k
hx : ∀ (i : Fin 2), x i ≠ 0
h : #(∑ i : Fin 2, C (x i) * X ^ k i).support = 2
⊢ C (x (Fin.castSucc 0)) * X ^ k (Fin.castSucc 0) + C (x (Fin.last 1)) * X ^ k (Fin.last 1) =
    C (x 0) * X ^ k 0 + C (x 1) * X ^ k 1

Proof state:
case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k m, ∃ (_ : k < m), ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), f = C x * X ^ k + C y * X ^ m) → #f.support = 2

Tactic:
rintro ⟨k, m, hkm, x, y, hx, hy, rfl⟩

Result:
case refine_2.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
k m : ℕ
hkm : k < m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ #(C x * X ^ k + C y * X ^ m).support = 2

Proof state:
case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support = 2
⊢ ∃ k m, ∃ (_ : k < m), ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), f = C x * X ^ k + C y * X ^ m

Tactic:
obtain ⟨k, x, hk, hx, rfl⟩ := card_support_eq.mp h

Result:
case refine_1.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
k : Fin 2 → ℕ
x : Fin 2 → R
hk : StrictMono k
hx : ∀ (i : Fin 2), x i ≠ 0
h : #(∑ i : Fin 2, C (x i) * X ^ k i).support = 2
⊢ ∃ k_1 m,
    ∃ (_ : k_1 < m),
      ∃ x_2 y, ∃ (_ : x_2 ≠ 0) (_ : y ≠ 0), ∑ i : Fin 2, C (x i) * X ^ k i = C x_2 * X ^ k_1 + C y * X ^ m

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
k m : ℕ
hkm : k < m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ #(C x * X ^ k + C y * X ^ m).support = 2

Tactic:
exact card_support_binomial hkm.ne hx hy

Result:
no goals