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