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