simp [zero_add] at hx
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₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
x : X
c : ¬x₀ = x
hx :
  (match false with
      | true => a₀
      | false => 0) +
      coords t x =
    0
lf : (x₀ == x) = false
⊢ coords ys x = 0
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₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
x : X
c : ¬x₀ = x
lf : (x₀ == x) = false
hx : coords t x = 0
⊢ coords ys x = 0