From 4557f2c44f0a147333dfd55aabfd13f08d2c45c9 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sat, 18 Feb 2023 18:11:02 +0000
Subject: [PATCH] feat: add lemmas about `List.Sorted` (#2311)

* Add `List.Sorted.le_of_lt` and `List.Sorted.lt_of_le` (new).
* Add `List.Sorted.rel_get_of_lt` and `List.Sorted.rel_get_of_le` (`get` versions of `nthLe` lemmas).
* Add `List.sorted_ofFn_iff`, `List.sorted_lt_ofFn_iff`, and `List.sorted_le_ofFn_iff` (new).
* Deprecate `List.monotone_iff_ofFn_sorted` in favor of `List.sorted_le_ofFn_iff`.
* Rename `List.Monotone.ofFn_sorted` to `Monotone.ofFn_sorted`. In Lean 3, dot notation `hf.of_fn_sorted` used `lift.monotone.of_fn_sorted` if the `list` namespace is open. This is no longer the case in Lean 4.
---
 Mathlib/Data/Fin/Tuple/Sort.lean |  7 ++---
 Mathlib/Data/Finset/Sort.lean    |  2 +-
 Mathlib/Data/List/Sort.lean      | 47 ++++++++++++++++++++++++--------
 3 files changed, 38 insertions(+), 18 deletions(-)

diff --git a/Mathlib/Data/Fin/Tuple/Sort.lean b/Mathlib/Data/Fin/Tuple/Sort.lean
index 9438bf42e9701..12d8443341267 100644
--- a/Mathlib/Data/Fin/Tuple/Sort.lean
+++ b/Mathlib/Data/Fin/Tuple/Sort.lean
@@ -62,8 +62,7 @@ theorem graph.card (f : Fin n → α) : (graph f).card = n := by
 
 /-- `graphEquiv₁ f` is the natural equivalence between `Fin n` and `graph f`,
 mapping `i` to `(f i, i)`. -/
-def graphEquiv₁ (f : Fin n → α) : Fin n ≃ graph f
-    where
+def graphEquiv₁ (f : Fin n → α) : Fin n ≃ graph f where
   toFun i := ⟨(f i, i), by simp [graph]⟩
   invFun p := p.1.2
   left_inv i := by simp
@@ -124,9 +123,7 @@ theorem unique_monotone [PartialOrder α] {f : Fin n → α} {σ τ : Equiv.Perm
     (hfσ : Monotone (f ∘ σ)) (hfτ : Monotone (f ∘ τ)) : f ∘ σ = f ∘ τ :=
   ofFn_injective <|
     eq_of_perm_of_sorted ((σ.ofFn_comp_perm f).trans (τ.ofFn_comp_perm f).symm)
-      -- Porting note: used to use dot notation
-      (List.Monotone.ofFn_sorted hfσ)
-      (List.Monotone.ofFn_sorted hfτ)
+      hfσ.ofFn_sorted hfτ.ofFn_sorted
 #align tuple.unique_monotone Tuple.unique_monotone
 
 variable [LinearOrder α] {f : Fin n → α} {σ : Equiv.Perm (Fin n)}
diff --git a/Mathlib/Data/Finset/Sort.lean b/Mathlib/Data/Finset/Sort.lean
index d0c136d11458f..ebf8d679091d7 100644
--- a/Mathlib/Data/Finset/Sort.lean
+++ b/Mathlib/Data/Finset/Sort.lean
@@ -89,7 +89,7 @@ section SortLinearOrder
 variable [LinearOrder α]
 
 theorem sort_sorted_lt (s : Finset α) : List.Sorted (· < ·) (sort (· ≤ ·) s) :=
-  (sort_sorted _ _).imp₂ (@lt_of_le_of_ne _ _) (sort_nodup _ _)
+  (sort_sorted _ _).lt_of_le (sort_nodup _ _)
 #align finset.sort_sorted_lt Finset.sort_sorted_lt
 
 theorem sorted_zero_eq_min'_aux (s : Finset α) (h : 0 < (s.sort (· ≤ ·)).length) (H : s.Nonempty) :
diff --git a/Mathlib/Data/List/Sort.lean b/Mathlib/Data/List/Sort.lean
index f6ea9449065e3..3cf795fb0ef48 100644
--- a/Mathlib/Data/List/Sort.lean
+++ b/Mathlib/Data/List/Sort.lean
@@ -45,6 +45,14 @@ instance decidableSorted [DecidableRel r] (l : List α) : Decidable (Sorted r l)
   List.instDecidablePairwise _
 #align list.decidable_sorted List.decidableSorted
 
+protected theorem Sorted.le_of_lt [Preorder α] {l : List α} (h : l.Sorted (· < ·)) :
+    l.Sorted (· ≤ ·) :=
+  h.imp le_of_lt
+
+protected theorem Sorted.lt_of_le [PartialOrder α] {l : List α} (h₁ : l.Sorted (· ≤ ·))
+    (h₂ : l.Nodup) : l.Sorted (· < ·) :=
+  h₁.imp₂ (fun _ _ => lt_of_le_of_ne)  h₂
+
 @[simp]
 theorem sorted_nil : Sorted r [] :=
   Pairwise.nil
@@ -102,17 +110,23 @@ theorem sorted_singleton (a : α) : Sorted r [a] :=
   pairwise_singleton _ _
 #align list.sorted_singleton List.sorted_singleton
 
+theorem Sorted.rel_get_of_lt {l : List α} (h : l.Sorted r) {a b : Fin l.length} (hab : a < b) :
+    r (l.get a) (l.get b) :=
+  List.pairwise_iff_get.1 h _ _ hab
+
 theorem Sorted.rel_nthLe_of_lt {l : List α} (h : l.Sorted r) {a b : ℕ} (ha : a < l.length)
     (hb : b < l.length) (hab : a < b) : r (l.nthLe a ha) (l.nthLe b hb) :=
   List.pairwise_iff_get.1 h ⟨a, ha⟩ ⟨b, hb⟩ hab
 #align list.sorted.rel_nth_le_of_lt List.Sorted.rel_nthLe_of_lt
 
+theorem Sorted.rel_get_of_le [IsRefl α r] {l : List α} (h : l.Sorted r) {a b : Fin l.length}
+    (hab : a ≤ b) : r (l.get a) (l.get b) := by
+  rcases hab.eq_or_lt with (rfl | hlt)
+  exacts [refl _, h.rel_get_of_lt hlt]
+
 theorem Sorted.rel_nthLe_of_le [IsRefl α r] {l : List α} (h : l.Sorted r) {a b : ℕ}
-    (ha : a < l.length) (hb : b < l.length) (hab : a ≤ b) : r (l.nthLe a ha) (l.nthLe b hb) := by
-  cases' eq_or_lt_of_le hab with H H
-  · subst H
-    exact refl _
-  · exact h.rel_nthLe_of_lt _ _ H
+    (ha : a < l.length) (hb : b < l.length) (hab : a ≤ b) : r (l.nthLe a ha) (l.nthLe b hb) :=
+  h.rel_get_of_le hab
 #align list.sorted.rel_nth_le_of_le List.Sorted.rel_nthLe_of_le
 
 theorem Sorted.rel_of_mem_take_of_mem_drop {l : List α} (h : List.Sorted r l) {k : ℕ} {x y : α}
@@ -130,17 +144,26 @@ section Monotone
 
 variable {n : ℕ} {α : Type uu} [Preorder α] {f : Fin n → α}
 
+theorem sorted_ofFn_iff {r : α → α → Prop} : (ofFn f).Sorted r ↔ ((· < ·) ⇒ r) f f := by
+  simp_rw [Sorted, pairwise_iff_get, length_ofFn, get_ofFn, Relator.LiftFun]
+  exact Iff.symm (Fin.cast _).surjective.forall₂
+
+/-- The list `List.ofFn f` is strictly sorted with respect to `(· ≤ ·)` if and only if `f` is
+strictly monotone. -/
+@[simp] theorem sorted_lt_ofFn_iff : (ofFn f).Sorted (· < ·) ↔ StrictMono f := sorted_ofFn_iff
+
+/-- The list `List.ofFn f` is sorted with respect to `(· ≤ ·)` if and only if `f` is monotone. -/
+@[simp] theorem sorted_le_ofFn_iff : (ofFn f).Sorted (· ≤ ·) ↔ Monotone f :=
+  sorted_ofFn_iff.trans monotone_iff_forall_lt.symm
+
 /-- A tuple is monotone if and only if the list obtained from it is sorted. -/
-theorem monotone_iff_ofFn_sorted : Monotone f ↔ (ofFn f).Sorted (· ≤ ·) := by
-  simp_rw [Sorted, pairwise_iff_get, length_ofFn, get_ofFn, monotone_iff_forall_lt]
-  refine ⟨fun h i j hij => h <| Fin.mk_lt_mk.mpr hij, fun h ⟨i, hi⟩ ⟨j, hj⟩ hij => ?_⟩
-  exact h ⟨i, (length_ofFn f).symm ▸ hi⟩ ⟨j, (length_ofFn f).symm ▸ hj⟩ hij
+@[deprecated sorted_le_ofFn_iff]
+theorem monotone_iff_ofFn_sorted : Monotone f ↔ (ofFn f).Sorted (· ≤ ·) := sorted_le_ofFn_iff.symm
 #align list.monotone_iff_of_fn_sorted List.monotone_iff_ofFn_sorted
 
 /-- The list obtained from a monotone tuple is sorted. -/
-theorem Monotone.ofFn_sorted (h : Monotone f) : (ofFn f).Sorted (· ≤ ·) :=
-  monotone_iff_ofFn_sorted.1 h
-#align list.monotone.of_fn_sorted List.Monotone.ofFn_sorted
+alias sorted_le_ofFn_iff ↔ _ _root_.Monotone.ofFn_sorted
+#align list.monotone.of_fn_sorted Monotone.ofFn_sorted
 
 end Monotone