[GOAL]
n : ℕ
x : ℕ × ℕ
⊢ x ∈ antidiagonal n ↔ x.fst + x.snd = n
[PROOFSTEP]
rw [antidiagonal, mem_coe, List.Nat.mem_antidiagonal]
[GOAL]
n : ℕ
⊢ ↑card (antidiagonal n) = n + 1
[PROOFSTEP]
rw [antidiagonal, coe_card, List.Nat.length_antidiagonal]
[GOAL]
n : ℕ
⊢ antidiagonal (n + 1) = (0, n + 1) ::ₘ map (Prod.map Nat.succ id) (antidiagonal n)
[PROOFSTEP]
simp only [antidiagonal, List.Nat.antidiagonal_succ, coe_map, cons_coe]
[GOAL]
n : ℕ
⊢ antidiagonal (n + 1) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
[PROOFSTEP]
rw [antidiagonal, List.Nat.antidiagonal_succ', ← coe_add, add_comm, antidiagonal, coe_map, coe_add,
  List.singleton_append, cons_coe]
[GOAL]
n : ℕ
⊢ antidiagonal (n + 2) = (0, n + 2) ::ₘ (n + 2, 0) ::ₘ map (Prod.map Nat.succ Nat.succ) (antidiagonal n)
[PROOFSTEP]
rw [antidiagonal_succ, antidiagonal_succ', map_cons, map_map, Prod_map]
[GOAL]
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)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ map Prod.swap (antidiagonal n) = antidiagonal n
[PROOFSTEP]
rw [antidiagonal, coe_map, List.Nat.map_swap_antidiagonal, coe_reverse]
