feat(Data/List/Range + Data/Finset/Sort): List.finRange lemmas (#7184)

Prove Fin.sort_univ and List.indexOf_finRange discussed in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20value.20of.20.60fintypeEquivFin.60



Co-authored-by: palalansoukî <73170405+iehality@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Data/Finset/Sort.lean

@@ -259,3 +259,14 @@ unsafe instance [Repr α] : Repr (Finset α) where
     if s.card = 0 then "∅" else repr s.1
 
 end Finset
+
+namespace Fin
+
+theorem sort_univ (n : ℕ) : Finset.univ.sort (fun x y : Fin n => x ≤ y) = List.finRange n :=
+  List.eq_of_perm_of_sorted
+    (List.perm_of_nodup_nodup_toFinset_eq
+      (Finset.univ.sort_nodup _) (List.nodup_finRange n) (by simp))
+    (Finset.univ.sort_sorted LE.le)
+    (List.pairwise_le_finRange n)
+
+end Fin

Mathlib/Data/Fintype/Basic.lean

@@ -809,6 +809,9 @@ theorem Fin.univ_def (n : ℕ) : (univ : Finset (Fin n)) = ⟨List.finRange n, L
   rfl
 #align fin.univ_def Fin.univ_def
 
+@[simp] theorem List.toFinset_finRange (n : ℕ) : (List.finRange n).toFinset = Finset.univ := by
+  ext; simp
+
 @[simp]
 theorem Fin.image_succAbove_univ {n : ℕ} (i : Fin (n + 1)) : univ.image i.succAbove = {i}ᶜ := by
   ext m

Mathlib/Data/List/Range.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Kenny Lau, Scott Morrison
 -/
 import Mathlib.Data.List.Chain
+import Mathlib.Data.List.Nodup
 import Mathlib.Data.List.Zip
 
 #align_import data.list.range from "leanprover-community/mathlib"@"7b78d1776212a91ecc94cf601f83bdcc46b04213"
@@ -156,6 +157,12 @@ theorem finRange_eq_nil {n : ℕ} : finRange n = [] ↔ n = 0 := by
   rw [← length_eq_zero, length_finRange]
 #align list.fin_range_eq_nil List.finRange_eq_nil
 
+theorem pairwise_lt_finRange (n : ℕ) : Pairwise (· < ·) (finRange n) :=
+  (List.pairwise_lt_range n).pmap (by simp) (by simp)
+
+theorem pairwise_le_finRange (n : ℕ) : Pairwise (· ≤ ·) (finRange n) :=
+  (List.pairwise_le_range n).pmap (by simp) (by simp)
+
 @[to_additive]
 theorem prod_range_succ {α : Type u} [Monoid α] (f : ℕ → α) (n : ℕ) :
     ((range n.succ).map f).prod = ((range n).map f).prod * f n := by
@@ -221,4 +228,10 @@ theorem nthLe_finRange {n : ℕ} {i : ℕ} (h) :
   get_finRange h
 #align list.nth_le_fin_range List.nthLe_finRange
 
+@[simp] theorem indexOf_finRange (i : Fin k) : (finRange k).indexOf i = i := by
+  have : (finRange k).indexOf i < (finRange k).length := indexOf_lt_length.mpr (by simp)
+  have h₁ : (finRange k).get ⟨(finRange k).indexOf i, this⟩ = i := indexOf_get this
+  have h₂ : (finRange k).get ⟨i, by simp⟩ = i := get_finRange _
+  simpa using (Nodup.get_inj_iff (nodup_finRange k)).mp (Eq.trans h₁ h₂.symm)
+
 end List