Theorem: LO.FirstOrder.Structure.le_iff_of_eq_of_lt (Logic/FirstOrder/Basic/Operator.lean)

State before:
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
Tactic:
simp [Operator.LE.def_of_Eq_of_LT]
State after:
no goals