no goals
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
s : Set β
f : β → α
⊢ DirectedOn r (f '' s) ↔ DirectedOn (f ⁻¹'o r) s
simp only [DirectedOn, Set.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp,
  forall_apply_eq_imp_iff₂, Order.Preimage]