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