apply And.intro
case h
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
⊢ (fun x => ¬FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) = 0) g ∧
    ∀ (y : G), (fun x => ¬FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) = 0) y → y = g
case h.left
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
⊢ (fun x => ¬FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) = 0) g

case h.right
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
⊢ ∀ (y : G), (fun x => ¬FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) = 0) y → y = g