case cons head tail _ =>
  simp [mul, mulMonom]
  apply funext ; intro x₀
  simp [coords]
  rw [monom_coords_at_zero]
  rw [zero_add]
  rw [← append_coords]
  simp [coords, mul]
  let l := mul_monom_zero h x₀ tail
  rw [l]
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
h : G
t : FormalSum R G
head : R × G
tail : List (R × G)
tail_ih✝ : mul tail ((0, h) :: t) ≈ mul tail t
⊢ mul (head :: tail) ((0, h) :: t) ≈ mul (head :: tail) t
no goals