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)]
n : ℕ
⊢ antidiagonal (n + 1) = map (Prod.map id succ) (antidiagonal n) ++ [(n + 1, 0)]
simp only [antidiagonal, range_succ, add_tsub_cancel_left, map_append, append_assoc, tsub_self,
  singleton_append, map_map, map]
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)
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)]
congr 1
case e_a.a
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range n → (x, n + 1 - x) = (Prod.map id succ ∘ fun i => (i, n - i)) x
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)
apply map_congr
no goals
case e_a.a
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range n → (x, n + 1 - x) = (Prod.map id succ ∘ fun i => (i, n - i)) x
simp (config := { contextual := true }) [le_of_lt, Nat.succ_eq_add_one, Nat.sub_add_comm]