rintro ⟨y, -, hy'⟩ x hx
case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype ↥H
⊢ (∃ x ∈ H, ∀ a ∈ H, a = x) → ∀ x ∈ H, x = 1
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