no goals
G : Type u_2
G' : Type ?u.215948
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.215957
inst✝ : AddGroup A
H K : Subgroup G
k : Set G
ι : Sort u_1
p : ι → Subgroup G
⊢ (⨆ (i : ι), p i) = closure (⋃ (i : ι), ↑(p i))
simp_rw [closure_iUnion, closure_eq]