simp only [neq, not_true] at h
case neg
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
x : G
this : FormalSum.coords p = FormalSum.coords [(a, g)]
h :
  ¬(match g == x with
      | true => a
      | false => 0) =
      0
c : ¬x = g
neq : (g == x) = false
⊢ x = g
no goals