calc x = y := hy' x hx
_      = 1 := (hy' 1 H.one_mem).symm
case mpr.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype ↥H
y : G
hy' : ∀ a ∈ H, a = y
x : G
hx : x ∈ H
⊢ x = 1
no goals