From 531fb837ad92805c35f6a97e020f1286533d38b7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= <vi.hdz.p@gmail.com>
Date: Wed, 30 Oct 2024 23:06:16 -0600
Subject: [PATCH] Update Lex.lean

---
 Mathlib/Data/Prod/Lex.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Data/Prod/Lex.lean b/Mathlib/Data/Prod/Lex.lean
index b0271fecee021..bf25866214de9 100644
--- a/Mathlib/Data/Prod/Lex.lean
+++ b/Mathlib/Data/Prod/Lex.lean
@@ -50,7 +50,11 @@ theorem lt_iff [LT α] [LT β] (a b : α × β) :
     toLex a < toLex b ↔ a.1 < b.1 ∨ a.1 = b.1 ∧ a.2 < b.2 :=
   Prod.lex_def
 
-example (x : α) (y : β) : toLex (x, y) = toLex (x, y) := rfl
+theorem left_le {α β} [PartialOrder α] [LT β] {a b : α} {c d : β}
+    (h₁ : a ≤ b) (h₂ : c < d) : toLex (a, c) < toLex (b, d) := by
+  obtain h₁ | rfl := h₁.lt_or_eq
+  · exact Prod.Lex.left _ _ h₁
+  · exact Prod.Lex.right _ h₂
 
 /-- Dictionary / lexicographic preorder for pairs. -/
 instance preorder (α β : Type*) [Preorder α] [Preorder β] : Preorder (α ×ₗ β) :=