G : Type u_1
G' : Type ?u.168605
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.168614
inst✝¹ : AddGroup A
H K : Subgroup G
inst✝ : Subsingleton { x // x ∈ H }
⊢ ∀ (x : G), x ∈ H → x = 1
G : Type u_1
G' : Type ?u.168605
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.168614
inst✝¹ : AddGroup A
H K : Subgroup G
inst✝ : Subsingleton { x // x ∈ H }
⊢ H = ⊥
rw [Subgroup.eq_bot_iff_forall]
G : Type u_1
G' : Type ?u.168605
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.168614
inst✝¹ : AddGroup A
H K : Subgroup G
inst✝ : Subsingleton { x // x ∈ H }
y : G
hy : y ∈ H
⊢ y = 1
G : Type u_1
G' : Type ?u.168605
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.168614
inst✝¹ : AddGroup A
H K : Subgroup G
inst✝ : Subsingleton { x // x ∈ H }
⊢ ∀ (x : G), x ∈ H → x = 1
intro y hy
no goals
G : Type u_1
G' : Type ?u.168605
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.168614
inst✝¹ : AddGroup A
H K : Subgroup G
inst✝ : Subsingleton { x // x ∈ H }
y : G
hy : y ∈ H
⊢ y = 1
rw [← Subgroup.coe_mk H y hy, Subsingleton.elim (⟨y, hy⟩ : H) 1, Subgroup.coe_one]