no goals
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort ?u.8073
inst✝ : Frame α
s t : Set α
a b : α
f : ι → α
⊢ Disjoint a (⨆ (i : ι), f i) ↔ ∀ (i : ι), Disjoint a (f i)
simpa only [disjoint_comm] using @iSup_disjoint_iff