no goals
α : Type u_1
β : Type ?u.7392
inst✝ : Preorder α
a b : α
h✝ : Compares lt a b
h : lt = eq
⊢ a = b
injection h
no goals
α : Type u_1
β : Type ?u.7392
inst✝ : Preorder α
a b : α
h✝ : Compares gt a b
h : gt = eq
⊢ a = b
injection h