have hmul_mem : ∀ a b : α, a ∈ H → b ∈ H → a * b ∈ H := by
  intros a b ha hb
  rw [Membership.mem, instMembershipSet] at ha
  simp at ha
  rw [Set.isMember, trivial_subgroup] at ha
  simp at ha
  rw [Membership.mem, instMembershipSet] at hb
  simp at hb
  rw [Set.isMember, trivial_subgroup] at hb
  simp at hb
  rw [ha, hb]
  rw [G.mul_one]
  simp
  rw [trivial_subgroup, Membership.mem, instMembershipSet]
  simp
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
⊢ subgroup G H
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
⊢ subgroup G H