[GOAL]
n : ℕ
⊢ fib (n + 2) = fib n + fib (n + 1)
[PROOFSTEP]
simp [fib, Function.iterate_succ_apply']
[GOAL]
n : ℕ
⊢ fib n ≤ fib (n + 1)
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ fib zero ≤ fib (zero + 1)
[PROOFSTEP]
simp [fib_add_two]
[GOAL]
case succ
n✝ : ℕ
⊢ fib (succ n✝) ≤ fib (succ n✝ + 1)
[PROOFSTEP]
simp [fib_add_two]
[GOAL]
n : ℕ
n_pos : 0 < n
⊢ 0 < fib 1
[PROOFSTEP]
decide
[GOAL]
n : ℕ
⊢ fib (n + 2) - fib (n + 1) = fib n
[PROOFSTEP]
rw [fib_add_two, add_tsub_cancel_right]
[GOAL]
n : ℕ
hn : 2 ≤ n
⊢ fib n < fib (n + 1)
[PROOFSTEP]
rcases exists_add_of_le hn with ⟨n, rfl⟩
[GOAL]
case intro
n : ℕ
hn : 2 ≤ 2 + n
⊢ fib (2 + n) < fib (2 + n + 1)
[PROOFSTEP]
rw [← tsub_pos_iff_lt, add_comm 2, fib_add_two_sub_fib_add_one]
[GOAL]
case intro
n : ℕ
hn : 2 ≤ 2 + n
⊢ 0 < fib (n + 1)
[PROOFSTEP]
apply fib_pos (succ_pos n)
[GOAL]
⊢ StrictMono fun n => fib (n + 2)
[PROOFSTEP]
refine' strictMono_nat_of_lt_succ fun n => _
[GOAL]
n : ℕ
⊢ fib (n + 2) < fib (n + 1 + 2)
[PROOFSTEP]
rw [add_right_comm]
[GOAL]
n : ℕ
⊢ fib (n + 2) < fib (n + 2 + 1)
[PROOFSTEP]
exact fib_lt_fib_succ (self_le_add_left _ _)
[GOAL]
n : ℕ
five_le_n : 5 ≤ n
⊢ n ≤ fib n
[PROOFSTEP]
induction' five_le_n with n five_le_n IH
[GOAL]
case refl
n : ℕ
⊢ 5 ≤ fib 5
[PROOFSTEP]
rfl
[GOAL]
case step
n✝ n : ℕ
five_le_n : Nat.le 5 n
IH : n ≤ fib n
⊢ succ n ≤ fib (succ n)
[PROOFSTEP]
rw [succ_le_iff]
[GOAL]
case step
n✝ n : ℕ
five_le_n : Nat.le 5 n
IH : n ≤ fib n
⊢ n < fib (succ n)
[PROOFSTEP]
calc
  n ≤ fib n := IH
  _ < fib (n + 1) := fib_lt_fib_succ (le_trans (by decide) five_le_n)
[GOAL]
n✝ n : ℕ
five_le_n : Nat.le 5 n
IH : n ≤ fib n
⊢ 2 ≤ 5
[PROOFSTEP]
decide
[GOAL]
n : ℕ
⊢ coprime (fib n) (fib (n + 1))
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
⊢ coprime (fib zero) (fib (zero + 1))
[PROOFSTEP]
simp
[GOAL]
case succ
n : ℕ
ih : coprime (fib n) (fib (n + 1))
⊢ coprime (fib (succ n)) (fib (succ n + 1))
[PROOFSTEP]
rw [fib_add_two]
[GOAL]
case succ
n : ℕ
ih : coprime (fib n) (fib (n + 1))
⊢ coprime (fib (succ n)) (fib n + fib (n + 1))
[PROOFSTEP]
simp only [coprime_add_self_right]
[GOAL]
case succ
n : ℕ
ih : coprime (fib n) (fib (n + 1))
⊢ coprime (fib (succ n)) (fib n)
[PROOFSTEP]
simp [coprime, ih.symm]
[GOAL]
m n : ℕ
⊢ fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)
[PROOFSTEP]
induction' n with n ih generalizing m
[GOAL]
case zero
m✝ m : ℕ
⊢ fib (m + zero + 1) = fib m * fib zero + fib (m + 1) * fib (zero + 1)
[PROOFSTEP]
simp
[GOAL]
case succ
m✝ n : ℕ
ih : ∀ (m : ℕ), fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)
m : ℕ
⊢ fib (m + succ n + 1) = fib m * fib (succ n) + fib (m + 1) * fib (succ n + 1)
[PROOFSTEP]
intros
[GOAL]
case succ
m✝ n : ℕ
ih : ∀ (m : ℕ), fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)
m : ℕ
⊢ fib (m + succ n + 1) = fib m * fib (succ n) + fib (m + 1) * fib (succ n + 1)
[PROOFSTEP]
specialize ih (m + 1)
[GOAL]
case succ
m✝ n m : ℕ
ih : fib (m + 1 + n + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)
⊢ fib (m + succ n + 1) = fib m * fib (succ n) + fib (m + 1) * fib (succ n + 1)
[PROOFSTEP]
rw [add_assoc m 1 n, add_comm 1 n] at ih 
[GOAL]
case succ
m✝ n m : ℕ
ih : fib (m + (n + 1) + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)
⊢ fib (m + succ n + 1) = fib m * fib (succ n) + fib (m + 1) * fib (succ n + 1)
[PROOFSTEP]
simp only [fib_add_two, ih]
[GOAL]
case succ
m✝ n m : ℕ
ih : fib (m + (n + 1) + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)
⊢ fib (m + 1) * fib n + (fib m + fib (m + 1)) * fib (n + 1) = fib m * fib (succ n) + fib (m + 1) * (fib n + fib (n + 1))
[PROOFSTEP]
ring
[GOAL]
n : ℕ
⊢ fib (2 * n) = fib n * (2 * fib (n + 1) - fib n)
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ fib (2 * zero) = fib zero * (2 * fib (zero + 1) - fib zero)
[PROOFSTEP]
simp
[GOAL]
case succ
n✝ : ℕ
⊢ fib (2 * succ n✝) = fib (succ n✝) * (2 * fib (succ n✝ + 1) - fib (succ n✝))
[PROOFSTEP]
rw [Nat.succ_eq_add_one, two_mul, ← add_assoc, fib_add, fib_add_two, two_mul]
[GOAL]
case succ
n✝ : ℕ
⊢ fib (n✝ + 1) * fib n✝ + (fib n✝ + fib (n✝ + 1)) * fib (n✝ + 1) =
    fib (n✝ + 1) * (fib n✝ + fib (n✝ + 1) + (fib n✝ + fib (n✝ + 1)) - fib (n✝ + 1))
[PROOFSTEP]
simp only [← add_assoc, add_tsub_cancel_right]
[GOAL]
case succ
n✝ : ℕ
⊢ fib (n✝ + 1) * fib n✝ + (fib n✝ + fib (n✝ + 1)) * fib (n✝ + 1) = fib (n✝ + 1) * (fib n✝ + fib (n✝ + 1) + fib n✝)
[PROOFSTEP]
ring
[GOAL]
n : ℕ
⊢ fib (2 * n + 1) = fib (n + 1) ^ 2 + fib n ^ 2
[PROOFSTEP]
rw [two_mul, fib_add]
[GOAL]
n : ℕ
⊢ fib n * fib n + fib (n + 1) * fib (n + 1) = fib (n + 1) ^ 2 + fib n ^ 2
[PROOFSTEP]
ring
[GOAL]
n : ℕ
⊢ fib (2 * n + 2) = fib (n + 1) * (2 * fib n + fib (n + 1))
[PROOFSTEP]
rw [fib_add_two, fib_two_mul, fib_two_mul_add_one]
  -- porting note: A bunch of issues similar to [this zulip thread](https://github.com/leanprover-community/mathlib4/pull/1576) with `zify`
[GOAL]
n : ℕ
⊢ fib n * (2 * fib (n + 1) - fib n) + (fib (n + 1) ^ 2 + fib n ^ 2) = fib (n + 1) * (2 * fib n + fib (n + 1))
[PROOFSTEP]
have : fib n ≤ 2 * fib (n + 1) := le_trans (fib_le_fib_succ) (mul_comm 2 _ ▸ le_mul_of_pos_right two_pos)
[GOAL]
n : ℕ
this : fib n ≤ 2 * fib (n + 1)
⊢ fib n * (2 * fib (n + 1) - fib n) + (fib (n + 1) ^ 2 + fib n ^ 2) = fib (n + 1) * (2 * fib n + fib (n + 1))
[PROOFSTEP]
zify [this]
[GOAL]
n : ℕ
this : fib n ≤ 2 * fib (n + 1)
⊢ ↑(fib n) * (2 * ↑(fib (n + 1)) - ↑(fib n)) + (↑(fib (n + 1)) ^ 2 + ↑(fib n) ^ 2) =
    ↑(fib (n + 1)) * (2 * ↑(fib n) + ↑(fib (n + 1)))
[PROOFSTEP]
ring
[GOAL]
n : ℕ
⊢ fib (bit0 n) = fib n * (2 * fib (n + 1) - fib n)
[PROOFSTEP]
rw [bit0_eq_two_mul, fib_two_mul]
[GOAL]
n : ℕ
⊢ fib (bit1 n) = fib (n + 1) ^ 2 + fib n ^ 2
[PROOFSTEP]
rw [Nat.bit1_eq_succ_bit0, bit0_eq_two_mul, fib_two_mul_add_one]
[GOAL]
n : ℕ
⊢ fib (bit1 n + 1) = fib (n + 1) * (2 * fib n + fib (n + 1))
[PROOFSTEP]
rw [Nat.bit1_eq_succ_bit0, bit0_eq_two_mul, fib_two_mul_add_two]
[GOAL]
n : ℕ
⊢ fastFibAux (bit false n) =
    let p := fastFibAux n;
    (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2)
[PROOFSTEP]
rw [fastFibAux, binaryRec_eq]
[GOAL]
n : ℕ
⊢ (if false = true then
      ((binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).snd ^
            2 +
          (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).fst ^
            2,
        (binaryRec (fib 0, fib 1)
              (fun b x p =>
                if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
              n).snd *
          (2 *
              (binaryRec (fib 0, fib 1)
                  (fun b x p =>
                    if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                    else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                  n).fst +
            (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).snd))
    else
      ((binaryRec (fib 0, fib 1)
              (fun b x p =>
                if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
              n).fst *
          (2 *
              (binaryRec (fib 0, fib 1)
                  (fun b x p =>
                    if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                    else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                  n).snd -
            (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).fst),
        (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).snd ^
            2 +
          (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).fst ^
            2)) =
    let p :=
      binaryRec (fib 0, fib 1)
        (fun b x p =>
          if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
          else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
        n;
    (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2)
[PROOFSTEP]
rfl
[GOAL]
case h
n : ℕ
⊢ (if false = true then
      ((fib 0, fib 1).snd ^ 2 + (fib 0, fib 1).fst ^ 2,
        (fib 0, fib 1).snd * (2 * (fib 0, fib 1).fst + (fib 0, fib 1).snd))
    else
      ((fib 0, fib 1).fst * (2 * (fib 0, fib 1).snd - (fib 0, fib 1).fst),
        (fib 0, fib 1).snd ^ 2 + (fib 0, fib 1).fst ^ 2)) =
    (fib 0, fib 1)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ fastFibAux (bit true n) =
    let p := fastFibAux n;
    (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
[PROOFSTEP]
rw [fastFibAux, binaryRec_eq]
[GOAL]
n : ℕ
⊢ (if true = true then
      ((binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).snd ^
            2 +
          (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).fst ^
            2,
        (binaryRec (fib 0, fib 1)
              (fun b x p =>
                if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
              n).snd *
          (2 *
              (binaryRec (fib 0, fib 1)
                  (fun b x p =>
                    if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                    else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                  n).fst +
            (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).snd))
    else
      ((binaryRec (fib 0, fib 1)
              (fun b x p =>
                if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
              n).fst *
          (2 *
              (binaryRec (fib 0, fib 1)
                  (fun b x p =>
                    if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                    else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                  n).snd -
            (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).fst),
        (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).snd ^
            2 +
          (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).fst ^
            2)) =
    let p :=
      binaryRec (fib 0, fib 1)
        (fun b x p =>
          if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
          else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
        n;
    (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
[PROOFSTEP]
rfl
[GOAL]
case h
n : ℕ
⊢ (if false = true then
      ((fib 0, fib 1).snd ^ 2 + (fib 0, fib 1).fst ^ 2,
        (fib 0, fib 1).snd * (2 * (fib 0, fib 1).fst + (fib 0, fib 1).snd))
    else
      ((fib 0, fib 1).fst * (2 * (fib 0, fib 1).snd - (fib 0, fib 1).fst),
        (fib 0, fib 1).snd ^ 2 + (fib 0, fib 1).fst ^ 2)) =
    (fib 0, fib 1)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ fastFibAux n = (fib n, fib (n + 1))
[PROOFSTEP]
apply Nat.binaryRec _ (fun b n' ih => _) n
[GOAL]
n : ℕ
⊢ fastFibAux 0 = (fib 0, fib (0 + 1))
[PROOFSTEP]
simp [fastFibAux]
[GOAL]
n : ℕ
⊢ ∀ (b : Bool) (n' : ℕ),
    fastFibAux n' = (fib n', fib (n' + 1)) → fastFibAux (bit b n') = (fib (bit b n'), fib (bit b n' + 1))
[PROOFSTEP]
intro b
[GOAL]
n : ℕ
b : Bool
⊢ ∀ (n' : ℕ), fastFibAux n' = (fib n', fib (n' + 1)) → fastFibAux (bit b n') = (fib (bit b n'), fib (bit b n' + 1))
[PROOFSTEP]
intro n'
[GOAL]
n : ℕ
b : Bool
n' : ℕ
⊢ fastFibAux n' = (fib n', fib (n' + 1)) → fastFibAux (bit b n') = (fib (bit b n'), fib (bit b n' + 1))
[PROOFSTEP]
intro ih
[GOAL]
n : ℕ
b : Bool
n' : ℕ
ih : fastFibAux n' = (fib n', fib (n' + 1))
⊢ fastFibAux (bit b n') = (fib (bit b n'), fib (bit b n' + 1))
[PROOFSTEP]
cases b
[GOAL]
case false
n n' : ℕ
ih : fastFibAux n' = (fib n', fib (n' + 1))
⊢ fastFibAux (bit false n') = (fib (bit false n'), fib (bit false n' + 1))
[PROOFSTEP]
simp only [fast_fib_aux_bit_ff, fast_fib_aux_bit_tt, congr_arg Prod.fst ih, congr_arg Prod.snd ih, Prod.mk.inj_iff]
[GOAL]
case true
n n' : ℕ
ih : fastFibAux n' = (fib n', fib (n' + 1))
⊢ fastFibAux (bit true n') = (fib (bit true n'), fib (bit true n' + 1))
[PROOFSTEP]
simp only [fast_fib_aux_bit_ff, fast_fib_aux_bit_tt, congr_arg Prod.fst ih, congr_arg Prod.snd ih, Prod.mk.inj_iff]
[GOAL]
case false
n n' : ℕ
ih : fastFibAux n' = (fib n', fib (n' + 1))
⊢ fib n' * (2 * fib (n' + 1) - fib n') = fib (bit false n') ∧ fib (n' + 1) ^ 2 + fib n' ^ 2 = fib (bit false n' + 1)
[PROOFSTEP]
simp [bit, fib_bit0, fib_bit1, fib_bit0_succ, fib_bit1_succ]
[GOAL]
case true
n n' : ℕ
ih : fastFibAux n' = (fib n', fib (n' + 1))
⊢ fib (n' + 1) ^ 2 + fib n' ^ 2 = fib (bit true n') ∧ fib (n' + 1) * (2 * fib n' + fib (n' + 1)) = fib (bit true n' + 1)
[PROOFSTEP]
simp [bit, fib_bit0, fib_bit1, fib_bit0_succ, fib_bit1_succ]
[GOAL]
n : ℕ
⊢ fastFib n = fib n
[PROOFSTEP]
rw [fastFib, fast_fib_aux_eq]
[GOAL]
m n : ℕ
⊢ gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)
[PROOFSTEP]
cases' Nat.eq_zero_or_pos n with h h
[GOAL]
case inl
m n : ℕ
h : n = 0
⊢ gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)
[PROOFSTEP]
rw [h]
[GOAL]
case inl
m n : ℕ
h : n = 0
⊢ gcd (fib m) (fib (0 + m)) = gcd (fib m) (fib 0)
[PROOFSTEP]
simp
[GOAL]
case inr
m n : ℕ
h : n > 0
⊢ gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)
[PROOFSTEP]
replace h := Nat.succ_pred_eq_of_pos h
[GOAL]
case inr
m n : ℕ
h : succ (pred n) = n
⊢ gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)
[PROOFSTEP]
rw [← h, succ_eq_add_one]
[GOAL]
case inr
m n : ℕ
h : succ (pred n) = n
⊢ gcd (fib m) (fib (pred n + 1 + m)) = gcd (fib m) (fib (pred n + 1))
[PROOFSTEP]
calc
  gcd (fib m) (fib (n.pred + 1 + m)) = gcd (fib m) (fib n.pred * fib m + fib (n.pred + 1) * fib (m + 1)) :=
    by
    rw [← fib_add n.pred _]
    ring_nf
  _ = gcd (fib m) (fib (n.pred + 1) * fib (m + 1)) := by rw [add_comm, gcd_add_mul_right_right (fib m) _ (fib n.pred)]
  _ = gcd (fib m) (fib (n.pred + 1)) :=
    coprime.gcd_mul_right_cancel_right (fib (n.pred + 1)) (coprime.symm (fib_coprime_fib_succ m))
[GOAL]
m n : ℕ
h : succ (pred n) = n
⊢ gcd (fib m) (fib (pred n + 1 + m)) = gcd (fib m) (fib (pred n) * fib m + fib (pred n + 1) * fib (m + 1))
[PROOFSTEP]
rw [← fib_add n.pred _]
[GOAL]
m n : ℕ
h : succ (pred n) = n
⊢ gcd (fib m) (fib (pred n + 1 + m)) = gcd (fib m) (fib (pred n + m + 1))
[PROOFSTEP]
ring_nf
[GOAL]
m n : ℕ
h : succ (pred n) = n
⊢ gcd (fib m) (fib (pred n) * fib m + fib (pred n + 1) * fib (m + 1)) = gcd (fib m) (fib (pred n + 1) * fib (m + 1))
[PROOFSTEP]
rw [add_comm, gcd_add_mul_right_right (fib m) _ (fib n.pred)]
[GOAL]
m n : ℕ
⊢ gcd (fib m) (fib (n + 0 * m)) = gcd (fib m) (fib n)
[PROOFSTEP]
simp
[GOAL]
m n k : ℕ
⊢ gcd (fib m) (fib (n + (k + 1) * m)) = gcd (fib m) (fib n)
[PROOFSTEP]
rw [← gcd_fib_add_mul_self m n k, add_mul, ← add_assoc, one_mul, gcd_fib_add_self _ _]
[GOAL]
m n : ℕ
⊢ fib (gcd m n) = gcd (fib m) (fib n)
[PROOFSTEP]
induction m, n using Nat.gcd.induction with
| H0 => simp
| H1 m n _ h' =>
  rw [← gcd_rec m n] at h' 
  conv_rhs => rw [← mod_add_div' n m]
  rwa [gcd_fib_add_mul_self m (n % m) (n / m), gcd_comm (fib m) _]
[GOAL]
m n : ℕ
⊢ fib (gcd m n) = gcd (fib m) (fib n)
[PROOFSTEP]
induction m, n using Nat.gcd.induction with
| H0 => simp
| H1 m n _ h' =>
  rw [← gcd_rec m n] at h' 
  conv_rhs => rw [← mod_add_div' n m]
  rwa [gcd_fib_add_mul_self m (n % m) (n / m), gcd_comm (fib m) _]
[GOAL]
case H0
n✝ : ℕ
⊢ fib (gcd 0 n✝) = gcd (fib 0) (fib n✝)
[PROOFSTEP]

| H0 => simp
[GOAL]
case H0
n✝ : ℕ
⊢ fib (gcd 0 n✝) = gcd (fib 0) (fib n✝)
[PROOFSTEP]
simp
[GOAL]
case H1
m n : ℕ
a✝ : 0 < m
h' : fib (gcd (n % m) m) = gcd (fib (n % m)) (fib m)
⊢ fib (gcd m n) = gcd (fib m) (fib n)
[PROOFSTEP]

| H1 m n _ h' =>
  rw [← gcd_rec m n] at h' 
  conv_rhs => rw [← mod_add_div' n m]
  rwa [gcd_fib_add_mul_self m (n % m) (n / m), gcd_comm (fib m) _]
[GOAL]
case H1
m n : ℕ
a✝ : 0 < m
h' : fib (gcd (n % m) m) = gcd (fib (n % m)) (fib m)
⊢ fib (gcd m n) = gcd (fib m) (fib n)
[PROOFSTEP]
rw [← gcd_rec m n] at h' 
[GOAL]
case H1
m n : ℕ
a✝ : 0 < m
h' : fib (gcd m n) = gcd (fib (n % m)) (fib m)
⊢ fib (gcd m n) = gcd (fib m) (fib n)
[PROOFSTEP]
conv_rhs => rw [← mod_add_div' n m]
[GOAL]
m n : ℕ
a✝ : 0 < m
h' : fib (gcd m n) = gcd (fib (n % m)) (fib m)
| gcd (fib m) (fib n)
[PROOFSTEP]
rw [← mod_add_div' n m]
[GOAL]
m n : ℕ
a✝ : 0 < m
h' : fib (gcd m n) = gcd (fib (n % m)) (fib m)
| gcd (fib m) (fib n)
[PROOFSTEP]
rw [← mod_add_div' n m]
[GOAL]
m n : ℕ
a✝ : 0 < m
h' : fib (gcd m n) = gcd (fib (n % m)) (fib m)
| gcd (fib m) (fib n)
[PROOFSTEP]
rw [← mod_add_div' n m]
[GOAL]
case H1
m n : ℕ
a✝ : 0 < m
h' : fib (gcd m n) = gcd (fib (n % m)) (fib m)
⊢ fib (gcd m n) = gcd (fib m) (fib (n % m + n / m * m))
[PROOFSTEP]
rwa [gcd_fib_add_mul_self m (n % m) (n / m), gcd_comm (fib m) _]
[GOAL]
m n : ℕ
h : m ∣ n
⊢ fib m ∣ fib n
[PROOFSTEP]
rwa [gcd_eq_left_iff_dvd, ← fib_gcd, gcd_eq_left_iff_dvd.mp]
[GOAL]
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
[PROOFSTEP]
rw [fib_add_two, h1, h2, Finset.Nat.antidiagonal_succ_succ', Finset.Nat.antidiagonal_succ']
[GOAL]
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
[PROOFSTEP]
simp [choose_succ_succ, Finset.sum_add_distrib, add_left_comm]
[GOAL]
n : ℕ
⊢ fib (n + 1) = ∑ k in Finset.range n, fib k + 1
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
⊢ fib (zero + 1) = ∑ k in Finset.range zero, fib k + 1
[PROOFSTEP]
simp
[GOAL]
case succ
n : ℕ
ih : fib (n + 1) = ∑ k in Finset.range n, fib k + 1
⊢ fib (succ n + 1) = ∑ k in Finset.range (succ n), fib k + 1
[PROOFSTEP]
calc
  fib (n + 2) = fib n + fib (n + 1) := fib_add_two
  _ = (fib n + ∑ k in Finset.range n, fib k) + 1 := by rw [ih, add_assoc]
  _ = (∑ k in Finset.range (n + 1), fib k) + 1 := by simp [Finset.range_add_one]
[GOAL]
n : ℕ
ih : fib (n + 1) = ∑ k in Finset.range n, fib k + 1
⊢ fib n + fib (n + 1) = fib n + ∑ k in Finset.range n, fib k + 1
[PROOFSTEP]
rw [ih, add_assoc]
[GOAL]
n : ℕ
ih : fib (n + 1) = ∑ k in Finset.range n, fib k + 1
⊢ fib n + ∑ k in Finset.range n, fib k + 1 = ∑ k in Finset.range (n + 1), fib k + 1
[PROOFSTEP]
simp [Finset.range_add_one]
