feat(data/*/nat_antidiagonal): induction lemmas about antidiagonals (#4193)

Adds a `nat.antidiagonal_succ` lemma for `list`, `multiset`, and `finset`, useful for proving facts about power series derivatives



Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>

Author: awainverse

src/algebra/big_operators/default.lean

@@ -3,3 +3,4 @@
 import algebra.big_operators.order
 import algebra.big_operators.intervals
 import algebra.big_operators.ring
+import algebra.big_operators.nat_antidiagonal

src/algebra/big_operators/nat_antidiagonal.lean

@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2020 Aaron Anderson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Aaron Anderson
+-/
+
+import data.finset.nat_antidiagonal
+import algebra.big_operators.basic
+
+/-!
+# Big operators for `nat_antidiagonal`
+
+This file contains theorems relevant to big operators over `finset.nat.antidiagonal`.
+-/
+
+open_locale big_operators
+
+variables {α : Type*} [add_comm_monoid α]
+
+namespace finset
+namespace nat
+
+lemma sum_antidiagonal_succ {n : ℕ} {f : ℕ × ℕ → α} :
+  (antidiagonal (n + 1)).sum f = f (0, n + 1) + ((antidiagonal n).map
+  (function.embedding.prod_map ⟨nat.succ, nat.succ_injective⟩ (function.embedding.refl _))).sum f :=
+begin
+  rw [antidiagonal_succ, sum_insert],
+  intro con, rcases mem_map.1 con with ⟨⟨a,b⟩, ⟨h1, h2⟩⟩,
+  simp only [prod.mk.inj_iff, function.embedding.coe_fn_mk, function.embedding.refl_apply,
+               function.embedding.coe_prod_map, prod.map_mk] at h2,
+  apply nat.succ_ne_zero a h2.1,
+end
+
+end nat
+end finset

src/data/finset/nat_antidiagonal.lean

@@ -22,7 +22,7 @@ def antidiagonal (n : ℕ) : finset (ℕ × ℕ) :=
 /-- A pair (i,j) is contained in the antidiagonal of `n` if and only if `i+j=n`. -/
 @[simp] lemma mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} :
   x ∈ antidiagonal n ↔ x.1 + x.2 = n :=
-by rw [antidiagonal, finset.mem_def, multiset.nat.mem_antidiagonal]
+by rw [antidiagonal, mem_def, multiset.nat.mem_antidiagonal]
 
 /-- The cardinality of the antidiagonal of `n` is `n+1`. -/
 @[simp] lemma card_antidiagonal (n : ℕ) : (antidiagonal n).card = n+1 :=
@@ -32,6 +32,34 @@ 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 _))) :=
+begin
+  apply eq_of_veq,
+  rw [insert_val_of_not_mem, 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_fn_mk, function.embedding.refl_apply,
+               function.embedding.coe_prod_map, prod.map_mk] at h2,
+    apply nat.succ_ne_zero a h2.1, }
+end
+
+lemma map_swap_antidiagonal {n : ℕ} :
+  (antidiagonal n).map ⟨prod.swap, prod.swap_right_inverse.injective⟩ = antidiagonal n :=
+begin
+  ext,
+  simp only [exists_prop, mem_map, mem_antidiagonal,
+    function.embedding.coe_fn_mk, prod.swap_prod_mk, prod.exists],
+  rw add_comm,
+  split,
+  { rintro ⟨b, c, ⟨rfl, rfl⟩⟩,
+    simp },
+  { rintro rfl,
+    use [a.snd, a.fst],
+    simp }
+end
+
 end nat
 
 end finset

src/data/list/nat_antidiagonal.lean

@@ -37,5 +37,14 @@ rfl
 lemma nodup_antidiagonal (n : ℕ) : nodup (antidiagonal n) :=
 nodup_map (@left_inverse.injective ℕ (ℕ × ℕ) prod.fst (λ i, (i, n-i)) $ λ i, rfl) (nodup_range _)
 
+@[simp] lemma antidiagonal_succ {n : ℕ} :
+  antidiagonal (n + 1) = (0, n + 1) :: ((antidiagonal n).map (prod.map nat.succ id) ) :=
+begin
+  simp only [antidiagonal, range_succ_eq_map, map_cons, true_and, nat.add_succ_sub_one, add_zero, 
+    id.def, eq_self_iff_true, nat.sub_zero, map_map, prod.map_mk],
+  apply congr (congr rfl _) rfl,
+  ext; simp,
+end
+
 end nat
 end list

src/data/multiset/nat_antidiagonal.lean

@@ -35,5 +35,9 @@ rfl
 @[simp] lemma nodup_antidiagonal (n : ℕ) : nodup (antidiagonal n) :=
 coe_nodup.2 $ list.nat.nodup_antidiagonal n
 
+@[simp] lemma antidiagonal_succ {n : ℕ} :
+  antidiagonal (n + 1) = (0, n + 1) :: ((antidiagonal n).map (prod.map nat.succ id)) :=
+by simp only [antidiagonal, list.nat.antidiagonal_succ, coe_map, cons_coe]
+
 end nat
 end multiset