have hH : H = trivial_subgroup G := by simp
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
⊢ subgroup G (trivial_subgroup G)
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
⊢ subgroup G (trivial_subgroup G)