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

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

Tactic:
rfl

Result:
no goals

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

Tactic:
rintro ⟨k, m, n, hkm, hmn, x, y, z, hx, hy, hz, rfl⟩

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

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

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

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

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

Tactic:
rw [Fin.sum_univ_castSucc, 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 3 → ℕ
x : Fin 3 → R
hk : StrictMono k
hx : ∀ (i : Fin 3), x i ≠ 0
h : #(∑ i : Fin 3, C (x i) * X ^ k i).support = 3
⊢ C (x (Fin.castSucc 0).castSucc) * X ^ k (Fin.castSucc 0).castSucc +
        C (x (Fin.last 1).castSucc) * X ^ k (Fin.last 1).castSucc +
      C (x (Fin.last 2)) * X ^ k (Fin.last 2) =
    C (x 0) * X ^ k 0 + C (x 1) * X ^ k 1 + C (x 2) * X ^ k 2

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

Tactic:
exact card_support_trinomial hkm hmn hx hy hz

Result:
no goals

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

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

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

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

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

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 3 → ℕ
x : Fin 3 → R
hk : StrictMono k
hx : ∀ (i : Fin 3), x i ≠ 0
h : #(∑ i : Fin 3, C (x i) * X ^ k i).support = 3
⊢ ∃ k_1 m n,
    ∃ (_ : k_1 < m) (_ : m < n),
      ∃ x_3 y z,
        ∃ (_ : x_3 ≠ 0) (_ : y ≠ 0) (_ : z ≠ 0),
          ∑ i : Fin 3, C (x i) * X ^ k i = C x_3 * X ^ k_1 + C y * X ^ m + C z * X ^ n