feat: CoeFun for Lex and Colex (#30481)

If `F` is a function type, we should be able to treat `Lex F` as a function type too. This diminishes the visual clutter of going to and from `Lex`.

This design was already present for pi types, but wasn't accounted for with neither of `DFinsupp` or `Finsupp`.

Author: vihdzp

Mathlib/Data/DFinsupp/Lex.lean

@@ -36,11 +36,15 @@ theorem _root_.Pi.lex_eq_dfinsupp_lex {r : ι → ι → Prop} {s : ∀ i, α i
 
 theorem lex_def {r : ι → ι → Prop} {s : ∀ i, α i → α i → Prop} {a b : Π₀ i, α i} :
     DFinsupp.Lex r s a b ↔ ∃ j, (∀ d, r d j → a d = b d) ∧ s j (a j) (b j) :=
-  Iff.rfl
+  .rfl
 
 instance [LT ι] [∀ i, LT (α i)] : LT (Lex (Π₀ i, α i)) :=
   ⟨fun f g ↦ DFinsupp.Lex (· < ·) (fun _ ↦ (· < ·)) (ofLex f) (ofLex g)⟩
 
+theorem lex_lt_iff [LT ι] [∀ i, LT (α i)] {a b : Lex (Π₀ i, α i)} :
+    a < b ↔ ∃ i, (∀ j, j < i → a j = b j) ∧ a i < b i :=
+  .rfl
+
 theorem lex_lt_of_lt_of_preorder [∀ i, Preorder (α i)] (r) [IsStrictOrder ι r] {x y : Π₀ i, α i}
     (hlt : x < y) : ∃ i, (∀ j, r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i := by
   obtain ⟨hle, j, hlt⟩ := Pi.lt_def.1 hlt
@@ -117,6 +121,7 @@ theorem toLex_monotone : Monotone (@toLex (Π₀ i, α i)) := by
     fun j hj ↦ notMem_neLocus.1 fun h ↦ (Finset.min'_le _ _ h).not_gt hj,
     (h _).lt_of_ne (mem_neLocus.1 <| Finset.min'_mem _ _)⟩
 
+@[deprecated lex_lt_iff (since := "2025-10-12")]
 theorem lt_of_forall_lt_of_lt (a b : Lex (Π₀ i, α i)) (i : ι) :
     (∀ j < i, ofLex a j = ofLex b j) → ofLex a i < ofLex b i → a < b :=
   fun h1 h2 ↦ ⟨i, h1, h2⟩

Mathlib/Data/Finsupp/Lex.lean

@@ -36,7 +36,7 @@ theorem _root_.Pi.lex_eq_finsupp_lex {r : α → α → Prop} {s : N → N → P
 
 theorem lex_def {r : α → α → Prop} {s : N → N → Prop} {a b : α →₀ N} :
     Finsupp.Lex r s a b ↔ ∃ j, (∀ d, r d j → a d = b d) ∧ s (a j) (b j) :=
-  Iff.rfl
+  .rfl
 
 theorem lex_eq_invImage_dfinsupp_lex (r : α → α → Prop) (s : N → N → Prop) :
     Finsupp.Lex r s = InvImage (DFinsupp.Lex r fun _ ↦ s) toDFinsupp :=
@@ -46,11 +46,11 @@ 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
+    a < b ↔ ∃ i, (∀ j, j < i → a j = b j) ∧ a i < b i :=
+  .rfl
 
 theorem lex_lt_iff_of_unique [Preorder α] [LT N] [Unique α] {a b : Lex (α →₀ N)} :
-    a < b ↔ ofLex a default < ofLex b default := by
+    a < b ↔ a default < 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
@@ -84,7 +84,7 @@ instance Lex.linearOrder [LinearOrder N] : LinearOrder (Lex (α →₀ N)) where
   le := (· ≤ ·)
   __ := LinearOrder.lift' (toLex ∘ toDFinsupp ∘ ofLex) finsuppEquivDFinsupp.injective
 
-theorem Lex.single_strictAnti : StrictAnti (fun (a : α) ↦ toLex (single a 1)) := by
+theorem Lex.single_strictAnti : StrictAnti fun (a : α) ↦ toLex (single a 1) := by
   intro a b h
   simp only [LT.lt, Finsupp.lex_def]
   simp only [ofLex_toLex, Nat.lt_eq]
@@ -100,20 +100,21 @@ theorem Lex.single_lt_iff {a b : α} : toLex (single b 1) < toLex (single a 1) 
 theorem Lex.single_le_iff {a b : α} : toLex (single b 1) ≤ toLex (single a 1) ↔ a ≤ b :=
   Lex.single_strictAnti.le_iff_ge
 
-theorem Lex.single_antitone : Antitone (fun (a : α) ↦ toLex (single a 1)) :=
+theorem Lex.single_antitone : Antitone fun (a : α) ↦ toLex (single a 1) :=
   Lex.single_strictAnti.antitone
 
 variable [PartialOrder N]
 
 theorem toLex_monotone : Monotone (@toLex (α →₀ N)) :=
-  fun a b h ↦ DFinsupp.toLex_monotone (id h : ∀ i, ofLex (toDFinsupp a) i ≤ ofLex (toDFinsupp b) i)
+  fun a b h ↦ DFinsupp.toLex_monotone (id h : ∀ i, (toDFinsupp a) i ≤ (toDFinsupp b) i)
 
+@[deprecated lex_lt_iff (since := "2025-10-12")]
 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
+    a ≤ b ↔ a default ≤ b default := by
   simp only [le_iff_eq_or_lt]
   apply or_congr _ lex_lt_iff_of_unique
   conv_lhs => rw [← toLex_ofLex a, ← toLex_ofLex b, toLex_inj]
@@ -151,7 +152,7 @@ variable [AddRightStrictMono N]
 
 instance Lex.addRightStrictMono : AddRightStrictMono (Lex (α →₀ N)) :=
   ⟨fun f _ _ ⟨a, lta, ha⟩ ↦
-    ⟨a, fun j ja ↦ congr_arg (· + ofLex f j) (lta j ja), add_lt_add_right ha _⟩⟩
+    ⟨a, fun j ja ↦ congr_arg (· + f j) (lta j ja), add_lt_add_right ha _⟩⟩
 
 instance Lex.addRightMono : AddRightMono (Lex (α →₀ N)) :=
   addRightMono_of_addRightStrictMono _

Mathlib/Order/PiLex.lean

@@ -49,14 +49,6 @@ basic API, just in case -/
 /-- The notation `Πₗ i, α i` refers to a pi type equipped with the lexicographic order. -/
 notation3 (prettyPrint := false) "Πₗ " (...) ", " r:(scoped p => Lex (∀ i, p i)) => r
 
-@[simp]
-theorem toLex_apply (x : ∀ i, β i) (i : ι) : toLex x i = x i :=
-  rfl
-
-@[simp]
-theorem ofLex_apply (x : Lex (∀ i, β i)) (i : ι) : ofLex x i = x i :=
-  rfl
-
 theorem lex_lt_of_lt_of_preorder [∀ i, Preorder (β i)] {r} (hwf : WellFounded r) {x y : ∀ i, β i}
     (hlt : x < y) : ∃ i, (∀ j, r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i :=
   let h' := Pi.lt_def.1 hlt
@@ -90,6 +82,16 @@ instance [LT ι] [∀ a, LT (β a)] : LT (Lex (∀ i, β i)) :=
 instance [LT ι] [∀ a, LT (β a)] : LT (Colex (∀ i, β i)) :=
   ⟨Pi.Lex (· > ·) (· < ·)⟩
 
+-- If `Lex` and `Colex` are ever made into one-field structures, we need a `CoeFun` instance.
+-- This will make `x i` syntactically equal to `ofLex x i` for `x : Πₗ i, α i`, thus making
+-- the following theorems redundant.
+
+@[simp] theorem toLex_apply (x : ∀ i, β i) (i : ι) : toLex x i = x i := rfl
+@[simp] theorem ofLex_apply (x : Lex (∀ i, β i)) (i : ι) : ofLex x i = x i := rfl
+
+@[simp] theorem toColex_apply (x : ∀ i, β i) (i : ι) : toColex x i = x i := rfl
+@[simp] theorem ofColex_apply (x : Colex (∀ i, β i)) (i : ι) : ofColex x i = x i := rfl
+
 instance Lex.isStrictOrder [LinearOrder ι] [∀ a, PartialOrder (β a)] :
     IsStrictOrder (Lex (∀ i, β i)) (· < ·) where
   irrefl := fun a ⟨k, _, hk₂⟩ => lt_irrefl (a k) hk₂

Mathlib/Order/Synonym.lean

@@ -177,6 +177,9 @@ instance (α : Type*) [DecidableEq α] : DecidableEq (Lex α) :=
 instance (α : Type*) [Inhabited α] : Inhabited (Lex α) :=
   inferInstanceAs (Inhabited α)
 
+instance {α γ} [H : CoeFun α γ] : CoeFun (Lex α) γ where
+  coe f := H.coe (ofLex f)
+
 /-- A recursor for `Lex`. Use as `induction x`. -/
 @[elab_as_elim, induction_eliminator, cases_eliminator]
 protected def Lex.rec {β : Lex α → Sort*} (h : ∀ a, β (toLex a)) : ∀ a, β a := fun a => h (ofLex a)
@@ -233,6 +236,9 @@ instance (α : Type*) [DecidableEq α] : DecidableEq (Colex α) :=
 instance (α : Type*) [Inhabited α] : Inhabited (Colex α) :=
   inferInstanceAs (Inhabited α)
 
+instance {α γ} [H : CoeFun α γ] : CoeFun (Colex α) γ where
+  coe f := H.coe (ofColex f)
+
 /-- A recursor for `Colex`. Use as `induction x`. -/
 @[elab_as_elim, induction_eliminator, cases_eliminator]
 protected def Colex.rec {β : Colex α → Sort*} (h : ∀ a, β (toColex a)) : ∀ a, β a :=