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 : α
⊢ c ∈ s ○ t ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = c
simp [disjSups, and_assoc]