-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
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))
⊢ (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 h : (if false = true then
      (HPow.hPow (β := ℕ) (fib 0, fib 1).2 2 + HPow.hPow (β := ℕ) (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),
        HPow.hPow (β := ℕ) (fib 0, fib 1).2 2 + HPow.hPow (β := ℕ) (fib 0, fib 1).1 2)) =
    (fib 0, fib 1) ∨
  (n = 0 → true = true)
Tactic: rw [fastFibAux, binaryRec_eq]