simp only [trivialNonZeroElem_trivial_nonzeroAux, ne_eq, exists_and_right, Quotient.eq, forall_const]
case a
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
⊢ ∀ (a : FormalSum R G),
    trivialNonZeroElem (Quotient.mk (formalSumSetoid R G) a) ↔
      ∃ a_1, ∃ g, Quotient.mk (formalSumSetoid R G) a = a_1 * g ∧ a_1 ≠ 0
no goals