-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
xb : Bool
x : ℕ
hxb : bit xb x ≠ 0
ih :
  ∀ (y : ℕ),
    bitwise f x y =
      binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
        (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
          binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
            (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
        x y
yb : Bool
y : ℕ
hyb : bit yb y ≠ 0
h_1 :
  bitwise f (bit xb x) y =
    binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit xb x else 0)
      (fun (b : Bool) (n x_1 : ℕ) ↦
        bit (f xb b)
          (binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
            (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
              binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
                (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
            x n))
      y
h :
  bitwise f (bit xb x) (bit yb y) =
    Eq.rec (motive := fun (x : ℕ) (h : bit (bit yb y).bodd (bit yb y).div2 = x) ↦ ℕ)
      (bit (f xb (bit yb y).bodd)
        (binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
          (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
            binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
              (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
          x (bit yb y).div2))
      ⋯
h₁ :
  bit (f (bit xb x).bodd (bit yb y).bodd) (bitwise f (bit xb x / 2) (bit yb y / 2)) =
    Eq.rec (motive := fun (x : ℕ) (h : bit (bit yb y).bodd (bit yb y).div2 = x) ↦ ℕ)
      (bit (f xb (bit yb y).bodd)
        (binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
          (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
            binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
              (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
          x (bit yb y).div2))
      ⋯
⊢ bitwise f (bit xb x) (bit yb y) =
    binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit xb x else 0)
      (fun (b : Bool) (n x_1 : ℕ) ↦
        bit (f xb b)
          (binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
            (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
              binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
                (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
            x n))
      (bit yb y)
have h₂ : bit (f xb yb) (bitwise f (bit xb x / 2) (bit yb y / 2)) =
  Eq.rec (motive := fun (x : ℕ) (h : bit (bit yb y).bodd (bit yb y).div2 = x) ↦ ℕ)
    (bit (f xb yb)
      (binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
        (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
          binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
            (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
        x (bit yb y).div2))
    sorry
Tactic: simp_rw [binaryRec_of_ne_zero _ _ hyb, bitwise_of_ne_zero hxb hyb, bodd_bit, div2_bit,
        bit_div_two, eq_rec_constant, ih]