f : Bool → Bool → Bool
h : f false false = false
m : ℕ
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif f true false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    bif f true false then m else 0
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
⊢ bitwise' f m 0 = bif f true false then m else 0
unfold bitwise'
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
⊢ ∀ (b : Bool) (n : ℕ),
    binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif f true false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) (bit b n) 0 =
      bif f true false then bit b n else 0
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif f true false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    bif f true false then m else 0
apply bitCasesOn m
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
b✝ : Bool
n✝ : ℕ
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif f true false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) (bit b✝ n✝) 0 =
    bif f true false then bit b✝ n✝ else 0
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
⊢ ∀ (b : Bool) (n : ℕ),
    binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif f true false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) (bit b n) 0 =
      bif f true false then bit b n else 0
intros
case h
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
b✝ : Bool
n✝ : ℕ
⊢ (binaryRec (bif f true false then bit false 0 else 0) fun b n x => bit (f false b) (bif f false true then n else 0)) =
    fun n => bif f false true then n else 0
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
b✝ : Bool
n✝ : ℕ
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif f true false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) (bit b✝ n✝) 0 =
    bif f true false then bit b✝ n✝ else 0
rw [binaryRec_eq, binaryRec_zero]
no goals
case h
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
b✝ : Bool
n✝ : ℕ
⊢ (binaryRec (bif f true false then bit false 0 else 0) fun b n x => bit (f false b) (bif f false true then n else 0)) =
    fun n => bif f false true then n else 0
exact bitwise'_bit_aux h