-- Mathlib/Data/Nat/Fib/Basic.lean
theorem fast_fib_aux_bit_ff (n : ℕ) :
    fastFibAux (bit false n) =
      let p := fastFibAux n
      (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)

Proof state:
n : ℕ
⊢ (if false = true then
      ((binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).2 ^
            2 +
          (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).1 ^
            2,
        (binaryRec (fib 0, fib 1)
              (fun b x p =>
                if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
              n).2 *
          (2 *
              (binaryRec (fib 0, fib 1)
                  (fun b x p =>
                    if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                    else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                  n).1 +
            (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).2))
    else
      ((binaryRec (fib 0, fib 1)
              (fun b x p =>
                if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
              n).1 *
          (2 *
              (binaryRec (fib 0, fib 1)
                  (fun b x p =>
                    if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                    else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                  n).2 -
            (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).1),
        (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).2 ^
            2 +
          (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).1 ^
            2)) =
    let p := n.fastFibAux;
    (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
⊢ (bit false n).fastFibAux =
    let p := n.fastFibAux;
    (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)

Tactic:
rw [fastFibAux, binaryRec_eq]

Result:
n : ℕ
⊢ (if false = true then
      ((binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).2 ^
            2 +
          (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).1 ^
            2,
        (binaryRec (fib 0, fib 1)
              (fun b x p =>
                if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
              n).2 *
          (2 *
              (binaryRec (fib 0, fib 1)
                  (fun b x p =>
                    if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                    else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                  n).1 +
            (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).2))
    else
      ((binaryRec (fib 0, fib 1)
              (fun b x p =>
                if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
              n).1 *
          (2 *
              (binaryRec (fib 0, fib 1)
                  (fun b x p =>
                    if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                    else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                  n).2 -
            (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).1),
        (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).2 ^
            2 +
          (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).1 ^
            2)) =
    let p := n.fastFibAux;
    (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)

case h
n : ℕ
⊢ (if false = true then
        ((fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2, (fib 0, fib 1).2 * (2 * (fib 0, fib 1).1 + (fib 0, fib 1).2))
      else
        ((fib 0, fib 1).1 * (2 * (fib 0, fib 1).2 - (fib 0, fib 1).1), (fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2)) =
      (fib 0, fib 1) ∨
    (n = 0 → false = true)

Proof state:
case h
n : ℕ
⊢ (if false = true then
        ((fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2, (fib 0, fib 1).2 * (2 * (fib 0, fib 1).1 + (fib 0, fib 1).2))
      else
        ((fib 0, fib 1).1 * (2 * (fib 0, fib 1).2 - (fib 0, fib 1).1), (fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2)) =
      (fib 0, fib 1) ∨
    (n = 0 → false = true)

Tactic:
simp

Result:
no goals