-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
⊢ (bit true n).fastFibAux =
    let p := n.fastFibAux;
    (HPow.hPow (β := ℕ) p.2 2 + HPow.hPow (β := ℕ) p.1 2, p.2 * (2 * p.1 + p.2))
have rw : (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: rw [fastFibAux, binaryRec_eq]