case refine'_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : card (support f) = 3
⊢ ∃ k m n hkm hmn x y z hx hy hz, 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 hkm hmn x y z hx hy hz, f = ↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) → card (support f) = 3
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ card (support f) = 3 ↔ ∃ k m n hkm hmn x y z hx hy hz, f = ↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n
refine' ⟨fun h => _, _⟩
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 : card (support (∑ i : Fin 3, ↑C (x i) * X ^ k i)) = 3
⊢ ∃ k_1 m n hkm hmn x_1 y z hx hy hz, ∑ i : Fin 3, ↑C (x i) * X ^ k i = ↑C x_1 * X ^ k_1 + ↑C y * X ^ m + ↑C z * X ^ n
case refine'_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : card (support f) = 3
⊢ ∃ k m n hkm hmn x y z hx hy hz, f = ↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n
obtain ⟨k, x, hk, hx, rfl⟩ := card_support_eq.mp h
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 : card (support (∑ i : Fin 3, ↑C (x i) * X ^ k i)) = 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
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 : card (support (∑ i : Fin 3, ↑C (x i) * X ^ k i)) = 3
⊢ ∃ k_1 m n hkm hmn x_1 y z hx hy hz, ∑ i : Fin 3, ↑C (x i) * X ^ k i = ↑C x_1 * X ^ k_1 + ↑C y * X ^ m + ↑C z * X ^ n
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,
    _⟩
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 : card (support (∑ i : Fin 3, ↑C (x i) * X ^ k i)) = 3
⊢ ↑C (x (↑Fin.castSucc (↑Fin.castSucc 0))) * X ^ k (↑Fin.castSucc (↑Fin.castSucc 0)) +
        ↑C (x (↑Fin.castSucc (Fin.last 1))) * X ^ k (↑Fin.castSucc (Fin.last 1)) +
      ↑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
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 : card (support (∑ i : Fin 3, ↑C (x i) * X ^ k i)) = 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
rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc, Fin.sum_univ_one]
no goals
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 : card (support (∑ i : Fin 3, ↑C (x i) * X ^ k i)) = 3
⊢ ↑C (x (↑Fin.castSucc (↑Fin.castSucc 0))) * X ^ k (↑Fin.castSucc (↑Fin.castSucc 0)) +
        ↑C (x (↑Fin.castSucc (Fin.last 1))) * X ^ k (↑Fin.castSucc (Fin.last 1)) +
      ↑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
rfl
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
⊢ card (support (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)) = 3
case refine'_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k m n hkm hmn x y z hx hy hz, f = ↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) → card (support f) = 3
rintro ⟨k, m, n, hkm, hmn, x, y, z, hx, hy, hz, rfl⟩
no goals
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
⊢ card (support (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)) = 3
exact card_support_trinomial hkm hmn hx hy hz