n : ℕ
⊢ (List.bind (range n) fun a => map (fun x => Fin.cons a x) (antidiagonalTuple 0 (n - a))) ++
      map (fun x => Fin.cons n x) (antidiagonalTuple 0 0) =
    [![n]]
n : ℕ
⊢ antidiagonalTuple 1 n = [![n]]
simp_rw [antidiagonalTuple, antidiagonal, List.range_succ, List.map_append, List.map_singleton,
  tsub_self, List.bind_append, List.bind_singleton, List.map_bind]
n : ℕ
⊢ (List.bind (range n) fun a => map (fun x => Fin.cons a x) (antidiagonalTuple 0 (n - a))) ++
      map (fun x => Fin.cons n x) (antidiagonalTuple 0 0) =
    [] ++ [![n]]
n : ℕ
⊢ (List.bind (range n) fun a => map (fun x => Fin.cons a x) (antidiagonalTuple 0 (n - a))) ++
      map (fun x => Fin.cons n x) (antidiagonalTuple 0 0) =
    [![n]]
conv_rhs => rw [← List.nil_append [![n]]]
case e_a
n : ℕ
⊢ (List.bind (range n) fun a => map (fun x => Fin.cons a x) (antidiagonalTuple 0 (n - a))) = []
n : ℕ
⊢ (List.bind (range n) fun a => map (fun x => Fin.cons a x) (antidiagonalTuple 0 (n - a))) ++
      map (fun x => Fin.cons n x) (antidiagonalTuple 0 0) =
    [] ++ [![n]]
congr 1
case e_a
n : ℕ
⊢ ∀ (x : ℕ), x < n → antidiagonalTuple 0 (n - x) = []
case e_a
n : ℕ
⊢ (List.bind (range n) fun a => map (fun x => Fin.cons a x) (antidiagonalTuple 0 (n - a))) = []
simp_rw [List.bind_eq_nil, List.mem_range, List.map_eq_nil]
case e_a
n x : ℕ
hx : x < n
⊢ antidiagonalTuple 0 (n - x) = []
case e_a
n : ℕ
⊢ ∀ (x : ℕ), x < n → antidiagonalTuple 0 (n - x) = []
intro x hx
case e_a.intro
x m : ℕ
hx : x < x + m + 1
⊢ antidiagonalTuple 0 (x + m + 1 - x) = []
case e_a
n x : ℕ
hx : x < n
⊢ antidiagonalTuple 0 (n - x) = []
obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_lt hx
no goals
case e_a.intro
x m : ℕ
hx : x < x + m + 1
⊢ antidiagonalTuple 0 (x + m + 1 - x) = []
rw [add_assoc, add_tsub_cancel_left, antidiagonalTuple_zero_succ]