no goals
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x y z : α
⊢ ordSeparatingSet (↑ofDual ⁻¹' s) (↑ofDual ⁻¹' t) = ↑ofDual ⁻¹' ordSeparatingSet s t
simp only [ordSeparatingSet, mem_preimage, ← toDual.surjective.iUnion_comp, ofDual_toDual,
  dual_ordConnectedComponent, ← preimage_compl, preimage_inter, preimage_iUnion]