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))
n : ℕ
⊢ map Prod.swap (antidiagonal n) = reverse (antidiagonal n)
rw [antidiagonal, map_map, ← List.map_reverse, range_eq_range', reverse_range', ←
  range_eq_range', map_map]
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
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))
apply map_congr
no goals
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
simp (config := { contextual := true }) [Nat.sub_sub_self, lt_succ_iff]