simp [Operator.LE.def_of_Eq_of_LT]
L : Language
M : Type u_1
inst✝⁵ : Structure L M
inst✝⁴ : Operator.Eq L
inst✝³ : Operator.LT L
inst✝² : LT M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
a b : M
⊢ op(≤).val ![a, b] ↔ a = b ∨ a < b
no goals