import data.nat.choose.basic
import data.nat.fib
import data.list.defs
import data.list.nat_antidiagonal
open function
lemma list.sum_map_add {ι α : Type*} [add_comm_monoid α] {f g : ι → α} (l : list ι) :
(l.map (λ x, f x + g x)).sum = (l.map f).sum + (l.map g).sum :=
list.sum_hom₂ _ _ add_add_add_comm (add_zero _) _ _
lemma list.nat.antidiagonal_succ' (n : ℕ) :
list.nat.antidiagonal (n + 1) =
((list.nat.antidiagonal n).map (prod.map id nat.succ)) ++ [(n + 1, 0)] :=
begin
simp only [list.nat.antidiagonal, list.range_succ, add_tsub_cancel_left, list.map_append,
list.append_assoc, tsub_self, list.singleton_append, list.map_map, list.map],
congr' 1,
apply list.map_congr,
simp [le_of_lt, nat.succ_eq_add_one, nat.sub_add_comm] { contextual := tt },
end
lemma list.nat.antidiagonal_succ_succ' (n : ℕ) :
list.nat.antidiagonal (n + 2) =
(0, n + 2) :: ((list.nat.antidiagonal n).map (prod.map nat.succ nat.succ)) ++ [(n + 2, 0)] :=
begin
induction n with n ih,
{ refl, },
{ rw [nat.succ_add, list.nat.antidiagonal_succ, ih],
simpa, },
end
theorem fib_eq_sum_choose_antidiagonal (n : ℕ) :
(n + 1).fib = ((list.nat.antidiagonal n).map (uncurry nat.choose)).sum :=
begin
induction n using nat.two_step_induction with n h0 h1,
{ refl, },
{ refl, },
rw [nat.fib_add_two, h0, h1, list.nat.antidiagonal_succ_succ', list.nat.antidiagonal_succ'],
simpa [←add_assoc, ←list.sum_map_add, uncurry, ←nat.choose_succ_succ],
end
``` All that said, using lists isn't the usual way you work with sums in mathlib. Instead, you work with finset and the "big operators." Contingent on the mathlib PR for manipulating antidiagonals, the theorem ends up being just this:
import data.finset.nat_antidiagonal
import data.nat.fib
import algebra.big_operators.basic
open_locale big_operators
open finset
theorem fib_eq_sum_choose_antidiagonal (n : ℕ) :
(n + 1).fib = ∑ p in nat.antidiagonal n, nat.choose p.1 p.2 :=
begin
induction n using nat.two_step_induction with n h0 h1,
{ refl, },
{ refl, },
rw [nat.fib_add_two, h0, h1, nat.antidiagonal_succ_succ', nat.antidiagonal_succ'],
simp [nat.choose_succ_succ, add_assoc, add_left_comm, sum_add_distrib],
end
After doing the basic manipulations you described in your proof outline, simp ends up doing the heavy lifting. An interesting thing about this tactic is that it's able to put things into a normal form even if the lemmas can potentially form rewrite loops. The add_assoc and add_left_comm lemmas here are giving simp the capability of sorting the additions, as a weak kind of ring. (Usually you'd include add_comm, too, but it wasn't necessary here.)