no goals
M : Type ?u.68895
N : Type ?u.68898
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_1
H : Type ?u.68910
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
x✝ : ∃ S, closure S = P ∧ Set.Finite S
S : Set G
hS : closure S = P
hf : Set.Finite S
⊢ closure ↑(Set.Finite.toFinset hf) = P
simp [hS]