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.
```lean
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](https://leanprover-community.github.io/mathlib_docs/init/data/nat/lemmas.html#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 `simp`s](https://leanprover-community.github.io/extras/simp.html) 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."
```lean
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](https://leanprover-community.github.io/mathlib_docs/algebra/big_operators/multiset.html#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:
```lean
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:
```lean
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](https://github.com/leanprover-community/mathlib/pull/12028) and [mathlib#12029](https://github.com/leanprover-community/mathlib/pull/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.
```lean
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:
```lean
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](https://github.com/leanprover-community/mathlib/pull/12028), the theorem ends up being just this:

```lean
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.)