no goals
α : Type u_1
β : Type ?u.78350
γ : Type ?u.78353
ι : Sort ?u.78356
κ : ι → Sort ?u.78361
inst✝ : LE α
S : Set (LowerSet α)
s t : LowerSet α
a : α
⊢ Disjoint ↑s ↑t ↔ Disjoint s t
simp [disjoint_iff, SetLike.ext'_iff]