-- Module: Mathlib.Data.Nat.Bitwise
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
y : ℕ
h :
  bitwise f (bit xb x) 0 =
    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))
      0
h₁ :
  ∀ (yb : Bool) (y : ℕ) (hyb : y = 0 → yb = true),
    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 →
      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)
⊢ 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

Tactic:
induction y using binaryRec' with
    | zero => simp only [bitwise_zero_right, binaryRec_zero, Bool.cond_eq_ite]
    | bit yb y hyb =>
      rw [← bit_ne_zero_iff] at hyb
      simp_rw [binaryRec_of_ne_zero _ _ hyb, bitwise_of_ne_zero hxb hyb, bodd_bit, div2_bit,
        bit_div_two, eq_rec_constant, ih]

Premises used: Nat.bit, Nat.bodd_bit, Nat.div2_bit, Nat.bit_div_two, Nat.binaryRec_zero, Nat.zero, eq_rec_constant, Nat.bitwise_zero_right, Nat.bit_ne_zero_iff, Bool.cond_eq_ite