chore(data/fintype/basic): Better fin lemmas (#14200)

Turn `finset.image` into `finset.map` and `insert` into `finset.cons` in the three lemmas relating `univ : finset (fin (n + 1))` and `univ : finset (fin n)`. Golf proofs involving the related big operators lemmas.

src/algebra/big_operators/basic.lean

@@ -41,6 +41,8 @@ See the documentation of `to_additive.attr` for more information.
 universes u v w
 variables {β : Type u} {α : Type v} {γ : Type w}
 
+open fin
+
 namespace finset
 
 /--
@@ -190,8 +192,8 @@ namespace finset
 section comm_monoid
 variables [comm_monoid β]
 
-@[simp, to_additive]
-lemma prod_empty {f : α → β} : (∏ x in (∅:finset α), f x) = 1 := rfl
+@[simp, to_additive] lemma prod_empty : ∏ x in ∅, f x = 1 := rfl
+@[to_additive] lemma prod_of_empty [is_empty α] : ∏ i, f i = 1 := by rw [univ_eq_empty, prod_empty]
 
 @[simp, to_additive]
 lemma prod_cons (h : a ∉ s) : (∏ x in (cons a s h), f x) = f a * ∏ x in s, f x :=

src/algebra/big_operators/fin.lean

@@ -61,13 +61,9 @@ is the product of `f x`, for some `x : fin (n + 1)` times the remaining product
 @[to_additive
 /- A sum of a function `f : fin (n + 1) → β` over all `fin (n + 1)`
 is the sum of `f x`, for some `x : fin (n + 1)` plus the remaining product -/]
-theorem prod_univ_succ_above [comm_monoid β] {n : ℕ} (f : fin (n + 1) → β)
-  (x : fin (n + 1)) :
+theorem prod_univ_succ_above [comm_monoid β] {n : ℕ} (f : fin (n + 1) → β) (x : fin (n + 1)) :
   ∏ i, f i = f x * ∏ i : fin n, f (x.succ_above i) :=
-begin
-  rw [fintype.prod_eq_mul_prod_compl x, ← image_succ_above_univ, prod_image],
-  exact λ _ _ _ _ h, x.succ_above.injective h
-end
+by rw [univ_succ_above, prod_cons, finset.prod_map, rel_embedding.coe_fn_to_embedding]
 
 /-- A product of a function `f : fin (n + 1) → β` over all `fin (n + 1)`
 is the product of `f 0` plus the remaining product -/
@@ -87,6 +83,10 @@ theorem prod_univ_cast_succ [comm_monoid β] {n : ℕ} (f : fin (n + 1) → β)
   ∏ i, f i = (∏ i : fin n, f i.cast_succ) * f (last n) :=
 by simpa [mul_comm] using prod_univ_succ_above f (last n)
 
+@[to_additive] lemma prod_cons [comm_monoid β] {n : ℕ} (x : β) (f : fin n → β) :
+  ∏ i : fin n.succ, (cons x f : fin n.succ → β) i = x * ∏ i : fin n, f i :=
+by simp_rw [prod_univ_succ, cons_zero, cons_succ]
+
 @[to_additive sum_univ_one] theorem prod_univ_one [comm_monoid β] (f : fin 1 → β) :
   ∏ i, f i = f 0 :=
 by simp

src/data/fin/tuple/nat_antidiagonal.lean

@@ -3,12 +3,9 @@ Copyright (c) 2022 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
-
-import data.fin.vec_notation
-import algebra.big_operators.basic
-import data.list.nat_antidiagonal
-import data.multiset.nat_antidiagonal
+import algebra.big_operators.fin
 import data.finset.nat_antidiagonal
+import data.fin.vec_notation
 import logic.equiv.fin
 
 /-!
@@ -76,11 +73,8 @@ begin
     { simp },
     { simp [eq_comm] }, },
   { refine fin.cons_induction (λ x₀ x, _) x,
-    have : (0 : fin k.succ) ∉ finset.image fin.succ (finset.univ : finset (fin k)) := by simp,
-    simp_rw [antidiagonal_tuple, list.mem_bind, list.mem_map, list.nat.mem_antidiagonal,
-      fin.univ_succ, finset.sum_insert this, fin.cons_zero,
-      finset.sum_image (λ x hx y hy h, fin.succ_injective _ h), fin.cons_succ, fin.cons_eq_cons,
-      exists_eq_right_right, ih, prod.exists],
+    simp_rw [fin.sum_cons, antidiagonal_tuple, list.mem_bind, list.mem_map,
+      list.nat.mem_antidiagonal, fin.cons_eq_cons, exists_eq_right_right, ih, prod.exists],
     split,
     { rintros ⟨a, b, rfl, rfl, rfl⟩, refl },
     { rintro rfl, exact ⟨_, _, rfl, rfl, rfl⟩, } },

src/data/fintype/basic.lean

@@ -758,21 +758,26 @@ by rw [← fin.succ_above_zero, fin.image_succ_above_univ]
   (univ : finset (fin n)).image fin.cast_succ = {fin.last n}ᶜ :=
 by rw [← fin.succ_above_last, fin.image_succ_above_univ]
 
+/- The following three lemmas use `finset.cons` instead of `insert` and `finset.map` instead of
+`finset.image` to reduce proof obligations downstream. -/
+
 /-- Embed `fin n` into `fin (n + 1)` by prepending zero to the `univ` -/
 lemma fin.univ_succ (n : ℕ) :
-  (univ : finset (fin (n + 1))) = insert 0 (univ.image fin.succ) :=
-by simp
+  (univ : finset (fin (n + 1))) =
+    cons 0 (univ.map ⟨fin.succ, fin.succ_injective _⟩) (by simp [map_eq_image]) :=
+by simp [map_eq_image]
 
 /-- Embed `fin n` into `fin (n + 1)` by appending a new `fin.last n` to the `univ` -/
 lemma fin.univ_cast_succ (n : ℕ) :
-  (univ : finset (fin (n + 1))) = insert (fin.last n) (univ.image fin.cast_succ) :=
-by simp
+  (univ : finset (fin (n + 1))) =
+    cons (fin.last n) (univ.map fin.cast_succ.to_embedding) (by simp [map_eq_image]) :=
+by simp [map_eq_image]
 
 /-- Embed `fin n` into `fin (n + 1)` by inserting
 around a specified pivot `p : fin (n + 1)` into the `univ` -/
 lemma fin.univ_succ_above (n : ℕ) (p : fin (n + 1)) :
-  (univ : finset (fin (n + 1))) = insert p (univ.image (fin.succ_above p)) :=
-by simp
+  (univ : finset (fin (n + 1))) = cons p (univ.map $ (fin.succ_above p).to_embedding) (by simp) :=
+by simp [map_eq_image]
 
 @[instance, priority 10] def unique.fintype {α : Type*} [unique α] : fintype α :=
 fintype.of_subsingleton default

src/linear_algebra/linear_independent.lean

@@ -3,9 +3,9 @@ Copyright (c) 2020 Anne Baanen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Alexander Bentkamp, Anne Baanen
 -/
+import algebra.big_operators.fin
 import linear_algebra.finsupp
 import linear_algebra.prod
-import logic.equiv.fin
 import set_theory.cardinal.basic
 
 /-!
@@ -253,19 +253,12 @@ lemma linear_independent.fin_cons' {m : ℕ} (x : M) (v : fin m → M)
 begin
   rw fintype.linear_independent_iff at hli ⊢,
   rintros g total_eq j,
-  have zero_not_mem : (0 : fin m.succ) ∉ finset.univ.image (fin.succ : fin m → fin m.succ),
-  { rw finset.mem_image,
-    rintro ⟨x, hx, succ_eq⟩,
-    exact fin.succ_ne_zero _ succ_eq },
-  simp only [submodule.coe_mk, fin.univ_succ, finset.sum_insert zero_not_mem,
-  fin.cons_zero, fin.cons_succ,
-  forall_true_iff, imp_self, fin.succ_inj, finset.sum_image] at total_eq,
+  simp_rw [fin.sum_univ_succ, fin.cons_zero, fin.cons_succ] at total_eq,
   have : g 0 = 0,
   { refine x_ortho (g 0) ⟨∑ (i : fin m), g i.succ • v i, _⟩ total_eq,
     exact sum_mem (λ i _, smul_mem _ _ (subset_span ⟨i, rfl⟩)) },
-  refine fin.cases this (λ j, _) j,
-  apply hli (λ i, g i.succ),
-  simpa only [this, zero_smul, zero_add] using total_eq
+  rw [this, zero_smul, zero_add] at total_eq,
+  exact fin.cases this (hli _ total_eq) j,
 end
 
 /-- A set of linearly independent vectors in a module `M` over a semiring `K` is also linearly