have eq₃ : s₃ ≃ s₂ := by
  have _ : ys.length + 1 < t.length + 1 := by
    apply Nat.succ_lt_succ
    exact ineqn
  apply equiv_of_equal_coeffs
  intro x
  rw [← hyp x]
  simp [coords]
  let d := coords_well_defined x _ _ eqn
  rw [coords] at d
  rw [← d]
  simp [monom_coords_hom, coords, add_assoc]
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
⊢ (a₀, x₀) :: t ≃ s₂
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : ¬0 = a₀
a₁ : R := coords t x₀
p₁ : ¬0 = a₁
ys : FormalSum R X
eqn : (coords t x₀, x₀) :: ys ≃ t
ineqn : List.length ys < List.length t
s₃ : List (R × X) := (a₀ + a₁, x₀) :: ys
eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃
eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t
eq₃ : s₃ ≃ s₂
⊢ (a₀, x₀) :: t ≃ s₂