no goals
ι : Type ?u.4759
α✝ : Type u
β : Type v
γ : Type w
π : ι → Type ?u.4770
r : α✝ → α✝ → Prop
α : Type u_1
inst✝ : PartialOrder α
x y : α
⊢ x ≤ y → y = x ↔ ¬x < y
rw [lt_iff_le_and_ne, not_and, Classical.not_not, eq_comm]