no goals
α : Type u_1
β : Type ?u.62085
γ : Type ?u.62088
ι : Sort u_2
ι' : Sort ?u.62094
l l' : Filter α
p : ι → Prop
s✝ : ι → Set α
t✝ : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
s : ι → Set α
h : Directed (fun x x_1 => x ≥ x_1) s
inst✝ : Nonempty ι
t : Set α
⊢ (t ∈ ⨅ (i : ι), 𝓟 (s i)) ↔ ∃ i, True ∧ s i ⊆ t
simpa only [true_and] using mem_iInf_of_directed (h.mono_comp monotone_principal.dual) t