no goals
G : Type u_1
G' : Type ?u.147239
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.147248
inst✝ : AddGroup A
H K : Subgroup G
g : G
h : g ∈ H
⊢ { val := g, property := h } = { val := 1, property := (_ : 1 ∈ H) } ↔ g = 1
simp