-- Mathlib/Data/Nat/Bitwise.lean
lemma bitwise_eq_binaryRec (f : Bool → Bool → Bool) :
    bitwise f =
    binaryRec (fun n => cond (f false true) n 0) fun a m Ia =>
      binaryRec (cond (f true false) (bit a m) 0) fun b n _ => bit (f a b) (Ia n)

Proof state:
f : Bool → Bool → Bool
⊢ bitwise f = fun n =>
    binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
      (fun a m Ia n => binaryRec (bif f true false then bit a m else 0) (fun b n x => bit (f a b) (Ia n)) n) n

Tactic:
funext x y

Result:
case h.h
f : Bool → Bool → Bool
x y : ℕ
⊢ bitwise f x y =
    binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
      (fun a m Ia n => binaryRec (bif f true false then bit a m else 0) (fun b n x => bit (f a b) (Ia n)) n) x y

Proof state:
case h.h.f
f : Bool → Bool → Bool
xb : Bool
x : ℕ
hxb : bit xb x ≠ 0
ih :
  ∀ (y : ℕ),
    bitwise f x y =
      binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
        (fun a m Ia n => binaryRec (bif f true false then bit a m else 0) (fun b n x => bit (f a b) (Ia n)) n) x y
y : ℕ
⊢ bitwise f (bit xb x) y =
    binaryRec (bif f true false then bit xb x else 0)
      (fun b n x_1 =>
        bit (f xb b)
          (binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
            (fun a m Ia n => binaryRec (bif f true false then bit a m else 0) (fun b n x => bit (f a b) (Ia n)) n) x n))
      y

Tactic:
induction y using binaryRec' with
| z => simp only [bitwise_zero_right, binaryRec_zero, Bool.cond_eq_ite]
| f 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_val,
    div2_bit, eq_rec_constant, ih]

Result:
no goals

Proof state:
case h.h.f.z
f : Bool → Bool → Bool
xb : Bool
x : ℕ
hxb : bit xb x ≠ 0
ih :
  ∀ (y : ℕ),
    bitwise f x y =
      binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
        (fun a m Ia n => binaryRec (bif f true false then bit a m else 0) (fun b n x => bit (f a b) (Ia n)) n) x y
⊢ bitwise f (bit xb x) 0 =
    binaryRec (bif f true false then bit xb x else 0)
      (fun b n x_1 =>
        bit (f xb b)
          (binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
            (fun a m Ia n => binaryRec (bif f true false then bit a m else 0) (fun b n x => bit (f a b) (Ia n)) n) x n))
      0

Tactic:
simp only [bitwise_zero_right, binaryRec_zero, Bool.cond_eq_ite]

Result:
no goals

Proof state:
case h.h.z
f : Bool → Bool → Bool
y : ℕ
⊢ bitwise f 0 y =
    binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
      (fun a m Ia n => binaryRec (bif f true false then bit a m else 0) (fun b n x => bit (f a b) (Ia n)) n) 0 y

Tactic:
simp only [bitwise_zero_left, binaryRec_zero, Bool.cond_eq_ite]

Result:
no goals

Proof state:
case h.h.f.f
f : Bool → Bool → Bool
xb : Bool
x : ℕ
hxb : bit xb x ≠ 0
ih :
  ∀ (y : ℕ),
    bitwise f x y =
      binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
        (fun a m Ia n => binaryRec (bif f true false then bit a m else 0) (fun b n x => bit (f a b) (Ia n)) n) x y
yb : Bool
y : ℕ
hyb : bit yb y ≠ 0
a✝ :
  bitwise f (bit xb x) y =
    binaryRec (bif f true false then bit xb x else 0)
      (fun b n x_1 =>
        bit (f xb b)
          (binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
            (fun a m Ia n => binaryRec (bif f true false then bit a m else 0) (fun b n x => bit (f a b) (Ia n)) n) x n))
      y
⊢ bitwise f (bit xb x) (bit yb y) =
    binaryRec (bif f true false then bit xb x else 0)
      (fun b n x_1 =>
        bit (f xb b)
          (binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
            (fun a m Ia n => binaryRec (bif f true false then bit a m else 0) (fun b n x => bit (f a b) (Ia n)) n) x n))
      (bit yb y)

Tactic:
simp_rw [binaryRec_of_ne_zero _ _ hyb, bitwise_of_ne_zero hxb hyb, bodd_bit, ← div2_val,
  div2_bit, eq_rec_constant, ih]

Result:
no goals

Proof state:
case h.h
f : Bool → Bool → Bool
x y : ℕ
⊢ bitwise f x y =
    binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
      (fun a m Ia n => binaryRec (bif f true false then bit a m else 0) (fun b n x => bit (f a b) (Ia n)) n) x y

Tactic:
induction x using binaryRec' generalizing y with
| z => simp only [bitwise_zero_left, binaryRec_zero, Bool.cond_eq_ite]
| f 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
  | z => simp only [bitwise_zero_right, binaryRec_zero, Bool.cond_eq_ite]
  | f 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_val,
      div2_bit, eq_rec_constant, ih]

Result:
no goals

Proof state:
case h.h.f
f : Bool → Bool → Bool
xb : Bool
x : ℕ
hxb : x = 0 → xb = true
ih :
  ∀ (y : ℕ),
    bitwise f x y =
      binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
        (fun a m Ia n => binaryRec (bif f true false then bit a m else 0) (fun b n x => bit (f a b) (Ia n)) n) x y
y : ℕ
⊢ bitwise f (bit xb x) y =
    binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
      (fun a m Ia n => binaryRec (bif f true false then bit a m else 0) (fun b n x => bit (f a b) (Ia n)) n) (bit xb x)
      y

Tactic:
rw [← bit_ne_zero_iff] at hxb

Result:
case h.h.f
f : Bool → Bool → Bool
xb : Bool
x : ℕ
hxb : bit xb x ≠ 0
ih :
  ∀ (y : ℕ),
    bitwise f x y =
      binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
        (fun a m Ia n => binaryRec (bif f true false then bit a m else 0) (fun b n x => bit (f a b) (Ia n)) n) x y
y : ℕ
⊢ bitwise f (bit xb x) y =
    binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
      (fun a m Ia n => binaryRec (bif f true false then bit a m else 0) (fun b n x => bit (f a b) (Ia n)) n) (bit xb x)
      y

Proof state:
case h.h.f
f : Bool → Bool → Bool
xb : Bool
x : ℕ
hxb : bit xb x ≠ 0
ih :
  ∀ (y : ℕ),
    bitwise f x y =
      binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
        (fun a m Ia n => binaryRec (bif f true false then bit a m else 0) (fun b n x => bit (f a b) (Ia n)) n) x y
y : ℕ
⊢ bitwise f (bit xb x) y =
    binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
      (fun a m Ia n => binaryRec (bif f true false then bit a m else 0) (fun b n x => bit (f a b) (Ia n)) n) (bit xb x)
      y

Tactic:
simp_rw [binaryRec_of_ne_zero _ _ hxb, bodd_bit, div2_bit, eq_rec_constant]

Result:
case h.h.f
f : Bool → Bool → Bool
xb : Bool
x : ℕ
hxb : bit xb x ≠ 0
ih :
  ∀ (y : ℕ),
    bitwise f x y =
      binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
        (fun a m Ia n => binaryRec (bif f true false then bit a m else 0) (fun b n x => bit (f a b) (Ia n)) n) x y
y : ℕ
⊢ bitwise f (bit xb x) y =
    binaryRec (bif f true false then bit xb x else 0)
      (fun b n x_1 =>
        bit (f xb b)
          (binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
            (fun a m Ia n => binaryRec (bif f true false then bit a m else 0) (fun b n x => bit (f a b) (Ia n)) n) x n))
      y