Theorem: trivialNonZeroElem_trivial_nonzero (UnitConjecture/GardamTheorem.lean)

State before:
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
⊢ ∀ (p : R[G]), trivialNonZeroElem p ↔ ∃ a, ∃ g, p = a * g ∧ a ≠ 0
Tactic:
apply Quotient.ind
State after:
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

State before:
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
Tactic:
simp only [trivialNonZeroElem_trivial_nonzeroAux, ne_eq, exists_and_right, Quotient.eq, forall_const]
State after:
no goals