refactor(data/finset/nat_antidiagonal): state lemmas with cons instea…

…d of insert (#14533)

This puts less of a burden on the caller rewriting in the forward direction, as they don't have to prove obvious things about membership when evaluating sums.

Since this adds the missing `finset.map_cons`, a number of uses of `multiset.map_cons` now need qualified names.

src/algebra/big_operators/nat_antidiagonal.lean

@@ -23,10 +23,7 @@ namespace nat
 lemma prod_antidiagonal_succ {n : ℕ} {f : ℕ × ℕ → M} :
   ∏ p in antidiagonal (n + 1), f p = f (0, n + 1) * ∏ p in antidiagonal n, f (p.1 + 1, p.2) :=
 begin
-  rw [antidiagonal_succ, prod_insert, prod_map], refl,
-  intro con, rcases mem_map.1 con with ⟨⟨a,b⟩, ⟨h1, h2⟩⟩,
-  simp only [prod.mk.inj_iff, function.embedding.coe_prod_map, prod.map_mk] at h2,
-  apply nat.succ_ne_zero a h2.1,
+  rw [antidiagonal_succ, prod_cons, prod_map], refl,
 end
 
 lemma sum_antidiagonal_succ {n : ℕ} {f : ℕ × ℕ → N} :

src/algebra/polynomial/big_operators.lean

@@ -142,7 +142,7 @@ lemma leading_coeff_multiset_prod' (h : (t.map leading_coeff).prod ≠ 0) :
   t.prod.leading_coeff = (t.map leading_coeff).prod :=
 begin
   induction t using multiset.induction_on with a t ih, { simp },
-  simp only [map_cons, multiset.prod_cons] at h ⊢,
+  simp only [multiset.map_cons, multiset.prod_cons] at h ⊢,
   rw polynomial.leading_coeff_mul'; { rwa ih, apply right_ne_zero_of_mul h }
 end
 
@@ -169,7 +169,7 @@ lemma nat_degree_multiset_prod' (h : (t.map (λ f, leading_coeff f)).prod ≠ 0)
 begin
   revert h,
   refine multiset.induction_on t _ (λ a t ih ht, _), { simp },
-  rw [map_cons, multiset.prod_cons] at ht ⊢,
+  rw [multiset.map_cons, multiset.prod_cons] at ht ⊢,
   rw [multiset.sum_cons, polynomial.nat_degree_mul', ih],
   { apply right_ne_zero_of_mul ht },
   { rwa polynomial.leading_coeff_multiset_prod', apply right_ne_zero_of_mul ht },
@@ -227,7 +227,7 @@ lemma coeff_zero_multiset_prod :
   t.prod.coeff 0 = (t.map (λ f, coeff f 0)).prod :=
 begin
   refine multiset.induction_on t _ (λ a t ht, _), { simp },
-  rw [multiset.prod_cons, map_cons, multiset.prod_cons, polynomial.mul_coeff_zero, ht]
+  rw [multiset.prod_cons, multiset.map_cons, multiset.prod_cons, polynomial.mul_coeff_zero, ht]
 end
 
 lemma coeff_zero_prod :

src/data/finset/basic.lean

@@ -1907,6 +1907,10 @@ coe_injective $ by simp only [coe_map, coe_singleton, set.image_singleton]
   (insert a s).map f = insert (f a) (s.map f) :=
 by simp only [insert_eq, map_union, map_singleton]
 
+@[simp] lemma map_cons (f : α ↪ β) (a : α) (s : finset α) (ha : a ∉ s) :
+  (cons a s ha).map f = cons (f a) (s.map f) (by simpa using ha) :=
+eq_of_veq $ multiset.map_cons f a s.val
+
 @[simp] theorem map_eq_empty : s.map f = ∅ ↔ s = ∅ :=
 ⟨λ h, eq_empty_of_forall_not_mem $
  λ a m, ne_empty_of_mem (mem_map_of_mem _ m) h, λ e, e.symm ▸ rfl⟩

src/data/finset/fold.lean

@@ -30,11 +30,11 @@ variables {op} {f : α → β} {b : β} {s : finset α} {a : α}
 @[simp] theorem fold_empty : (∅ : finset α).fold op b f = b := rfl
 
 @[simp] theorem fold_cons (h : a ∉ s) : (cons a s h).fold op b f = f a * s.fold op b f :=
-by { dunfold fold, rw [cons_val, map_cons, fold_cons_left], }
+by { dunfold fold, rw [cons_val, multiset.map_cons, fold_cons_left], }
 
 @[simp] theorem fold_insert [decidable_eq α] (h : a ∉ s) :
   (insert a s).fold op b f = f a * s.fold op b f :=
-by unfold fold; rw [insert_val, ndinsert_of_not_mem h, map_cons, fold_cons_left]
+by unfold fold; rw [insert_val, ndinsert_of_not_mem h, multiset.map_cons, fold_cons_left]
 
 @[simp] theorem fold_singleton : ({a} : finset α).fold op b f = f a * b := rfl
 

src/data/finset/nat_antidiagonal.lean

@@ -39,32 +39,33 @@ by simp [antidiagonal]
 @[simp] lemma antidiagonal_zero : antidiagonal 0 = {(0, 0)} :=
 rfl
 
-lemma antidiagonal_succ {n : ℕ} :
-  antidiagonal (n + 1) = insert (0, n + 1) ((antidiagonal n).map
-  (function.embedding.prod_map ⟨nat.succ, nat.succ_injective⟩ (function.embedding.refl _))) :=
+lemma antidiagonal_succ (n : ℕ) :
+  antidiagonal (n + 1) = cons (0, n + 1) ((antidiagonal n).map
+  (function.embedding.prod_map ⟨nat.succ, nat.succ_injective⟩ (function.embedding.refl _)))
+  (by simp) :=
 begin
   apply eq_of_veq,
-  rw [insert_val_of_not_mem, map_val],
+  rw [cons_val, map_val],
   { apply multiset.nat.antidiagonal_succ },
-  { intro con, rcases mem_map.1 con with ⟨⟨a,b⟩, ⟨h1, h2⟩⟩,
-    simp only [prod.mk.inj_iff, function.embedding.coe_prod_map, prod.map_mk] at h2,
-    apply nat.succ_ne_zero a h2.1, }
 end
 
-lemma antidiagonal_succ' {n : ℕ} :
-  antidiagonal (n + 1) = insert (n + 1, 0) ((antidiagonal n).map
-  (function.embedding.prod_map (function.embedding.refl _) ⟨nat.succ, nat.succ_injective⟩)) :=
+lemma antidiagonal_succ' (n : ℕ) :
+  antidiagonal (n + 1) = cons (n + 1, 0) ((antidiagonal n).map
+  (function.embedding.prod_map (function.embedding.refl _) ⟨nat.succ, nat.succ_injective⟩))
+  (by simp) :=
 begin
   apply eq_of_veq,
-  rw [insert_val_of_not_mem, map_val],
-  { apply multiset.nat.antidiagonal_succ' },
-  { simp },
+  rw [cons_val, map_val],
+  exact multiset.nat.antidiagonal_succ',
 end
 
 lemma antidiagonal_succ_succ' {n : ℕ} :
-  antidiagonal (n + 2) = insert (0, n + 2) (insert (n + 2, 0) ((antidiagonal n).map
-  (function.embedding.prod_map ⟨nat.succ, nat.succ_injective⟩ ⟨nat.succ, nat.succ_injective⟩))) :=
-by { rw [antidiagonal_succ, antidiagonal_succ', map_insert, map_map], refl }
+  antidiagonal (n + 2) =
+    cons (0, n + 2)
+      (cons (n + 2, 0) ((antidiagonal n).map
+        (function.embedding.prod_map ⟨nat.succ, nat.succ_injective⟩ ⟨nat.succ, nat.succ_injective⟩))
+        $ by simp) (by simp) :=
+by { simp_rw [antidiagonal_succ (n + 1), antidiagonal_succ', finset.map_cons, map_map], refl }
 
 lemma map_swap_antidiagonal {n : ℕ} :
   (antidiagonal n).map ⟨prod.swap, prod.swap_right_inverse.injective⟩ = antidiagonal n :=