rw [ha, hb]
α : 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
⊢ 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 : b = has_one.one
⊢ has_one.one * has_one.one ∈ H