Theorem: LO.FirstOrder.Semiformula.Operator.LE.le_inj (Logic/FirstOrder/Basic/Operator.lean)

State before:
L : Language
ξ₂ : Type u_1
n₂ : ℕ
inst✝¹ : L.Eq
inst✝ : L.LT
t₁ t₂ u₁ u₂ : Semiterm L ξ₂ n₂
⊢ op(≤).operator ![t₁, u₁] = op(≤).operator ![t₂, u₂] ↔ t₁ = t₂ ∧ u₁ = u₂
Tactic:
simp [operator, LE.sentence_eq, Eq.sentence_eq, LT.sentence_eq, Matrix.fun_eq_vec₂]
State after:
no goals