n : ℕ
⊢ (0, n + 1 + 1) ::ₘ
      (Nat.succ (n + 1, 0).fst, id (n + 1, 0).snd) ::ₘ
        map (Prod.map Nat.succ id ∘ Prod.map id Nat.succ) (antidiagonal n) =
    (0, n + 2) ::ₘ (n + 2, 0) ::ₘ map (Prod.map Nat.succ Nat.succ) (antidiagonal n)
n : ℕ
⊢ antidiagonal (n + 2) = (0, n + 2) ::ₘ (n + 2, 0) ::ₘ map (Prod.map Nat.succ Nat.succ) (antidiagonal n)
rw [antidiagonal_succ, antidiagonal_succ', map_cons, map_map, Prod_map]
no goals
n : ℕ
⊢ (0, n + 1 + 1) ::ₘ
      (Nat.succ (n + 1, 0).fst, id (n + 1, 0).snd) ::ₘ
        map (Prod.map Nat.succ id ∘ Prod.map id Nat.succ) (antidiagonal n) =
    (0, n + 2) ::ₘ (n + 2, 0) ::ₘ map (Prod.map Nat.succ Nat.succ) (antidiagonal n)
rfl