-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
⊢ (if true = true then
      (HPow.hPow (α := ℕ) (β := ℕ)
            (binaryRec (motive := fun (x : ℕ) ↦ ℕ × ℕ) (fib 0, fib 1)
                (fun (b : Bool) (x : ℕ) (p : ℕ × ℕ) ↦
                  if b = true then (HPow.hPow (β := ℕ) p.2 2 + HPow.hPow (β := ℕ) p.1 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), HPow.hPow (β := ℕ) p.2 2 + HPow.hPow (β := ℕ) p.1 2))
                n).2
            2 +
          HPow.hPow (α := ℕ) (β := ℕ)
            (binaryRec (motive := fun (x : ℕ) ↦ ℕ × ℕ) (fib 0, fib 1)
                (fun (b : Bool) (x : ℕ) (p : ℕ × ℕ) ↦
                  if b = true then (HPow.hPow (β := ℕ) p.2 2 + HPow.hPow (β := ℕ) p.1 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), HPow.hPow (β := ℕ) p.2 2 + HPow.hPow (β := ℕ) p.1 2))
                n).1
            2,
        (binaryRec (motive := fun (x : ℕ) ↦ ℕ × ℕ) (fib 0, fib 1)
              (fun (b : Bool) (x : ℕ) (p : ℕ × ℕ) ↦
                if b = true then (HPow.hPow (β := ℕ) p.2 2 + HPow.hPow (β := ℕ) p.1 2, p.2 * (2 * p.1 + p.2))
                else (p.1 * (2 * p.2 - p.1), HPow.hPow (β := ℕ) p.2 2 + HPow.hPow (β := ℕ) p.1 2))
              n).2 *
          (HMul.hMul (α := ℕ) 2
              (binaryRec (motive := fun (x : ℕ) ↦ ℕ × ℕ) (fib 0, fib 1)
                  (fun (b : Bool) (x : ℕ) (p : ℕ × ℕ) ↦
                    if b = true then (HPow.hPow (β := ℕ) p.2 2 + HPow.hPow (β := ℕ) p.1 2, p.2 * (2 * p.1 + p.2))
                    else (p.1 * (2 * p.2 - p.1), HPow.hPow (β := ℕ) p.2 2 + HPow.hPow (β := ℕ) p.1 2))
                  n).1 +
            (binaryRec (motive := fun (x : ℕ) ↦ ℕ × ℕ) (fib 0, fib 1)
                (fun (b : Bool) (x : ℕ) (p : ℕ × ℕ) ↦
                  if b = true then (HPow.hPow (β := ℕ) p.2 2 + HPow.hPow (β := ℕ) p.1 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), HPow.hPow (β := ℕ) p.2 2 + HPow.hPow (β := ℕ) p.1 2))
                n).2))
    else
      ((binaryRec (motive := fun (x : ℕ) ↦ ℕ × ℕ) (fib 0, fib 1)
              (fun (b : Bool) (x : ℕ) (p : ℕ × ℕ) ↦
                if b = true then (HPow.hPow (β := ℕ) p.2 2 + HPow.hPow (β := ℕ) p.1 2, p.2 * (2 * p.1 + p.2))
                else (p.1 * (2 * p.2 - p.1), HPow.hPow (β := ℕ) p.2 2 + HPow.hPow (β := ℕ) p.1 2))
              n).1 *
          (HMul.hMul (α := ℕ) 2
              (binaryRec (motive := fun (x : ℕ) ↦ ℕ × ℕ) (fib 0, fib 1)
                  (fun (b : Bool) (x : ℕ) (p : ℕ × ℕ) ↦
                    if b = true then (HPow.hPow (β := ℕ) p.2 2 + HPow.hPow (β := ℕ) p.1 2, p.2 * (2 * p.1 + p.2))
                    else (p.1 * (2 * p.2 - p.1), HPow.hPow (β := ℕ) p.2 2 + HPow.hPow (β := ℕ) p.1 2))
                  n).2 -
            (binaryRec (motive := fun (x : ℕ) ↦ ℕ × ℕ) (fib 0, fib 1)
                (fun (b : Bool) (x : ℕ) (p : ℕ × ℕ) ↦
                  if b = true then (HPow.hPow (β := ℕ) p.2 2 + HPow.hPow (β := ℕ) p.1 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), HPow.hPow (β := ℕ) p.2 2 + HPow.hPow (β := ℕ) p.1 2))
                n).1),
        HPow.hPow (α := ℕ) (β := ℕ)
            (binaryRec (motive := fun (x : ℕ) ↦ ℕ × ℕ) (fib 0, fib 1)
                (fun (b : Bool) (x : ℕ) (p : ℕ × ℕ) ↦
                  if b = true then (HPow.hPow (β := ℕ) p.2 2 + HPow.hPow (β := ℕ) p.1 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), HPow.hPow (β := ℕ) p.2 2 + HPow.hPow (β := ℕ) p.1 2))
                n).2
            2 +
          HPow.hPow (α := ℕ) (β := ℕ)
            (binaryRec (motive := fun (x : ℕ) ↦ ℕ × ℕ) (fib 0, fib 1)
                (fun (b : Bool) (x : ℕ) (p : ℕ × ℕ) ↦
                  if b = true then (HPow.hPow (β := ℕ) p.2 2 + HPow.hPow (β := ℕ) p.1 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), HPow.hPow (β := ℕ) p.2 2 + HPow.hPow (β := ℕ) p.1 2))
                n).1
            2)) =
    let p := n.fastFibAux;
    (HPow.hPow (β := ℕ) p.2 2 + HPow.hPow (β := ℕ) p.1 2, p.2 * (2 * p.1 + p.2))

Tactic:
rfl