case refine'_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : card (support f) = 2
⊢ ∃ k m hkm x y hx hy, f = ↑C x * X ^ k + ↑C y * X ^ m

case refine'_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k m hkm x y hx hy, f = ↑C x * X ^ k + ↑C y * X ^ m) → card (support f) = 2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ card (support f) = 2 ↔ ∃ k m hkm x y hx hy, f = ↑C x * X ^ k + ↑C y * X ^ m
refine' ⟨fun h => _, _⟩
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 : card (support (∑ i : Fin 2, ↑C (x i) * X ^ k i)) = 2
⊢ ∃ k_1 m hkm x_1 y hx hy, ∑ i : Fin 2, ↑C (x i) * X ^ k i = ↑C x_1 * X ^ k_1 + ↑C y * X ^ m
case refine'_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : card (support f) = 2
⊢ ∃ k m hkm x y hx hy, f = ↑C x * X ^ k + ↑C y * X ^ m
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 2 → ℕ
x : Fin 2 → R
hk : StrictMono k
hx : ∀ (i : Fin 2), x i ≠ 0
h : card (support (∑ i : Fin 2, ↑C (x i) * X ^ k i)) = 2
⊢ ∑ i : Fin 2, ↑C (x i) * X ^ k i = ↑C (x 0) * X ^ k 0 + ↑C (x 1) * X ^ k 1
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 : card (support (∑ i : Fin 2, ↑C (x i) * X ^ k i)) = 2
⊢ ∃ k_1 m hkm x_1 y hx hy, ∑ i : Fin 2, ↑C (x i) * X ^ k i = ↑C x_1 * X ^ k_1 + ↑C y * X ^ m
refine' ⟨k 0, k 1, hk Nat.zero_lt_one, x 0, x 1, hx 0, hx 1, _⟩
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 : card (support (∑ i : Fin 2, ↑C (x i) * X ^ k i)) = 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
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 : card (support (∑ i : Fin 2, ↑C (x i) * X ^ k i)) = 2
⊢ ∑ i : Fin 2, ↑C (x i) * X ^ k i = ↑C (x 0) * X ^ k 0 + ↑C (x 1) * X ^ k 1
rw [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 2 → ℕ
x : Fin 2 → R
hk : StrictMono k
hx : ∀ (i : Fin 2), x i ≠ 0
h : card (support (∑ i : Fin 2, ↑C (x i) * X ^ k i)) = 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
rfl
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
⊢ card (support (↑C x * X ^ k + ↑C y * X ^ m)) = 2
case refine'_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k m hkm x y hx hy, f = ↑C x * X ^ k + ↑C y * X ^ m) → card (support f) = 2
rintro ⟨k, m, hkm, x, y, hx, hy, rfl⟩
no goals
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
⊢ card (support (↑C x * X ^ k + ↑C y * X ^ m)) = 2
exact card_support_binomial hkm.ne hx hy