From 52aaf17383caf3129abab9c090e0b7c6ffabc1ea Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Tue, 15 Feb 2022 17:47:30 +0000
Subject: [PATCH] feat(data/{list,multiset,finset}/nat_antidiagonal): add
 lemmas to remove elements from head and tail of antidiagonal (#12028)

Also lowered `finset.nat.map_swap_antidiagonal` down to `list` through `multiset`.
---
 src/data/finset/nat_antidiagonal.lean   | 29 +++++++++++++++----------
 src/data/list/nat_antidiagonal.lean     | 24 ++++++++++++++++++++
 src/data/multiset/nat_antidiagonal.lean | 14 ++++++++++++
 3 files changed, 55 insertions(+), 12 deletions(-)

diff --git a/src/data/finset/nat_antidiagonal.lean b/src/data/finset/nat_antidiagonal.lean
index b74d438a74aba..66f68b4a912f4 100644
--- a/src/data/finset/nat_antidiagonal.lean
+++ b/src/data/finset/nat_antidiagonal.lean
@@ -45,26 +45,31 @@ lemma antidiagonal_succ {n : ℕ} :
 begin
   apply eq_of_veq,
   rw [insert_val_of_not_mem, map_val],
-  {apply multiset.nat.antidiagonal_succ},
+  { 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 map_swap_antidiagonal {n : ℕ} :
-  (antidiagonal n).map ⟨prod.swap, prod.swap_right_inverse.injective⟩ = antidiagonal n :=
+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⟩)) :=
 begin
-  ext,
-  simp only [exists_prop, mem_map, mem_antidiagonal, prod.exists],
-  rw add_comm,
-  split,
-  { rintro ⟨b, c, ⟨rfl, rfl⟩⟩,
-    simp },
-  { rintro rfl,
-    use [a.snd, a.fst],
-    simp }
+  apply eq_of_veq,
+  rw [insert_val_of_not_mem, map_val],
+  { apply multiset.nat.antidiagonal_succ' },
+  { simp },
 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 }
+
+lemma map_swap_antidiagonal {n : ℕ} :
+  (antidiagonal n).map ⟨prod.swap, prod.swap_right_inverse.injective⟩ = antidiagonal n :=
+eq_of_veq $ by simp [antidiagonal, multiset.nat.map_swap_antidiagonal]
+
 /-- A point in the antidiagonal is determined by its first co-ordinate. -/
 lemma antidiagonal_congr {n : ℕ} {p q : ℕ × ℕ} (hp : p ∈ antidiagonal n)
   (hq : q ∈ antidiagonal n) : p = q ↔ p.fst = q.fst :=
diff --git a/src/data/list/nat_antidiagonal.lean b/src/data/list/nat_antidiagonal.lean
index baa368e6e35a5..3fdd272fcb750 100644
--- a/src/data/list/nat_antidiagonal.lean
+++ b/src/data/list/nat_antidiagonal.lean
@@ -59,5 +59,29 @@ begin
   ext; simp,
 end
 
+lemma antidiagonal_succ' {n : ℕ} :
+  antidiagonal (n + 1) = ((antidiagonal n).map (prod.map id nat.succ)) ++ [(n + 1, 0)] :=
+begin
+  simp only [antidiagonal, range_succ, add_tsub_cancel_left, map_append,
+    append_assoc, tsub_self, singleton_append, map_map, map],
+  congr' 1,
+  apply map_congr,
+  simp [le_of_lt, nat.succ_eq_add_one, nat.sub_add_comm] { contextual := tt },
+end
+
+lemma antidiagonal_succ_succ' {n : ℕ} :
+  antidiagonal (n + 2) =
+  (0, n + 2) :: ((antidiagonal n).map (prod.map nat.succ nat.succ)) ++ [(n + 2, 0)] :=
+by { rw antidiagonal_succ', simpa }
+
+lemma map_swap_antidiagonal {n : ℕ} :
+  (antidiagonal n).map prod.swap = (antidiagonal n).reverse :=
+begin
+  rw [antidiagonal, map_map, prod.swap, ← list.map_reverse,
+    range_eq_range', reverse_range', ← range_eq_range', map_map],
+  apply map_congr,
+  simp [nat.sub_sub_self, lt_succ_iff] { contextual := tt },
+end
+
 end nat
 end list
diff --git a/src/data/multiset/nat_antidiagonal.lean b/src/data/multiset/nat_antidiagonal.lean
index 7baddb3243291..40ca75f930169 100644
--- a/src/data/multiset/nat_antidiagonal.lean
+++ b/src/data/multiset/nat_antidiagonal.lean
@@ -48,5 +48,19 @@ coe_nodup.2 $ list.nat.nodup_antidiagonal 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]
 
+lemma antidiagonal_succ' {n : ℕ} :
+  antidiagonal (n + 1) = (n + 1, 0) ::ₘ ((antidiagonal n).map (prod.map id nat.succ)) :=
+by rw [antidiagonal, list.nat.antidiagonal_succ', ← coe_add, add_comm, antidiagonal, coe_map,
+  coe_add, list.singleton_append, cons_coe]
+
+lemma antidiagonal_succ_succ' {n : ℕ} :
+  antidiagonal (n + 2) =
+  (0, n + 2) ::ₘ (n + 2, 0) ::ₘ ((antidiagonal n).map (prod.map nat.succ nat.succ)) :=
+by { rw [antidiagonal_succ, antidiagonal_succ', map_cons, map_map, prod_map], refl }
+
+lemma map_swap_antidiagonal {n : ℕ} :
+  (antidiagonal n).map prod.swap = antidiagonal n :=
+by rw [antidiagonal, coe_map, list.nat.map_swap_antidiagonal, coe_reverse]
+
 end nat
 end multiset