feat(Data/Finsupp/MonomialOrder) : lexicographic order on Unique (#20699)

Two lemmas for lexicographic order on a`Unique` type are added.

Author: AntoineChambert-Loir

Mathlib/Data/Finsupp/Lex.lean

@@ -46,6 +46,16 @@ theorem lex_eq_invImage_dfinsupp_lex (r : α → α → Prop) (s : N → N → P
 instance [LT α] [LT N] : LT (Lex (α →₀ N)) :=
   ⟨fun f g ↦ Finsupp.Lex (· < ·) (· < ·) (ofLex f) (ofLex g)⟩
 
+theorem lex_lt_iff [LT α] [LT N] {a b : Lex (α →₀ N)} :
+    a < b ↔ ∃ i, (∀ j, j < i → ofLex a j = ofLex b j) ∧ ofLex a i < ofLex b i :=
+  Finsupp.lex_def
+
+theorem lex_lt_iff_of_unique [Preorder α] [LT N] [Unique α] {a b : Lex (α →₀ N)} :
+    a < b ↔ ofLex a default < ofLex b default := by
+  simp only [lex_lt_iff, Unique.exists_iff, and_iff_right_iff_imp]
+  refine fun _ j hj ↦ False.elim (lt_irrefl j ?_)
+  simpa only [Unique.uniq] using hj
+
 theorem lex_lt_of_lt_of_preorder [Preorder N] (r) [IsStrictOrder α r] {x y : α →₀ N} (hlt : x < y) :
     ∃ i, (∀ j, r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i :=
   DFinsupp.lex_lt_of_lt_of_preorder r (id hlt : x.toDFinsupp < y.toDFinsupp)
@@ -104,6 +114,13 @@ theorem lt_of_forall_lt_of_lt (a b : Lex (α →₀ N)) (i : α) :
     (∀ j < i, ofLex a j = ofLex b j) → ofLex a i < ofLex b i → a < b :=
   fun h1 h2 ↦ ⟨i, h1, h2⟩
 
+theorem lex_le_iff_of_unique [Unique α] {a b : Lex (α →₀ N)} :
+    a ≤ b ↔ ofLex a default ≤ ofLex b default := by
+  simp only [le_iff_eq_or_lt, EmbeddingLike.apply_eq_iff_eq]
+  apply or_congr _ lex_lt_iff_of_unique
+  conv_lhs => rw [← toLex_ofLex a, ← toLex_ofLex b, toLex_inj]
+  simp only [Finsupp.ext_iff, Unique.forall_iff]
+
 end NHasZero
 
 section Covariants

Mathlib/Data/Finsupp/MonomialOrder.lean

@@ -113,16 +113,6 @@ noncomputable instance {α N : Type*} [LinearOrder α] [OrderedCancelAddCommMono
   le_of_add_le_add_left a b c h := by simpa only [add_le_add_iff_left] using h
   add_le_add_left a b h c := by simpa only [add_le_add_iff_left] using h
 
-theorem Finsupp.lex_lt_iff {α N : Type*} [LinearOrder α] [LinearOrder N] [Zero N]
-    {a b : Lex (α →₀ N)} :
-    a < b ↔ ∃ i, (∀ j, j< i → ofLex a j = ofLex b j) ∧ ofLex a i < ofLex b i :=
-    Finsupp.lex_def
-
-theorem Finsupp.lex_le_iff {α N : Type*} [LinearOrder α] [LinearOrder N] [Zero N]
-    {a b : Lex (α →₀ N)} :
-    a ≤ b ↔ a = b ∨ ∃ i, (∀ j, j< i → ofLex a j = ofLex b j) ∧ ofLex a i < ofLex b i := by
-    rw [le_iff_eq_or_lt, Finsupp.lex_lt_iff]
-
 /-- for the lexicographic ordering, X 0 * X 1 < X 0  ^ 2 -/
 example : toLex (Finsupp.single 0 2) > toLex (Finsupp.single 0 1 + Finsupp.single 1 1) := by
   use 0; simp
@@ -152,4 +142,12 @@ theorem MonomialOrder.lex_le_iff [WellFoundedGT σ] {c d : σ →₀ ℕ} :
 theorem MonomialOrder.lex_lt_iff [WellFoundedGT σ] {c d : σ →₀ ℕ} :
     c ≺[lex] d ↔ toLex c < toLex d := Iff.rfl
 
+theorem MonomialOrder.lex_lt_iff_of_unique [Unique σ] {c d : σ →₀ ℕ} :
+    c ≺[lex] d ↔ c default < d default := by
+  simp only [MonomialOrder.lex_lt_iff, Finsupp.lex_lt_iff_of_unique, ofLex_toLex]
+
+theorem MonomialOrder.lex_le_iff_of_unique [Unique σ] {c d : σ →₀ ℕ} :
+    c ≼[lex] d ↔ c default ≤ d default := by
+  simp only [MonomialOrder.lex_le_iff, Finsupp.lex_le_iff_of_unique, ofLex_toLex]
+
 end Lex