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