have hinv_mem : ∀ a : α, a ∈ whole_group → G.inv a ∈ whole_group := by
  intros a _
  rw [Membership.mem, instMembershipSet]
  simp
  rw [Set.isMember, whole_group]
  simp
α : Type u_1
G : group α
hmul_mem : ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
hone_mem : has_one.one ∈ whole_group
⊢ subgroup G whole_group
α : Type u_1
G : group α
hmul_mem : ∀ (a b : α), a ∈ whole_group → b ∈ whole_group → a * b ∈ whole_group
hone_mem : has_one.one ∈ whole_group
hinv_mem : ∀ (a : α), a ∈ whole_group → group.inv a ∈ whole_group
⊢ subgroup G whole_group