induction s with
| nil => 
simp [mulMonom, coords]
| cons head tail ih => 
  let (a, g) := head
  simp [mulMonom, coords]
  rw [left_distrib]
  rw [monom_coords_hom]
  rw [ih]
  conv =>
    lhs
    rw [add_assoc]
    arg 2
    rw [← add_assoc]
    congr
    rw [add_comm]    
  conv =>
    rhs
    rw [add_assoc]
  conv =>
    rhs 
    arg 2
    skip 
    rw [← add_assoc]
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
s : FormalSum R G
⊢ coords (mulMonom (b₁ + b₂) h s) x₀ = coords (mulMonom b₁ h s) x₀ + coords (mulMonom b₂ h s) x₀
no goals