exact
  if p₁ : 0 = a₁ then by
    have cf₂ : s₂.coords x₀ = a₀ := by
      rw [← hyp]
      simp [coords, ← p₁, Nat.add_zero, monomCoeff]
    let ⟨ys, eqn, _⟩ :=
      nonzero_coeff_has_complement x₀ s₂
        (by
          rw [cf₂]
          assumption)
    let cfs := fun x => coords_well_defined x _ _ eqn
    rw [cf₂] at cfs
    let cfs' := fun (x : X) => Eq.trans (hyp x) (Eq.symm (cfs x))
    simp [coords] at cfs'
    have _ : t.length < (h :: t).length := by
      simp [List.length_cons]
    let step := equiv_of_equal_coeffs t ys cfs'
    let _step' := cons_equiv_of_equiv t ys a₀ x₀ step
    rw [cf₂] at eqn
    exact Eq.trans _step' eqn
  else by
    let ⟨ys, eqn, ineqn⟩ := nonzero_coeff_has_complement x₀ t p₁
    let s₃ := (a₀ + a₁, x₀) :: ys
    have eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃ := by
      apply Quot.sound
      let lem := ElementaryMove.addCoeffs a₀ a₁ x₀ ys
      exact lem
    have eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t := by
      apply cons_equiv_of_equiv
      assumption
    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]
    apply Eq.trans (Eq.trans (Eq.symm eq₂) eq₁) eq₃
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₀
⊢ (a₀, x₀) :: t ≃ s₂
no goals