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

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
```