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 : α
⊢ (s₁ ∪ s₂) ○ t = s₁ ○ t ∪ s₂ ○ t
simp [disjSups, filter_union, image_union]