intro ⟨x, hyp⟩
case mp
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
⊢ (∃! x, FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) → ∃ a, ∃ g, p ≈ [(a, g)] ∧ a ≠ 0
case mp
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
x : G
hyp :
  (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) x ∧
    ∀ (y : G), (fun x => FreeModule.coordinates x (Quotient.mk (formalSumSetoid R G) p) ≠ 0) y → y = x
⊢ ∃ a, ∃ g, p ≈ [(a, g)] ∧ a ≠ 0