G : Type u_1
G' : Type ?u.169479
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.169488
inst✝ : AddGroup A
H✝ K H : Subgroup G
x✝ : ∃ g, ↑H = {g}
g : G
hg : ↑H = {g}
⊢ Subsingleton ↑{g}
G : Type u_1
G' : Type ?u.169479
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.169488
inst✝ : AddGroup A
H✝ K H : Subgroup G
x✝ : ∃ g, ↑H = {g}
g : G
hg : ↑H = {g}
⊢ Subsingleton ↑↑H
rw [hg]
no goals
G : Type u_1
G' : Type ?u.169479
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.169488
inst✝ : AddGroup A
H✝ K H : Subgroup G
x✝ : ∃ g, ↑H = {g}
g : G
hg : ↑H = {g}
⊢ Subsingleton ↑{g}
infer_instance