f : Bool → Bool → Bool
h : f false false = false
k : ℕ
⊢ ∀ (m n : ℕ), testBit (bitwise' f m n) k = f (testBit m k) (testBit n k)
f : Bool → Bool → Bool
h : f false false = false
m n k : ℕ
⊢ testBit (bitwise' f m n) k = f (testBit m k) (testBit n k)
revert m n
case zero
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
a : Bool
m' : ℕ
b : Bool
n' : ℕ
⊢ testBit (bit (f a b) (bitwise' f m' n')) zero = f (testBit (bit a m') zero) (testBit (bit b n') zero)

case succ
f : Bool → Bool → Bool
h : f false false = false
k : ℕ
IH : ∀ (m n : ℕ), testBit (bitwise' f m n) k = f (testBit m k) (testBit n k)
m n : ℕ
a : Bool
m' : ℕ
b : Bool
n' : ℕ
⊢ testBit (bit (f a b) (bitwise' f m' n')) (succ k) = f (testBit (bit a m') (succ k)) (testBit (bit b n') (succ k))
f : Bool → Bool → Bool
h : f false false = false
k : ℕ
⊢ ∀ (m n : ℕ), testBit (bitwise' f m n) k = f (testBit m k) (testBit n k)
induction' k with k IH <;>
intros m n <;>
apply bitCasesOn m <;> intros a m' <;>
apply bitCasesOn n <;> intros b n' <;>
rw [bitwise'_bit h]
no goals
case zero
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
a : Bool
m' : ℕ
b : Bool
n' : ℕ
⊢ testBit (bit (f a b) (bitwise' f m' n')) zero = f (testBit (bit a m') zero) (testBit (bit b n') zero)
simp [testBit_zero]
no goals
case succ
f : Bool → Bool → Bool
h : f false false = false
k : ℕ
IH : ∀ (m n : ℕ), testBit (bitwise' f m n) k = f (testBit m k) (testBit n k)
m n : ℕ
a : Bool
m' : ℕ
b : Bool
n' : ℕ
⊢ testBit (bit (f a b) (bitwise' f m' n')) (succ k) = f (testBit (bit a m') (succ k)) (testBit (bit b n') (succ k))
simp [testBit_succ, IH]