feat(data/fin/tuple/nat_antidiagonal): add an equiv and some TODO com…

…ments. (#13338)

This follows on from #13031, and:

* Adds the tuple version of an antidiagonal equiv
* Makes some arguments implicit
* Adds some comments to tie together `finset.nat.antidiagonal_tuple` with the `cut` definition used in one of the 100 Freek problems.

archive/100-theorems-list/45_partition.lean

@@ -7,6 +7,7 @@ import ring_theory.power_series.basic
 import combinatorics.partition
 import data.nat.parity
 import data.finset.nat_antidiagonal
+import data.fin.tuple.nat_antidiagonal
 import tactic.interval_cases
 import tactic.apply_fun
 
@@ -84,8 +85,8 @@ def partial_distinct_gf (m : ℕ) [comm_semiring α] :=
 /--
 Functions defined only on `s`, which sum to `n`. In other words, a partition of `n` indexed by `s`.
 Every function in here is finitely supported, and the support is a subset of `s`.
-This should be thought of as a generalisation of `finset.nat.antidiagonal`, where
-`antidiagonal n` is the same thing as `cut s n` if `s` has two elements.
+This should be thought of as a generalisation of `finset.nat.antidiagonal_tuple` where
+`antidiagonal_tuple k n` is the same thing as `cut (s : finset.univ (fin k)) n`.
 -/
 def cut {ι : Type*} (s : finset ι) (n : ℕ) : finset (ι → ℕ) :=
 finset.filter (λ f, s.sum f = n) ((s.pi (λ _, range (n+1))).map
@@ -120,6 +121,10 @@ begin
   simp [mem_cut, add_comm],
 end
 
+lemma cut_univ_fin_eq_antidiagonal_tuple (n : ℕ) (k : ℕ) :
+  cut univ n = nat.antidiagonal_tuple k n :=
+by { ext, simp [nat.mem_antidiagonal_tuple, mem_cut] }
+
 /-- There is only one `cut` of 0. -/
 @[simp]
 lemma cut_zero {ι : Type*} (s : finset ι) :

src/data/fin/tuple/nat_antidiagonal.lean

@@ -36,6 +36,10 @@ the sequence of elements `x : fin k → ℕ` such that `n = ∑ i, x i`.
 
 While we could implement this by filtering `(fintype.pi_finset $ λ _, range (n + 1))` or similar,
 this implementation would be much slower.
+
+In the future, we could consider generalizing `finset.nat.antidiagonal_tuple` further to
+support finitely-supported functions, as is done with `cut` in
+`archive/100-theorems-list/45_partition.lean`.
 -/
 
 open_locale big_operators
@@ -63,7 +67,7 @@ def antidiagonal_tuple : Π k, ℕ → list (fin k → ℕ)
 @[simp] lemma antidiagonal_tuple_zero_zero : antidiagonal_tuple 0 0 = [![]] := rfl
 @[simp] lemma antidiagonal_tuple_zero_succ (n : ℕ) : antidiagonal_tuple 0 n.succ = [] := rfl
 
-lemma mem_antidiagonal_tuple {n : ℕ} {k : ℕ} (x : fin k → ℕ) :
+lemma mem_antidiagonal_tuple {n : ℕ} {k : ℕ} {x : fin k → ℕ} :
   x ∈ antidiagonal_tuple k n ↔ ∑ i, x i = n :=
 begin
   induction k with k ih generalizing n,
@@ -143,9 +147,9 @@ list.nat.antidiagonal_tuple k n
 @[simp] lemma antidiagonal_tuple_zero_zero : antidiagonal_tuple 0 0 = { ![]} := rfl
 @[simp] lemma antidiagonal_tuple_zero_succ (n : ℕ) : antidiagonal_tuple 0 n.succ = 0 := rfl
 
-lemma mem_antidiagonal_tuple {n : ℕ} {k : ℕ} (x : fin k → ℕ) :
+lemma mem_antidiagonal_tuple {n : ℕ} {k : ℕ} {x : fin k → ℕ} :
   x ∈ antidiagonal_tuple k n ↔ ∑ i, x i = n :=
-list.nat.mem_antidiagonal_tuple _
+list.nat.mem_antidiagonal_tuple
 
 lemma nodup_antidiagonal_tuple (k n : ℕ) : (antidiagonal_tuple k n).nodup :=
 list.nat.nodup_antidiagonal_tuple _ _
@@ -169,9 +173,9 @@ def antidiagonal_tuple (k n : ℕ) : finset (fin k → ℕ) :=
 @[simp] lemma antidiagonal_tuple_zero_zero : antidiagonal_tuple 0 0 = { ![]} := rfl
 @[simp] lemma antidiagonal_tuple_zero_succ (n : ℕ) : antidiagonal_tuple 0 n.succ = ∅ := rfl
 
-lemma mem_antidiagonal_tuple {n : ℕ} {k : ℕ} (x : fin k → ℕ) :
+lemma mem_antidiagonal_tuple {n : ℕ} {k : ℕ} {x : fin k → ℕ} :
   x ∈ antidiagonal_tuple k n ↔ ∑ i, x i = n :=
-list.nat.mem_antidiagonal_tuple _
+list.nat.mem_antidiagonal_tuple
 
 @[simp] lemma antidiagonal_tuple_one (n : ℕ) : antidiagonal_tuple 1 n = { ![n]} :=
 finset.eq_of_veq (multiset.nat.antidiagonal_tuple_one n)
@@ -180,4 +184,19 @@ lemma antidiagonal_tuple_two (n : ℕ) :
   antidiagonal_tuple 2 n = (antidiagonal n).map (pi_fin_two_equiv (λ _, ℕ)).symm.to_embedding :=
 finset.eq_of_veq (multiset.nat.antidiagonal_tuple_two n)
 
+section equiv_prod
+
+/-- The disjoint union of antidiagonal tuples `Σ n, antidiagonal_tuple k n` is equivalent to the
+`k`-tuple `fin k → ℕ`. This is such an equivalence, obtained by mapping `(n, x)` to `x`.
+
+This is the tuple version of `finset.nat.sigma_antidiagonal_equiv_prod`. -/
+@[simps] def sigma_antidiagonal_tuple_equiv_tuple (k : ℕ) :
+  (Σ n, antidiagonal_tuple k n) ≃ (fin k → ℕ) :=
+{ to_fun := λ x, x.2,
+  inv_fun := λ x, ⟨∑ i, x i, x, mem_antidiagonal_tuple.mpr rfl⟩,
+  left_inv := λ ⟨n, t, h⟩, sigma.subtype_ext (mem_antidiagonal_tuple.mp h) rfl,
+  right_inv := λ x, rfl }
+
+end equiv_prod
+
 end finset.nat