no goals
α : Type u_1
ι : Sort ?u.5784
κ : ι → Sort ?u.5789
inst✝¹ inst✝ : PartialOrder α
c : ClosureOperator α
x y : α
hy : closed c y
⊢ ↑c.toOrderHom x ≤ y ↔ x ≤ y
rw [← c.closure_eq_self_of_mem_closed hy, ← le_closure_iff]