induction h with
| zeroCoeff tail x a hyp =>
  simp [coords, hyp, monom_coords_at_zero]
| addCoeffs a b x tail =>
  simp [coords, monom_coords_at_zero, ← add_assoc, monom_coords_hom]
| cons a x s₁ s₂ _ step =>
  simp [coords, step]
| swap a₁ a₂ x₁ x₂ tail =>
  simp [coords, ← add_assoc, add_comm]
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
s₁ s₂ : FormalSum R X
h : ElementaryMove R X s₁ s₂
⊢ coords s₁ x₀ = coords s₂ x₀
no goals