no goals
G : Type u_2
G' : Type ?u.188842
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.188851
inst✝ : AddGroup A
H K : Subgroup G
ι : Sort u_1
S : ι → Subgroup G
⊢ ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)
simp only [iInf, coe_sInf, Set.biInter_range]