n : ℕ
h1 : fib (n + 1) = ∑ p in Finset.Nat.antidiagonal n, choose p.fst p.snd
h2 : fib (succ n + 1) = ∑ p in Finset.Nat.antidiagonal (succ n), choose p.fst p.snd
⊢ ∑ p in Finset.Nat.antidiagonal n, choose p.fst p.snd +
      ∑ p in
        Finset.cons (n + 1, 0)
          (Finset.map (Function.Embedding.prodMap (Function.Embedding.refl ℕ) { toFun := succ, inj' := succ_injective })
            (Finset.Nat.antidiagonal n))
          (_ :
            ¬(n + 1, 0) ∈
                Finset.map
                  (Function.Embedding.prodMap (Function.Embedding.refl ℕ) { toFun := succ, inj' := succ_injective })
                  (Finset.Nat.antidiagonal n)),
        choose p.fst p.snd =
    ∑ p in
      Finset.cons (0, n + 2)
        (Finset.cons (n + 2, 0)
          (Finset.map
            (Function.Embedding.prodMap { toFun := succ, inj' := succ_injective }
              { toFun := succ, inj' := succ_injective })
            (Finset.Nat.antidiagonal n))
          (_ :
            ¬(n + 2, 0) ∈
                Finset.map
                  (Function.Embedding.prodMap { toFun := succ, inj' := succ_injective }
                    { toFun := succ, inj' := succ_injective })
                  (Finset.Nat.antidiagonal n)))
        (_ :
          ¬(0, n + 2) ∈
              Finset.cons (n + 2, 0)
                (Finset.map
                  (Function.Embedding.prodMap { toFun := succ, inj' := succ_injective }
                    { toFun := succ, inj' := succ_injective })
                  (Finset.Nat.antidiagonal n))
                (_ :
                  ¬(n + 2, 0) ∈
                      Finset.map
                        (Function.Embedding.prodMap { toFun := succ, inj' := succ_injective }
                          { toFun := succ, inj' := succ_injective })
                        (Finset.Nat.antidiagonal n))),
      choose p.fst p.snd
n : ℕ
h1 : fib (n + 1) = ∑ p in Finset.Nat.antidiagonal n, choose p.fst p.snd
h2 : fib (succ n + 1) = ∑ p in Finset.Nat.antidiagonal (succ n), choose p.fst p.snd
⊢ fib (succ (succ n) + 1) = ∑ p in Finset.Nat.antidiagonal (succ (succ n)), choose p.fst p.snd
rw [fib_add_two, h1, h2, Finset.Nat.antidiagonal_succ_succ', Finset.Nat.antidiagonal_succ']
no goals
n : ℕ
h1 : fib (n + 1) = ∑ p in Finset.Nat.antidiagonal n, choose p.fst p.snd
h2 : fib (succ n + 1) = ∑ p in Finset.Nat.antidiagonal (succ n), choose p.fst p.snd
⊢ ∑ p in Finset.Nat.antidiagonal n, choose p.fst p.snd +
      ∑ p in
        Finset.cons (n + 1, 0)
          (Finset.map (Function.Embedding.prodMap (Function.Embedding.refl ℕ) { toFun := succ, inj' := succ_injective })
            (Finset.Nat.antidiagonal n))
          (_ :
            ¬(n + 1, 0) ∈
                Finset.map
                  (Function.Embedding.prodMap (Function.Embedding.refl ℕ) { toFun := succ, inj' := succ_injective })
                  (Finset.Nat.antidiagonal n)),
        choose p.fst p.snd =
    ∑ p in
      Finset.cons (0, n + 2)
        (Finset.cons (n + 2, 0)
          (Finset.map
            (Function.Embedding.prodMap { toFun := succ, inj' := succ_injective }
              { toFun := succ, inj' := succ_injective })
            (Finset.Nat.antidiagonal n))
          (_ :
            ¬(n + 2, 0) ∈
                Finset.map
                  (Function.Embedding.prodMap { toFun := succ, inj' := succ_injective }
                    { toFun := succ, inj' := succ_injective })
                  (Finset.Nat.antidiagonal n)))
        (_ :
          ¬(0, n + 2) ∈
              Finset.cons (n + 2, 0)
                (Finset.map
                  (Function.Embedding.prodMap { toFun := succ, inj' := succ_injective }
                    { toFun := succ, inj' := succ_injective })
                  (Finset.Nat.antidiagonal n))
                (_ :
                  ¬(n + 2, 0) ∈
                      Finset.map
                        (Function.Embedding.prodMap { toFun := succ, inj' := succ_injective }
                          { toFun := succ, inj' := succ_injective })
                        (Finset.Nat.antidiagonal n))),
      choose p.fst p.snd
simp [choose_succ_succ, Finset.sum_add_distrib, add_left_comm]