no goals
L : Language
M : Type w
N : Type ?u.19468
P : Type ?u.19471
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
ι : Sort u_1
S : ι → Substructure L M
⊢ ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)
simp only [iInf, coe_sInf, Set.biInter_range]