no goals
α : Type u
β : Type v
γ : Type ?u.10908
f✝ g✝ : Ultrafilter α
s t : Set α
p q : α → Prop
u : Ultrafilter α
f g : Filter α
⊢ ¬↑u ≤ f ⊔ g ↔ ¬(↑u ≤ f ∨ ↑u ≤ g)
simp only [← disjoint_iff_not_le, not_or, disjoint_sup_right]