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