intro h
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype ↥H
⊢ (∀ x ∈ H, x = 1) → ∃ x ∈ H, ∀ a ∈ H, a = x
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype ↥H
h : ∀ x ∈ H, x = 1
⊢ ∃ x ∈ H, ∀ a ∈ H, a = x