f : Bool → Bool → Bool
h : f false false = false
a : Bool
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 a m)
      (bit b n) =
    bit (f a b)
      (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 n)
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
⊢ bitwise' f (bit a m) (bit b n) = bit (f a b) (bitwise' f m n)
unfold bitwise'
case h
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
⊢ bit (f a false)
      (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 bit a m else 0

case h
f : Bool → Bool → Bool
h : f false false = false
a : Bool
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
a : Bool
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 a m)
      (bit b n) =
    bit (f a b)
      (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 n)
rw [binaryRec_eq, binaryRec_eq]
case h.false
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ bit (f a false)
      (binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0) =
    bif false then bit a m else 0

case h.true
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ bit (f a false)
      (binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif true then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0) =
    bif true then bit a m else 0
case h
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
⊢ bit (f a false)
      (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 bit a m else 0
induction' ftf : f true false
case h.false
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ bit false
      (binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0) =
    bif false then bit a m else 0

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

case h.true
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ bit (f a false)
      (binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif true then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0) =
    bif true then bit a m else 0
rw [show f a false = false by cases a <;> assumption]
case h.false
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    0

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

case h.true
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ bit (f a false)
      (binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif true then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0) =
    bif true then bit a m else 0
apply @congr_arg _ _ _ 0 (bit false)
case h.true
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ bit (f a false)
      (binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif true then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0) =
    bif true then bit a m else 0

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

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

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

case h.false
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    0
rw [show f a false = a by cases a <;> assumption]
case h.true
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif true then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    m

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

case h.false
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    0
apply congr_arg (bit a)
no goals
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ f a false = false
cases a <;> assumption
no goals
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ f a false = a
cases a <;> assumption
no goals
case h.false
f : Bool → Bool → Bool
h : f false false = false
a✝ : Bool
m✝ : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
a : Bool
m : ℕ
⊢ (bif false then bit a m else 0) = 0
rfl
no goals
case h.false.h
f : Bool → Bool → Bool
h : f false false = false
a✝ : Bool
m✝ : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
a : Bool
m : ℕ
⊢ (binaryRec (bif 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
rw [← bitwise'_bit_aux h, ftf]
no goals
case h
f : Bool → Bool → Bool
h : f false false = false
a : Bool
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