[GOAL]
n : ℕ
x : ℕ × ℕ
⊢ x ∈ antidiagonal n ↔ x.fst + x.snd = n
[PROOFSTEP]
rw [antidiagonal, mem_map]
[GOAL]
n : ℕ
x : ℕ × ℕ
⊢ (∃ a, a ∈ range (n + 1) ∧ (a, n - a) = x) ↔ x.fst + x.snd = n
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
x : ℕ × ℕ
⊢ (∃ a, a ∈ range (n + 1) ∧ (a, n - a) = x) → x.fst + x.snd = n
[PROOFSTEP]
rintro ⟨i, hi, rfl⟩
[GOAL]
case mp.intro.intro
n i : ℕ
hi : i ∈ range (n + 1)
⊢ (i, n - i).fst + (i, n - i).snd = n
[PROOFSTEP]
rw [mem_range, lt_succ_iff] at hi 
[GOAL]
case mp.intro.intro
n i : ℕ
hi : i ≤ n
⊢ (i, n - i).fst + (i, n - i).snd = n
[PROOFSTEP]
exact add_tsub_cancel_of_le hi
[GOAL]
case mpr
n : ℕ
x : ℕ × ℕ
⊢ x.fst + x.snd = n → ∃ a, a ∈ range (n + 1) ∧ (a, n - a) = x
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
x : ℕ × ℕ
⊢ ∃ a, a ∈ range (x.fst + x.snd + 1) ∧ (a, x.fst + x.snd - a) = x
[PROOFSTEP]
refine' ⟨x.fst, _, _⟩
[GOAL]
case mpr.refine'_1
x : ℕ × ℕ
⊢ x.fst ∈ range (x.fst + x.snd + 1)
[PROOFSTEP]
rw [mem_range, add_assoc, lt_add_iff_pos_right]
[GOAL]
case mpr.refine'_1
x : ℕ × ℕ
⊢ 0 < x.snd + 1
[PROOFSTEP]
exact zero_lt_succ _
[GOAL]
case mpr.refine'_2
x : ℕ × ℕ
⊢ (x.fst, x.fst + x.snd - x.fst) = x
[PROOFSTEP]
exact Prod.ext rfl (by simp only [add_tsub_cancel_left])
[GOAL]
x : ℕ × ℕ
⊢ (x.fst, x.fst + x.snd - x.fst).snd = x.snd
[PROOFSTEP]
simp only [add_tsub_cancel_left]
[GOAL]
n : ℕ
⊢ length (antidiagonal n) = n + 1
[PROOFSTEP]
rw [antidiagonal, length_map, length_range]
[GOAL]
n : ℕ
⊢ antidiagonal (n + 1) = (0, n + 1) :: map (Prod.map succ id) (antidiagonal n)
[PROOFSTEP]
simp only [antidiagonal, range_succ_eq_map, map_cons, true_and_iff, Nat.add_succ_sub_one, add_zero, id.def,
  eq_self_iff_true, tsub_zero, map_map, Prod.map_mk]
[GOAL]
n : ℕ
⊢ (0, n + 1) :: (succ 0, n) :: map ((fun i => (i, n + 1 - i)) ∘ succ ∘ succ) (range n) =
    (0, n + 1) :: (succ 0, n) :: map (Prod.map succ id ∘ (fun i => (i, n - i)) ∘ succ) (range n)
[PROOFSTEP]
apply congr rfl (congr rfl _)
[GOAL]
n : ℕ
⊢ map ((fun i => (i, n + 1 - i)) ∘ succ ∘ succ) (range n) =
    map (Prod.map succ id ∘ (fun i => (i, n - i)) ∘ succ) (range n)
[PROOFSTEP]
ext
[GOAL]
case a.a
n n✝ : ℕ
a✝ : ℕ × ℕ
⊢ a✝ ∈ get? (map ((fun i => (i, n + 1 - i)) ∘ succ ∘ succ) (range n)) n✝ ↔
    a✝ ∈ get? (map (Prod.map succ id ∘ (fun i => (i, n - i)) ∘ succ) (range n)) n✝
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ antidiagonal (n + 1) = map (Prod.map id succ) (antidiagonal n) ++ [(n + 1, 0)]
[PROOFSTEP]
simp only [antidiagonal, range_succ, add_tsub_cancel_left, map_append, append_assoc, tsub_self, singleton_append,
  map_map, map]
[GOAL]
n : ℕ
⊢ map (fun i => (i, n + 1 - i)) (range n) ++ [(n, 1), (n + 1, 0)] =
    map (Prod.map id succ ∘ fun i => (i, n - i)) (range n) ++ [Prod.map id succ (n, 0), (n + 1, 0)]
[PROOFSTEP]
congr 1
[GOAL]
case e_a
n : ℕ
⊢ map (fun i => (i, n + 1 - i)) (range n) = map (Prod.map id succ ∘ fun i => (i, n - i)) (range n)
[PROOFSTEP]
apply map_congr
[GOAL]
case e_a.a
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range n → (x, n + 1 - x) = (Prod.map id succ ∘ fun i => (i, n - i)) x
[PROOFSTEP]
simp (config := { contextual := true }) [le_of_lt, Nat.succ_eq_add_one, Nat.sub_add_comm]
[GOAL]
n : ℕ
⊢ antidiagonal (n + 2) = (0, n + 2) :: map (Prod.map succ succ) (antidiagonal n) ++ [(n + 2, 0)]
[PROOFSTEP]
rw [antidiagonal_succ']
[GOAL]
n : ℕ
⊢ map (Prod.map id succ) (antidiagonal (n + 1)) ++ [(n + 1 + 1, 0)] =
    (0, n + 2) :: map (Prod.map succ succ) (antidiagonal n) ++ [(n + 2, 0)]
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ map (Prod.map id succ ∘ Prod.map succ id) (antidiagonal n) = map (Prod.map succ succ) (antidiagonal n)
[PROOFSTEP]
ext
[GOAL]
case a.a
n n✝ : ℕ
a✝ : ℕ × ℕ
⊢ a✝ ∈ get? (map (Prod.map id succ ∘ Prod.map succ id) (antidiagonal n)) n✝ ↔
    a✝ ∈ get? (map (Prod.map succ succ) (antidiagonal n)) n✝
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ map Prod.swap (antidiagonal n) = reverse (antidiagonal n)
[PROOFSTEP]
rw [antidiagonal, map_map, ← List.map_reverse, range_eq_range', reverse_range', ← range_eq_range', map_map]
[GOAL]
n : ℕ
⊢ map (Prod.swap ∘ fun i => (i, n - i)) (range (n + 1)) =
    map ((fun i => (i, n - i)) ∘ fun x => 0 + (n + 1) - 1 - x) (range (n + 1))
[PROOFSTEP]
apply map_congr
[GOAL]
case a
n : ℕ
⊢ ∀ (x : ℕ),
    x ∈ range (n + 1) → (Prod.swap ∘ fun i => (i, n - i)) x = ((fun i => (i, n - i)) ∘ fun x => 0 + (n + 1) - 1 - x) x
[PROOFSTEP]
simp (config := { contextual := true }) [Nat.sub_sub_self, lt_succ_iff]
