no goals
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t u v : Finset α
⊢ s ○ (t ○ u) = t ○ (s ○ u)
simp_rw [← disjSups_assoc, disjSups_comm s]