feat: lemmas relating Finset.univ and List.get (#11704)

We add sufficient lemmas for the simplifier to prove
`∀ (l : List α), Finset.univ.val.map l.get = ↑l`,
as well as the easier to apply phrasing
`∀ (l : List α), Finset.univ.val.map (f <| l.get ·) = ↑(l.map f)`.

We then add lemmas stating the corollaries for functions out of `Finset` which are built out of `Multiset.map`, such as `Finset.image` and `Finset.prod`.

Author: timotree3

Mathlib/Algebra/BigOperators/Fin.lean

@@ -44,18 +44,19 @@ end Finset
 
 namespace Fin
 
-@[to_additive]
-theorem prod_univ_def [CommMonoid β] {n : ℕ} (f : Fin n → β) :
-    ∏ i, f i = ((List.finRange n).map f).prod := by simp [univ_def]
-#align fin.prod_univ_def Fin.prod_univ_def
-#align fin.sum_univ_def Fin.sum_univ_def
-
 @[to_additive]
 theorem prod_ofFn [CommMonoid β] {n : ℕ} (f : Fin n → β) : (List.ofFn f).prod = ∏ i, f i := by
-  rw [List.ofFn_eq_map, prod_univ_def]
+  simp [prod_eq_multiset_prod]
 #align fin.prod_of_fn Fin.prod_ofFn
 #align fin.sum_of_fn Fin.sum_ofFn
 
+@[to_additive]
+theorem prod_univ_def [CommMonoid β] {n : ℕ} (f : Fin n → β) :
+    ∏ i, f i = ((List.finRange n).map f).prod := by
+  rw [← List.ofFn_eq_map, prod_ofFn]
+#align fin.prod_univ_def Fin.prod_univ_def
+#align fin.sum_univ_def Fin.sum_univ_def
+
 /-- A product of a function `f : Fin 0 → β` is `1` because `Fin 0` is empty -/
 @[to_additive "A sum of a function `f : Fin 0 → β` is `0` because `Fin 0` is empty"]
 theorem prod_univ_zero [CommMonoid β] (f : Fin 0 → β) : ∏ i, f i = 1 :=
@@ -95,6 +96,15 @@ theorem prod_univ_castSucc [CommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) :
 #align fin.prod_univ_cast_succ Fin.prod_univ_castSucc
 #align fin.sum_univ_cast_succ Fin.sum_univ_castSucc
 
+@[to_additive (attr := simp)]
+theorem prod_univ_get [CommMonoid α] (l : List α) : ∏ i, l.get i = l.prod := by
+  simp [Finset.prod_eq_multiset_prod]
+
+@[to_additive (attr := simp)]
+theorem prod_univ_get' [CommMonoid β] (l : List α) (f : α → β) :
+    ∏ i, f (l.get i) = (l.map f).prod := by
+  simp [Finset.prod_eq_multiset_prod]
+
 @[to_additive]
 theorem prod_cons [CommMonoid β] {n : ℕ} (x : β) (f : Fin n → β) :
     (∏ i : Fin n.succ, (cons x f : Fin n.succ → β) i) = x * ∏ i : Fin n, f i := by
@@ -477,10 +487,8 @@ theorem prod_take_ofFn {n : ℕ} (f : Fin n → α) (i : ℕ) :
 #align list.sum_take_of_fn List.sum_take_ofFn
 
 @[to_additive]
-theorem prod_ofFn {n : ℕ} {f : Fin n → α} : (ofFn f).prod = ∏ i, f i := by
-  convert prod_take_ofFn f n
-  · rw [take_all_of_le (le_of_eq (length_ofFn f))]
-  · simp
+theorem prod_ofFn {n : ℕ} {f : Fin n → α} : (ofFn f).prod = ∏ i, f i :=
+  Fin.prod_ofFn f
 #align list.prod_of_fn List.prod_ofFn
 #align list.sum_of_fn List.sum_ofFn
 

Mathlib/Data/Fintype/Basic.lean

@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 import Mathlib.Algebra.Ring.Hom.Defs -- FIXME: This import is bogus
 import Mathlib.Data.Finset.Image
 import Mathlib.Data.Fin.OrderHom
+import Mathlib.Data.List.FinRange
 
 #align_import data.fintype.basic from "leanprover-community/mathlib"@"d78597269638367c3863d40d45108f52207e03cf"
 
@@ -836,6 +837,18 @@ theorem Fin.univ_def (n : ℕ) : (univ : Finset (Fin n)) = ⟨List.finRange n, L
 @[simp] theorem List.toFinset_finRange (n : ℕ) : (List.finRange n).toFinset = Finset.univ := by
   ext; simp
 
+@[simp] theorem Fin.univ_val_map {n : ℕ} (f : Fin n → α) :
+    Finset.univ.val.map f = List.ofFn f := by
+  simp [List.ofFn_eq_map, univ_def]
+
+theorem Fin.univ_image_def {n : ℕ} [DecidableEq α] (f : Fin n → α) :
+    Finset.univ.image f = (List.ofFn f).toFinset := by
+  simp [Finset.image]
+
+theorem Fin.univ_map_def {n : ℕ} (f : Fin n ↪ α) :
+    Finset.univ.map f = ⟨List.ofFn f, List.nodup_ofFn.mpr f.injective⟩ := by
+  simp [Finset.map]
+
 @[simp]
 theorem Fin.image_succAbove_univ {n : ℕ} (i : Fin (n + 1)) : univ.image i.succAbove = {i}ᶜ := by
   ext m
@@ -858,25 +871,33 @@ theorem Fin.image_castSucc (n : ℕ) :
 /-- Embed `Fin n` into `Fin (n + 1)` by prepending zero to the `univ` -/
 theorem Fin.univ_succ (n : ℕ) :
     (univ : Finset (Fin (n + 1))) =
-      cons 0 (univ.map ⟨Fin.succ, Fin.succ_injective _⟩) (by simp [map_eq_image]) :=
+      Finset.cons 0 (univ.map ⟨Fin.succ, Fin.succ_injective _⟩) (by simp [map_eq_image]) :=
   by simp [map_eq_image]
 #align fin.univ_succ Fin.univ_succ
 
 /-- Embed `Fin n` into `Fin (n + 1)` by appending a new `Fin.last n` to the `univ` -/
 theorem Fin.univ_castSuccEmb (n : ℕ) :
     (univ : Finset (Fin (n + 1))) =
-      cons (Fin.last n) (univ.map Fin.castSuccEmb.toEmbedding) (by simp [map_eq_image]) :=
+      Finset.cons (Fin.last n) (univ.map Fin.castSuccEmb.toEmbedding) (by simp [map_eq_image]) :=
   by simp [map_eq_image]
 #align fin.univ_cast_succ Fin.univ_castSuccEmb
 
 /-- Embed `Fin n` into `Fin (n + 1)` by inserting
 around a specified pivot `p : Fin (n + 1)` into the `univ` -/
 theorem Fin.univ_succAbove (n : ℕ) (p : Fin (n + 1)) :
     (univ : Finset (Fin (n + 1))) =
-      cons p (univ.map <| (Fin.succAboveEmb p).toEmbedding) (by simp) :=
+      Finset.cons p (univ.map <| (Fin.succAboveEmb p).toEmbedding) (by simp) :=
   by simp [map_eq_image]
 #align fin.univ_succ_above Fin.univ_succAbove
 
+@[simp] theorem Fin.univ_image_get [DecidableEq α] (l : List α) :
+    Finset.univ.image l.get = l.toFinset := by
+  simp [univ_image_def]
+
+@[simp] theorem Fin.univ_image_get' [DecidableEq β] (l : List α) (f : α → β) :
+    Finset.univ.image (f <| l.get ·) = (l.map f).toFinset := by
+  simp [univ_image_def]
+
 @[instance]
 def Unique.fintype {α : Type*} [Unique α] : Fintype α :=
   Fintype.ofSubsingleton default

Mathlib/Data/List/OfFn.lean

@@ -186,13 +186,18 @@ theorem ofFn_mul' {m n} (f : Fin (m * n) → α) :
   simp_rw [mul_comm m n, mul_comm m, ofFn_mul, Fin.cast_mk]
 #align list.of_fn_mul' List.ofFn_mul'
 
+@[simp]
 theorem ofFn_get : ∀ l : List α, (ofFn (get l)) = l
   | [] => rfl
   | a :: l => by
     rw [ofFn_succ]
     congr
     exact ofFn_get l
 
+@[simp]
+theorem ofFn_get_eq_map {β : Type*} (l : List α) (f : α → β) : ofFn (f <| l.get ·) = l.map f := by
+  rw [← Function.comp_def, ← map_ofFn, ofFn_get]
+
 set_option linter.deprecated false in
 @[deprecated ofFn_get] -- 2023-01-17
 theorem ofFn_nthLe : ∀ l : List α, (ofFn fun i => nthLe l i i.2) = l :=