rw [whole_group]
α : Type u_1
G : group α
⊢ ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
α : Type u_1
G : group α
⊢ ∀ (a b : α),
    a ∈ { isMember := fun x => True } → b ∈ { isMember := fun x => True } → a * b ∈ { isMember := fun x => True }