awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if f true true = true then
      bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + 1
    else bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2)) =
    if f true true = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
have pos : f true true = true →
  bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + 1 =
    2 * bitwise f m n + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
pos :
  f true true = true →
    bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + 1 =
      2 * bitwise f m n + 1
⊢ (if f true true = true then
      bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + 1
    else bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2)) =
    if f true true = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
have neg : ¬f true true = true →
  bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) = 2 * bitwise f m n
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : m = 0 → a = true
hbn : n = 0 → b = true
| bitwise f (bit a m) (bit b n)
have unfold : if bit a m = 0 then if f false true = true then bit b n else 0
else
  if bit b n = 0 then if f true false = true then bit a m else 0
  else
    have n' := bit a m / 2;
    have m' := bit b n / 2;
    let b₁ := bit a m % 2 = 1;
    let b₂ := bit b n % 2 = 1;
    have r := bitwise f n' m';
    if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r
Tactic: unfold bitwise
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : m = 0 → a = true
hbn : n = 0 → b = true
⊢ bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n)
have conv_lhs : (if bit a m = 0 then if f false true = true then bit b n else 0
  else
    if bit b n = 0 then if f true false = true then bit a m else 0
    else
      have n' := bit a m / 2;
      have m' := bit b n / 2;
      let b₁ := bit a m % 2 = 1;
      let b₂ := bit b n % 2 = 1;
      have r := bitwise f n' m';
      if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
  bit (f a b) (bitwise f m n)
Tactic: conv_lhs => unfold bitwise
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (hypothesis)
Goal:
f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : m = 0 → a = true
hbn : n = 0 → b = true
⊢ (if bit a m = 0 then if f false true = true then bit b n else 0
    else
      if bit b n = 0 then if f true false = true then bit a m else 0
      else
        have n' := bit a m / 2;
        have m' := bit b n / 2;
        let b₁ := bit a m % 2 = 1;
        let b₂ := bit b n % 2 = 1;
        have r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    bit (f a b) (bitwise f m n)
have ham₁ : bit a m ≠ 0
Tactic: rw [← bit_ne_zero_iff] at ham hbn
Cleared hypotheses: ham, hbn
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (hypothesis)
Goal:
f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : m = 0 → a = true
hbn : n = 0 → b = true
ham₁ : bit a m ≠ 0
⊢ (if bit a m = 0 then if f false true = true then bit b n else 0
    else
      if bit b n = 0 then if f true false = true then bit a m else 0
      else
        have n' := bit a m / 2;
        have m' := bit b n / 2;
        let b₁ := bit a m % 2 = 1;
        let b₂ := bit b n % 2 = 1;
        have r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    bit (f a b) (bitwise f m n)
have hbn₁ : bit b n ≠ 0
Tactic: rw [← bit_ne_zero_iff] at ham hbn
Cleared hypotheses: ham, hbn
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : bit a m ≠ 0
hbn : bit b n ≠ 0
⊢ (if bit a m = 0 then if f false true = true then bit b n else 0
    else
      if bit b n = 0 then if f true false = true then bit a m else 0
      else
        have n' := bit a m / 2;
        have m' := bit b n / 2;
        let b₁ := bit a m % 2 = 1;
        let b₂ := bit b n % 2 = 1;
        have r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    bit (f a b) (bitwise f m n)
have simp : (if f a b = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n) =
  bit (f a b) (bitwise f m n)
Tactic: simp only [ham, hbn, bit_mod_two_eq_one_iff, Bool.decide_coe, ← div2_val, div2_bit,
    ite_false]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : bit a m ≠ 0
hbn : bit b n ≠ 0
| bit (f a b) (bitwise f m n)
have simp : if f a b = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n
Tactic: simp only [bit, two_mul, Bool.cond_eq_ite]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : bit a m ≠ 0
hbn : bit b n ≠ 0
⊢ (if f a b = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n) =
    bit (f a b) (bitwise f m n)
have conv_rhs : (if f a b = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n) =
  bit (f a b) (bitwise f m n)
Tactic: conv_rhs => simp only [bit, two_mul, Bool.cond_eq_ite]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : bit a m ≠ 0
hbn : bit b n ≠ 0
conv_rhs :
  (if f a b = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n) =
    bit (f a b) (bitwise f m n)
⊢ (if f a b = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n) =
    bit (f a b) (bitwise f m n)
have conv_rhs₁ : (if f a b = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n) =
  if f a b = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n
Tactic: conv_rhs => simp only [bit, two_mul, Bool.cond_eq_ite]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
⊢ bitwise f = fun (n : ℕ) ↦
    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)
      n
have h : ∀ (x 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
Tactic: funext x y
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
xb : Bool
x : ℕ
hxb : x = 0 → xb = true
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 : ℕ
⊢ bitwise f (bit xb 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)
      (bit xb x) y
have h : ∀ (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 : ℕ),
  bitwise f (bit xb 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)
      (bit xb x) y
Tactic: rw [← bit_ne_zero_iff] at hxb
Cleared hypotheses: hxb, ih, y
-- 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
y : ℕ
⊢ bitwise f (bit xb 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)
      (bit xb x) y
have h : 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: simp_rw [binaryRec_of_ne_zero _ _ hxb, bodd_bit, div2_bit, eq_rec_constant]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (hypothesis)
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 : y = 0 → yb = true
h :
  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)
have hyb₁ : bit yb y ≠ 0
Tactic: rw [← bit_ne_zero_iff] at hyb
Cleared hypotheses: hyb, h
-- 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 :
  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)
have 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))
    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]
-- 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))
      ⋯
⊢ 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 (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))
    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]
-- 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
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
have 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
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]
Cleared hypotheses: y
-- 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
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
⊢ 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
have 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)
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]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
x 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
have h : ∀ (y : ℕ),
  bitwise f 0 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)
      0 y
Tactic: induction x using binaryRec' generalizing y with
  | zero => simp only [bitwise_zero_left, binaryRec_zero, Bool.cond_eq_ite]
  | bit xb x hxb ih =>
    rw [← bit_ne_zero_iff] at hxb
    simp_rw [binaryRec_of_ne_zero _ _ hxb, bodd_bit, div2_bit, eq_rec_constant]
    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]
Cleared hypotheses: x, y