I'll first go through piece-by-piece and suggest some local improvements.
For the induction principle, when you find yourself doing intros as the first step of a tactic proof, you should strongly consider putting arguments "before the colon" rather than leaving them within universal quantifiers. Another thing is that when you have multiple goals (for example, as produced by have or induction) it is good practice to use curly braces to focus on the goal -- that way when the proof breaks you can more easily figure out what needs fixing. And, a tip: if you are using the same tactic on each goal produced by a tactic, you can use the ; operator.
lemma fib_ind (P : ℕ → Prop)
(p0 : P 0) (p1 : P 1) (pss : ∀ m : ℕ, P m → P m.succ → P m.succ.succ) (n : ℕ) : P n :=
begin
have pns : P n /\ P n.succ,
{ induction n; tauto },
tauto,
end
For naming, we can refer to mathlib itself: it's nat.two_step_induction, so we can replace the tactic proof with the term nat.two_step_induction p0 p1 pss n. Note: the P argument would more commonly be given as an implicit argument.
The next lemma gets a similar treatment, but, with list.map, you can make use of dot notation: l.map f means "since l has type list, use list.map and have l be its first list argument." Since this lemma is about a homomorphism property, I think it would normally be written with the equality flipped, and for naming, this might be unnecessarily long, but sum_map_apply_add_apply would work (one way mathlib names arise is to read off relevant parts of the in-order traversal of the abstract syntax tree). Also, non-terminal simps should be avoided, since if the simp set later changes, you can have a hard time fixing a proof. I used squeeze_simp to figure out which lemmas it was using, and I inserted *, which means "and rewrite using hypothesis from the local context."
lemma sum_map_apply_add_apply (f g : ℕ → ℕ) (l : list ℕ) :
(l.map (λ x, f x + g x)).sum = (l.map f).sum + (l.map g).sum :=
begin
induction l,
{ simp, },
{ simp only [list.sum_cons, list.map, *],
ring, },
end
However, searching the documentation for "list sum map add", I came across multiset.sum_map_add. The proof in the source code (after interpreting what the to_additive attribute does) essentially carries over to lists. After generalizing it appropriately, this should probably find its way into mathlib:
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 _) _ _
The next lemma boils down to the fact that l.map f = l.map g (a congruence lemma), so searching for "list map congr" I got this:
lemma sum_eq_elementwise (f g : ℕ → ℕ) (l : list ℕ) (h : ∀ x, x ∈ l → f x = g x) :
(l.map f).sum = (l.map g).sum :=
begin
rw list.map_congr h,
end
For the main theorem, there is a lot of unfolding of definitions. It's better to encapsulate those into some additional lemmas, since mathlib style is to try to avoid relying on definitions unless they're considered part of the interface (this isn't always clear). Two lemmas that seem useful are for popping terms off the front and back of the antidiagonal:
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
In these, I'm (somewhat) misusing a feature of simpa, which is that it basically tries refl at the end. (These lemmas should also probably find their way into mathlib, but I'm not too familiar with the list antidiagonal functions. Edit: mathlib#12028 and mathlib#12029)
With these, we can simplify the main proof. I flipped the equality because I imagine that the main use would be to take existing fibonacci numbers and rewrite them into this other form. I also changed n.succ to n + 1 since that tends to be the normal form for arithmetic expressions. By the way, it's common to open function, so uncurry doesn't need to be fully qualified.
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
Now that we've gone through everything, let's put it all together. We have three lemmas that arguably should be in mathlib already, and then your proof is pretty close to what you said in your outline:
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
```