n : ℕ
⊢ (List.bind (antidiagonal n) fun ni => map (fun x => Fin.cons ni.fst x) (antidiagonalTuple 1 ni.snd)) =
    map (fun i => ![i.fst, i.snd]) (antidiagonal n)
n : ℕ
⊢ antidiagonalTuple 2 n = map (fun i => ![i.fst, i.snd]) (antidiagonal n)
rw [antidiagonalTuple]
n : ℕ
⊢ (List.bind (antidiagonal n) fun ni => [Fin.cons ni.fst ![ni.snd]]) = map (fun i => ![i.fst, i.snd]) (antidiagonal n)
n : ℕ
⊢ (List.bind (antidiagonal n) fun ni => map (fun x => Fin.cons ni.fst x) (antidiagonalTuple 1 ni.snd)) =
    map (fun i => ![i.fst, i.snd]) (antidiagonal n)
simp_rw [antidiagonalTuple_one, List.map_singleton]
n : ℕ
⊢ (List.bind (antidiagonal n) fun ni => [Fin.cons ni.fst ![ni.snd]]) =
    List.bind (antidiagonal n) fun x => [![x.fst, x.snd]]
n : ℕ
⊢ (List.bind (antidiagonal n) fun ni => [Fin.cons ni.fst ![ni.snd]]) = map (fun i => ![i.fst, i.snd]) (antidiagonal n)
rw [List.map_eq_bind]
no goals
n : ℕ
⊢ (List.bind (antidiagonal n) fun ni => [Fin.cons ni.fst ![ni.snd]]) =
    List.bind (antidiagonal n) fun x => [![x.fst, x.snd]]
rfl