no goals
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ {a} ○ {b} = if Disjoint a b then {a ⊔ b} else ∅
split_ifs with h <;> simp [disjSups, filter_singleton, h]