no goals
L : Language
M : Type w
N : Type ?u.19040
P : Type ?u.19043
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
ι : Sort u_1
S : ι → Substructure L M
x : M
⊢ (x ∈ ⨅ (i : ι), S i) ↔ ∀ (i : ι), x ∈ S i
simp only [iInf, mem_sInf, Set.forall_range_iff]