[GOAL]
n : ℕ
x : ℕ × ℕ
⊢ x ∈ antidiagonal n ↔ x.fst + x.snd = n
[PROOFSTEP]
rw [antidiagonal, mem_def, Multiset.Nat.mem_antidiagonal]
[GOAL]
n : ℕ
⊢ card (antidiagonal n) = n + 1
[PROOFSTEP]
simp [antidiagonal]
[GOAL]
n : ℕ
⊢ ¬(0, n + 1) ∈
      map (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ)) (antidiagonal n)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ antidiagonal (n + 1) =
    cons (0, n + 1)
      (map (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ)) (antidiagonal n))
      (_ :
        ¬(0, n + 1) ∈
            map (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ))
              (antidiagonal n))
[PROOFSTEP]
apply eq_of_veq
[GOAL]
case a
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (cons (0, n + 1)
        (map (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ)) (antidiagonal n))
        (_ :
          ¬(0, n + 1) ∈
              map (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ))
                (antidiagonal n))).val
[PROOFSTEP]
rw [cons_val, map_val]
[GOAL]
case a
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (0, n + 1) ::ₘ
      Multiset.map (↑(Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ)))
        (antidiagonal n).val
[PROOFSTEP]
apply Multiset.Nat.antidiagonal_succ
[GOAL]
n : ℕ
⊢ ¬(n + 1, 0) ∈
      map (Embedding.prodMap (Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective }) (antidiagonal n)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ antidiagonal (n + 1) =
    cons (n + 1, 0)
      (map (Embedding.prodMap (Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective }) (antidiagonal n))
      (_ :
        ¬(n + 1, 0) ∈
            map (Embedding.prodMap (Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective })
              (antidiagonal n))
[PROOFSTEP]
apply eq_of_veq
[GOAL]
case a
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (cons (n + 1, 0)
        (map (Embedding.prodMap (Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective }) (antidiagonal n))
        (_ :
          ¬(n + 1, 0) ∈
              map (Embedding.prodMap (Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective })
                (antidiagonal n))).val
[PROOFSTEP]
rw [cons_val, map_val]
[GOAL]
case a
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (n + 1, 0) ::ₘ
      Multiset.map (↑(Embedding.prodMap (Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective }))
        (antidiagonal n).val
[PROOFSTEP]
exact Multiset.Nat.antidiagonal_succ'
[GOAL]
n : ℕ
⊢ ¬(n + 2, 0) ∈
      map
        (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }
          { toFun := Nat.succ, inj' := Nat.succ_injective })
        (antidiagonal n)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ ¬(0, n + 2) ∈
      cons (n + 2, 0)
        (map
          (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }
            { toFun := Nat.succ, inj' := Nat.succ_injective })
          (antidiagonal n))
        (_ :
          ¬(n + 2, 0) ∈
              map
                (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }
                  { toFun := Nat.succ, inj' := Nat.succ_injective })
                (antidiagonal n))
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ antidiagonal (n + 2) =
    cons (0, n + 2)
      (cons (n + 2, 0)
        (map
          (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }
            { toFun := Nat.succ, inj' := Nat.succ_injective })
          (antidiagonal n))
        (_ :
          ¬(n + 2, 0) ∈
              map
                (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }
                  { toFun := Nat.succ, inj' := Nat.succ_injective })
                (antidiagonal n)))
      (_ :
        ¬(0, n + 2) ∈
            cons (n + 2, 0)
              (map
                (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }
                  { toFun := Nat.succ, inj' := Nat.succ_injective })
                (antidiagonal n))
              (_ :
                ¬(n + 2, 0) ∈
                    map
                      (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }
                        { toFun := Nat.succ, inj' := Nat.succ_injective })
                      (antidiagonal n)))
[PROOFSTEP]
simp_rw [antidiagonal_succ (n + 1), antidiagonal_succ', Finset.map_cons, map_map]
[GOAL]
n : ℕ
⊢ cons (0, n + 1 + 1)
      (cons (↑(Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ)) (n + 1, 0))
        (map
          (Embedding.trans (Embedding.prodMap (Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective })
            (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ)))
          (antidiagonal n))
        (_ :
          ¬↑(Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ)) (n + 1, 0) ∈
              map
                (Embedding.trans
                  (Embedding.prodMap (Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective })
                  (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ)))
                (antidiagonal n)))
      (_ :
        ¬(0, n + 1 + 1) ∈
            cons (↑(Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ)) (n + 1, 0))
              (map
                (Embedding.trans
                  (Embedding.prodMap (Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective })
                  (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ)))
                (antidiagonal n))
              (_ :
                ¬↑(Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ)) (n + 1, 0) ∈
                    map
                      (Embedding.trans
                        (Embedding.prodMap (Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective })
                        (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ)))
                      (antidiagonal n))) =
    cons (0, n + 2)
      (cons (n + 2, 0)
        (map
          (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }
            { toFun := Nat.succ, inj' := Nat.succ_injective })
          (antidiagonal n))
        (_ :
          ¬(n + 2, 0) ∈
              map
                (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }
                  { toFun := Nat.succ, inj' := Nat.succ_injective })
                (antidiagonal n)))
      (_ :
        ¬(0, n + 2) ∈
            cons (n + 2, 0)
              (map
                (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }
                  { toFun := Nat.succ, inj' := Nat.succ_injective })
                (antidiagonal n))
              (_ :
                ¬(n + 2, 0) ∈
                    map
                      (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }
                        { toFun := Nat.succ, inj' := Nat.succ_injective })
                      (antidiagonal n)))
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ (map { toFun := Prod.swap, inj' := (_ : Injective Prod.swap) } (antidiagonal n)).val = (antidiagonal n).val
[PROOFSTEP]
simp [antidiagonal, Multiset.Nat.map_swap_antidiagonal]
[GOAL]
n : ℕ
p q : ℕ × ℕ
hp : p ∈ antidiagonal n
hq : q ∈ antidiagonal n
⊢ p = q ↔ p.fst = q.fst
[PROOFSTEP]
refine' ⟨congr_arg Prod.fst, fun h ↦ Prod.ext h ((add_right_inj q.fst).mp _)⟩
[GOAL]
n : ℕ
p q : ℕ × ℕ
hp : p ∈ antidiagonal n
hq : q ∈ antidiagonal n
h : p.fst = q.fst
⊢ q.fst + p.snd = q.fst + q.snd
[PROOFSTEP]
rw [mem_antidiagonal] at hp hq 
[GOAL]
n : ℕ
p q : ℕ × ℕ
hp : p.fst + p.snd = n
hq : q.fst + q.snd = n
h : p.fst = q.fst
⊢ q.fst + p.snd = q.fst + q.snd
[PROOFSTEP]
rw [hq, ← h, hp]
[GOAL]
n : ℕ
kl : ℕ × ℕ
hlk : kl ∈ antidiagonal n
⊢ kl.fst ≤ n
[PROOFSTEP]
rw [le_iff_exists_add]
[GOAL]
n : ℕ
kl : ℕ × ℕ
hlk : kl ∈ antidiagonal n
⊢ ∃ c, n = kl.fst + c
[PROOFSTEP]
use kl.2
[GOAL]
case h
n : ℕ
kl : ℕ × ℕ
hlk : kl ∈ antidiagonal n
⊢ n = kl.fst + kl.snd
[PROOFSTEP]
rwa [mem_antidiagonal, eq_comm] at hlk 
[GOAL]
n : ℕ
kl : ℕ × ℕ
hlk : kl ∈ antidiagonal n
⊢ kl.snd ≤ n
[PROOFSTEP]
rw [le_iff_exists_add]
[GOAL]
n : ℕ
kl : ℕ × ℕ
hlk : kl ∈ antidiagonal n
⊢ ∃ c, n = kl.snd + c
[PROOFSTEP]
use kl.1
[GOAL]
case h
n : ℕ
kl : ℕ × ℕ
hlk : kl ∈ antidiagonal n
⊢ n = kl.snd + kl.fst
[PROOFSTEP]
rwa [mem_antidiagonal, eq_comm, add_comm] at hlk 
[GOAL]
n m : ℕ
⊢ filter (fun x => x.fst = m) (antidiagonal n) = if m ≤ n then {(m, n - m)} else ∅
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case a.mk
n m x y : ℕ
⊢ (x, y) ∈ filter (fun x => x.fst = m) (antidiagonal n) ↔ (x, y) ∈ if m ≤ n then {(m, n - m)} else ∅
[PROOFSTEP]
simp only [mem_filter, Nat.mem_antidiagonal]
[GOAL]
case a.mk
n m x y : ℕ
⊢ x + y = n ∧ x = m ↔ (x, y) ∈ if m ≤ n then {(m, n - m)} else ∅
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
n m x y : ℕ
h : m ≤ n
⊢ x + y = n ∧ x = m ↔ (x, y) ∈ {(m, n - m)}
[PROOFSTEP]
simp (config := { contextual := true }) [and_comm, eq_tsub_iff_add_eq_of_le h, add_comm]
[GOAL]
case neg
n m x y : ℕ
h : ¬m ≤ n
⊢ x + y = n ∧ x = m ↔ (x, y) ∈ ∅
[PROOFSTEP]
rw [not_le] at h 
[GOAL]
case neg
n m x y : ℕ
h : n < m
⊢ x + y = n ∧ x = m ↔ (x, y) ∈ ∅
[PROOFSTEP]
simp only [not_mem_empty, iff_false_iff, not_and, decide_eq_true_eq]
[GOAL]
case neg
n m x y : ℕ
h : n < m
⊢ x + y = n → ¬x = m
[PROOFSTEP]
exact fun hn => ne_of_lt (lt_of_le_of_lt (le_self_add.trans hn.le) h)
[GOAL]
n m : ℕ
⊢ filter (fun x => x.snd = m) (antidiagonal n) = if m ≤ n then {(n - m, m)} else ∅
[PROOFSTEP]
have : (fun x : ℕ × ℕ ↦ (x.snd = m)) ∘ Prod.swap = fun x : ℕ × ℕ ↦ x.fst = m := by ext; simp
[GOAL]
n m : ℕ
⊢ (fun x => x.snd = m) ∘ Prod.swap = fun x => x.fst = m
[PROOFSTEP]
ext
[GOAL]
case h.a
n m : ℕ
x✝ : ℕ × ℕ
⊢ ((fun x => x.snd = m) ∘ Prod.swap) x✝ ↔ x✝.fst = m
[PROOFSTEP]
simp
[GOAL]
n m : ℕ
this : (fun x => x.snd = m) ∘ Prod.swap = fun x => x.fst = m
⊢ filter (fun x => x.snd = m) (antidiagonal n) = if m ≤ n then {(n - m, m)} else ∅
[PROOFSTEP]
rw [← map_swap_antidiagonal, filter_map]
[GOAL]
n m : ℕ
this : (fun x => x.snd = m) ∘ Prod.swap = fun x => x.fst = m
⊢ map { toFun := Prod.swap, inj' := (_ : Injective Prod.swap) }
      (filter ((fun x => x.snd = m) ∘ ↑{ toFun := Prod.swap, inj' := (_ : Injective Prod.swap) }) (antidiagonal n)) =
    if m ≤ n then {(n - m, m)} else ∅
[PROOFSTEP]
simp [this, filter_fst_eq_antidiagonal, apply_ite (Finset.map _)]
[GOAL]
n k : ℕ
h : k ≤ n
⊢ filter (fun a => a.snd ≤ k) (antidiagonal n) =
    map
      (Embedding.prodMap { toFun := fun x => x + (n - k), inj' := (_ : Injective fun x => x + (n - k)) }
        (Embedding.refl ℕ))
      (antidiagonal k)
[PROOFSTEP]
ext ⟨i, j⟩
[GOAL]
case a.mk
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ (i, j) ∈ filter (fun a => a.snd ≤ k) (antidiagonal n) ↔
    (i, j) ∈
      map
        (Embedding.prodMap { toFun := fun x => x + (n - k), inj' := (_ : Injective fun x => x + (n - k)) }
          (Embedding.refl ℕ))
        (antidiagonal k)
[PROOFSTEP]
suffices : i + j = n ∧ j ≤ k ↔ ∃ a, a + j = k ∧ a + (n - k) = i
[GOAL]
case a.mk
n k : ℕ
h : k ≤ n
i j : ℕ
this : i + j = n ∧ j ≤ k ↔ ∃ a, a + j = k ∧ a + (n - k) = i
⊢ (i, j) ∈ filter (fun a => a.snd ≤ k) (antidiagonal n) ↔
    (i, j) ∈
      map
        (Embedding.prodMap { toFun := fun x => x + (n - k), inj' := (_ : Injective fun x => x + (n - k)) }
          (Embedding.refl ℕ))
        (antidiagonal k)
[PROOFSTEP]
simpa
[GOAL]
case this
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ i + j = n ∧ j ≤ k ↔ ∃ a, a + j = k ∧ a + (n - k) = i
[PROOFSTEP]
refine' ⟨fun hi ↦ ⟨k - j, tsub_add_cancel_of_le hi.2, _⟩, _⟩
[GOAL]
case this.refine'_1
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ j ≤ k
⊢ k - j + (n - k) = i
[PROOFSTEP]
rw [add_comm, tsub_add_eq_add_tsub h, ← hi.1, add_assoc, Nat.add_sub_of_le hi.2, add_tsub_cancel_right]
[GOAL]
case this.refine'_2
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ (∃ a, a + j = k ∧ a + (n - k) = i) → i + j = n ∧ j ≤ k
[PROOFSTEP]
rintro ⟨l, hl, rfl⟩
[GOAL]
case this.refine'_2.intro.intro
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ l + (n - k) + j = n ∧ j ≤ k
[PROOFSTEP]
refine' ⟨_, hl ▸ Nat.le_add_left j l⟩
[GOAL]
case this.refine'_2.intro.intro
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ l + (n - k) + j = n
[PROOFSTEP]
rw [add_assoc, add_comm, add_assoc, add_comm j l, hl]
[GOAL]
case this.refine'_2.intro.intro
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ n - k + k = n
[PROOFSTEP]
exact Nat.sub_add_cancel h
[GOAL]
n k : ℕ
h : k ≤ n
⊢ filter (fun a => a.fst ≤ k) (antidiagonal n) =
    map
      (Embedding.prodMap (Embedding.refl ℕ)
        { toFun := fun x => x + (n - k), inj' := (_ : Injective fun x => x + (n - k)) })
      (antidiagonal k)
[PROOFSTEP]
have aux₁ : (fun a ↦ a.fst ≤ k) = (fun a ↦ a.snd ≤ k) ∘ (Equiv.prodComm ℕ ℕ).symm := rfl
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => a.fst ≤ k) = (fun a => a.snd ≤ k) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
⊢ filter (fun a => a.fst ≤ k) (antidiagonal n) =
    map
      (Embedding.prodMap (Embedding.refl ℕ)
        { toFun := fun x => x + (n - k), inj' := (_ : Injective fun x => x + (n - k)) })
      (antidiagonal k)
[PROOFSTEP]
have aux₂ : ∀ i j, (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j :=
  fun i j ↦ by rw [exists_comm]; exact exists₂_congr (fun a b ↦ by rw [add_comm])
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => a.fst ≤ k) = (fun a => a.snd ≤ k) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
i j : ℕ
⊢ (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j
[PROOFSTEP]
rw [exists_comm]
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => a.fst ≤ k) = (fun a => a.snd ≤ k) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
i j : ℕ
⊢ (∃ b a, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j
[PROOFSTEP]
exact exists₂_congr (fun a b ↦ by rw [add_comm])
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => a.fst ≤ k) = (fun a => a.snd ≤ k) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
i j a b : ℕ
⊢ b + a = k ∧ a = i ∧ b + (n - k) = j ↔ a + b = k ∧ a = i ∧ b + (n - k) = j
[PROOFSTEP]
rw [add_comm]
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => a.fst ≤ k) = (fun a => a.snd ≤ k) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j
⊢ filter (fun a => a.fst ≤ k) (antidiagonal n) =
    map
      (Embedding.prodMap (Embedding.refl ℕ)
        { toFun := fun x => x + (n - k), inj' := (_ : Injective fun x => x + (n - k)) })
      (antidiagonal k)
[PROOFSTEP]
rw [← map_prodComm_antidiagonal]
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => a.fst ≤ k) = (fun a => a.snd ≤ k) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j
⊢ filter (fun a => a.fst ≤ k) (map (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)) (antidiagonal n)) =
    map
      (Embedding.prodMap (Embedding.refl ℕ)
        { toFun := fun x => x + (n - k), inj' := (_ : Injective fun x => x + (n - k)) })
      (antidiagonal k)
[PROOFSTEP]
simp_rw [aux₁, ← map_filter, antidiagonal_filter_snd_le_of_le h, map_map]
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => a.fst ≤ k) = (fun a => a.snd ≤ k) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j
⊢ map
      (Embedding.trans
        (Embedding.prodMap { toFun := fun x => x + (n - k), inj' := (_ : Injective fun x => x + (n - k)) }
          (Embedding.refl ℕ))
        (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)))
      (antidiagonal k) =
    map
      (Embedding.prodMap (Embedding.refl ℕ)
        { toFun := fun x => x + (n - k), inj' := (_ : Injective fun x => x + (n - k)) })
      (antidiagonal k)
[PROOFSTEP]
ext ⟨i, j⟩
[GOAL]
case a.mk
n k : ℕ
h : k ≤ n
aux₁ : (fun a => a.fst ≤ k) = (fun a => a.snd ≤ k) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j
i j : ℕ
⊢ (i, j) ∈
      map
        (Embedding.trans
          (Embedding.prodMap { toFun := fun x => x + (n - k), inj' := (_ : Injective fun x => x + (n - k)) }
            (Embedding.refl ℕ))
          (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)))
        (antidiagonal k) ↔
    (i, j) ∈
      map
        (Embedding.prodMap (Embedding.refl ℕ)
          { toFun := fun x => x + (n - k), inj' := (_ : Injective fun x => x + (n - k)) })
        (antidiagonal k)
[PROOFSTEP]
simpa using aux₂ i j
[GOAL]
n k : ℕ
h : k ≤ n
⊢ filter (fun a => k ≤ a.fst) (antidiagonal n) =
    map (Embedding.prodMap { toFun := fun x => x + k, inj' := (_ : Injective fun x => x + k) } (Embedding.refl ℕ))
      (antidiagonal (n - k))
[PROOFSTEP]
ext ⟨i, j⟩
[GOAL]
case a.mk
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ (i, j) ∈ filter (fun a => k ≤ a.fst) (antidiagonal n) ↔
    (i, j) ∈
      map (Embedding.prodMap { toFun := fun x => x + k, inj' := (_ : Injective fun x => x + k) } (Embedding.refl ℕ))
        (antidiagonal (n - k))
[PROOFSTEP]
suffices : i + j = n ∧ k ≤ i ↔ ∃ a, a + j = n - k ∧ a + k = i
[GOAL]
case a.mk
n k : ℕ
h : k ≤ n
i j : ℕ
this : i + j = n ∧ k ≤ i ↔ ∃ a, a + j = n - k ∧ a + k = i
⊢ (i, j) ∈ filter (fun a => k ≤ a.fst) (antidiagonal n) ↔
    (i, j) ∈
      map (Embedding.prodMap { toFun := fun x => x + k, inj' := (_ : Injective fun x => x + k) } (Embedding.refl ℕ))
        (antidiagonal (n - k))
[PROOFSTEP]
simpa
[GOAL]
case this
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ i + j = n ∧ k ≤ i ↔ ∃ a, a + j = n - k ∧ a + k = i
[PROOFSTEP]
refine' ⟨fun hi ↦ ⟨i - k, _, tsub_add_cancel_of_le hi.2⟩, _⟩
[GOAL]
case this.refine'_1
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ k ≤ i
⊢ i - k + j = n - k
[PROOFSTEP]
rw [← Nat.sub_add_comm hi.2, hi.1]
[GOAL]
case this.refine'_2
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ (∃ a, a + j = n - k ∧ a + k = i) → i + j = n ∧ k ≤ i
[PROOFSTEP]
rintro ⟨l, hl, rfl⟩
[GOAL]
case this.refine'_2.intro.intro
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ l + k + j = n ∧ k ≤ l + k
[PROOFSTEP]
refine' ⟨_, Nat.le_add_left k l⟩
[GOAL]
case this.refine'_2.intro.intro
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ l + k + j = n
[PROOFSTEP]
rw [add_right_comm, hl]
[GOAL]
case this.refine'_2.intro.intro
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ n - k + k = n
[PROOFSTEP]
exact tsub_add_cancel_of_le h
[GOAL]
n k : ℕ
h : k ≤ n
⊢ filter (fun a => k ≤ a.snd) (antidiagonal n) =
    map (Embedding.prodMap (Embedding.refl ℕ) { toFun := fun x => x + k, inj' := (_ : Injective fun x => x + k) })
      (antidiagonal (n - k))
[PROOFSTEP]
have aux₁ : (fun a ↦ k ≤ a.snd) = (fun a ↦ k ≤ a.fst) ∘ (Equiv.prodComm ℕ ℕ).symm := rfl
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.snd) = (fun a => k ≤ a.fst) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
⊢ filter (fun a => k ≤ a.snd) (antidiagonal n) =
    map (Embedding.prodMap (Embedding.refl ℕ) { toFun := fun x => x + k, inj' := (_ : Injective fun x => x + k) })
      (antidiagonal (n - k))
[PROOFSTEP]
have aux₂ : ∀ i j, (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j := fun i j ↦ by
  rw [exists_comm]; exact exists₂_congr (fun a b ↦ by rw [add_comm])
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.snd) = (fun a => k ≤ a.fst) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
i j : ℕ
⊢ (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
[PROOFSTEP]
rw [exists_comm]
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.snd) = (fun a => k ≤ a.fst) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
i j : ℕ
⊢ (∃ b a, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
[PROOFSTEP]
exact exists₂_congr (fun a b ↦ by rw [add_comm])
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.snd) = (fun a => k ≤ a.fst) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
i j a b : ℕ
⊢ b + a = n - k ∧ a = i ∧ b + k = j ↔ a + b = n - k ∧ a = i ∧ b + k = j
[PROOFSTEP]
rw [add_comm]
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.snd) = (fun a => k ≤ a.fst) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
⊢ filter (fun a => k ≤ a.snd) (antidiagonal n) =
    map (Embedding.prodMap (Embedding.refl ℕ) { toFun := fun x => x + k, inj' := (_ : Injective fun x => x + k) })
      (antidiagonal (n - k))
[PROOFSTEP]
rw [← map_prodComm_antidiagonal]
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.snd) = (fun a => k ≤ a.fst) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
⊢ filter (fun a => k ≤ a.snd) (map (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)) (antidiagonal n)) =
    map (Embedding.prodMap (Embedding.refl ℕ) { toFun := fun x => x + k, inj' := (_ : Injective fun x => x + k) })
      (antidiagonal (n - k))
[PROOFSTEP]
simp_rw [aux₁, ← map_filter, antidiagonal_filter_le_fst_of_le h, map_map]
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.snd) = (fun a => k ≤ a.fst) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
⊢ map
      (Embedding.trans
        (Embedding.prodMap { toFun := fun x => x + k, inj' := (_ : Injective fun x => x + k) } (Embedding.refl ℕ))
        (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)))
      (antidiagonal (n - k)) =
    map (Embedding.prodMap (Embedding.refl ℕ) { toFun := fun x => x + k, inj' := (_ : Injective fun x => x + k) })
      (antidiagonal (n - k))
[PROOFSTEP]
ext ⟨i, j⟩
[GOAL]
case a.mk
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.snd) = (fun a => k ≤ a.fst) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
i j : ℕ
⊢ (i, j) ∈
      map
        (Embedding.trans
          (Embedding.prodMap { toFun := fun x => x + k, inj' := (_ : Injective fun x => x + k) } (Embedding.refl ℕ))
          (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)))
        (antidiagonal (n - k)) ↔
    (i, j) ∈
      map (Embedding.prodMap (Embedding.refl ℕ) { toFun := fun x => x + k, inj' := (_ : Injective fun x => x + k) })
        (antidiagonal (n - k))
[PROOFSTEP]
simpa using aux₂ i j
[GOAL]
⊢ LeftInverse
    (fun x => { fst := x.fst + x.snd, snd := { val := x, property := (_ : x ∈ antidiagonal (x.fst + x.snd)) } })
    fun x => ↑x.snd
[PROOFSTEP]
rintro ⟨n, ⟨k, l⟩, h⟩
[GOAL]
case mk.mk.mk
n k l : ℕ
h : (k, l) ∈ antidiagonal n
⊢ (fun x => { fst := x.fst + x.snd, snd := { val := x, property := (_ : x ∈ antidiagonal (x.fst + x.snd)) } })
      ((fun x => ↑x.snd) { fst := n, snd := { val := (k, l), property := h } }) =
    { fst := n, snd := { val := (k, l), property := h } }
[PROOFSTEP]
rw [mem_antidiagonal] at h 
[GOAL]
case mk.mk.mk
n k l : ℕ
h✝ : (k, l) ∈ antidiagonal n
h : (k, l).fst + (k, l).snd = n
⊢ (fun x => { fst := x.fst + x.snd, snd := { val := x, property := (_ : x ∈ antidiagonal (x.fst + x.snd)) } })
      ((fun x => ↑x.snd) { fst := n, snd := { val := (k, l), property := h✝ } }) =
    { fst := n, snd := { val := (k, l), property := h✝ } }
[PROOFSTEP]
exact Sigma.subtype_ext h rfl
