rw [trivial_subgroup, Membership.mem, instMembershipSet]
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : b = has_one.one
⊢ has_one.one ∈ trivial_subgroup G
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : b = has_one.one
⊢ { mem := fun x s => Set.isMember x }.1 has_one.one { isMember := fun x => x = has_one.one }