no goals
G : Type u_1
G' : Type ?u.194712
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.194721
inst✝ : AddGroup A
H K : Subgroup G
h : Subsingleton G
x y : Subgroup G
i : G
⊢ 1 ∈ x ↔ 1 ∈ y
simp [Subgroup.one_mem]