exact
  if hz : a₀ = 0 then by
    rw [hz] at hyp₀
    rw [zero_add] at hyp₀
    have tail_coeffs : ∀ x : X, coords t x = 0 := by
      intro x
      exact
        if c : (x₀ = x) then by
          rw [← c]
          assumption
        else by
          let hx := hyp x
          simp [coords, monomCoeff] at hx
          have lf : (x₀ == x) = false := decide_eq_false c
          rw [lf] at hx
          simp [zero_add] at hx
          assumption
    have _ : t.length < (h :: t).length := by
      simp [List.length_cons]
    let step : t ≃ [] := by
      apply equiv_e_of_zero_coeffs
      exact tail_coeffs
    rw [hz]
    have ls : (0, x₀) :: t ≃ t := by
      apply Quot.sound
      apply ElementaryMove.zeroCoeff
      rfl
    exact Eq.trans ls step
  else by
    have non_zero : 0 ≠ coords t x₀ := by
      intro contra'
      let contra := Eq.symm contra'
      rw [contra, add_zero] at hyp₀
      contradiction
    let ⟨ys, eqnStep, lIneqStep⟩ := nonzero_coeff_has_complement x₀ t non_zero
    have tail_coeffs : ∀ x : X, coords ys x = 0 := by
      intro x
      exact
        if c : (x₀ = x) then by
          rw [← c]
          let ceq := coords_well_defined x₀ _ _ eqnStep
          simp [coords, monomCoeff] at ceq
          assumption
        else by
          let hx := hyp x
          simp [coords, monomCoeff] at hx
          have lf : (x₀ == x) = false := decide_eq_false c
          rw [lf] at hx
          simp [zero_add] at hx
          let ceq := coords_well_defined x _ _ eqnStep
          simp [coords, monomCoeff, lf] at ceq
          rw [hx] at ceq
          exact ceq
    have _ : ys.length < (h :: t).length := by
      simp [List.length_cons]
      apply Nat.le_trans lIneqStep
      apply Nat.le_succ
    let step : ys ≃ [] := by
      apply equiv_e_of_zero_coeffs
      exact tail_coeffs
    let eqn₁ := cons_equiv_of_equiv _ _ (coords t x₀) x₀ step
    let eqn₂ : t ≃ (coords t x₀, x₀) :: [] := Eq.trans (Eq.symm eqnStep) eqn₁
    let eqn₃ := cons_equiv_of_equiv _ _ a₀ x₀ eqn₂
    apply Eq.trans eqn₃
    have eqn₄ : sum [(a₀, x₀), (coords t x₀, x₀)] = sum [(a₀ + coords t x₀, x₀)] := by
      apply Quot.sound
      apply ElementaryMove.addCoeffs
    apply Eq.trans eqn₄
    rw [hyp₀]
    apply Quot.sound
    apply ElementaryMove.zeroCoeff
    rfl
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : a₀ + coords t x₀ = 0
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
⊢ (a₀, x₀) :: t ≃ []
no goals