case h.h
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
⊢ bitwise' (Function.swap f) m n = Function.swap (bitwise' f) m n
f : Bool → Bool → Bool
h : f false false = false
⊢ bitwise' (Function.swap f) = Function.swap (bitwise' f)
funext m n
case h.h
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
⊢ ∀ (n : ℕ), bitwise' (Function.swap f) m n = Function.swap (bitwise' f) m n
case h.h
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
⊢ bitwise' (Function.swap f) m n = Function.swap (bitwise' f) m n
revert n
case h.h
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
⊢ ∀ (n : ℕ), bitwise' (fun y x => f x y) m n = bitwise' f n m
case h.h
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
⊢ ∀ (n : ℕ), bitwise' (Function.swap f) m n = Function.swap (bitwise' f) m n
dsimp [Function.swap]
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
⊢ bitwise' (fun y x => f x y) 0 n = bitwise' f n 0

f : Bool → Bool → Bool
h : f false false = false
m : ℕ
n : Bool
⊢ ∀ (n_1 : ℕ),
    (∀ (n : ℕ), bitwise' (fun y x => f x y) n_1 n = bitwise' f n n_1) →
      ∀ (n_2 : ℕ), bitwise' (fun y x => f x y) (bit n n_1) n_2 = bitwise' f n_2 (bit n n_1)
case h.h
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
⊢ ∀ (n : ℕ), bitwise' (fun y x => f x y) m n = bitwise' f n m
apply binaryRec _ _ m <;> intro n
case h
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
⊢ f false false = false
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
⊢ bitwise' (fun y x => f x y) 0 n = bitwise' f n 0
rw [bitwise'_zero_left, bitwise'_zero_right]
no goals
case h
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
⊢ f false false = false
exact h
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
n : Bool
a : ℕ
ih : ∀ (n : ℕ), bitwise' (fun y x => f x y) a n = bitwise' f n a
m' : ℕ
⊢ bitwise' (fun y x => f x y) (bit n a) m' = bitwise' f m' (bit n a)
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
n : Bool
⊢ ∀ (n_1 : ℕ),
    (∀ (n : ℕ), bitwise' (fun y x => f x y) n_1 n = bitwise' f n n_1) →
      ∀ (n_2 : ℕ), bitwise' (fun y x => f x y) (bit n n_1) n_2 = bitwise' f n_2 (bit n n_1)
intros a ih m'
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
n : Bool
a : ℕ
ih : ∀ (n : ℕ), bitwise' (fun y x => f x y) a n = bitwise' f n a
m' : ℕ
⊢ ∀ (b : Bool) (n_1 : ℕ), bitwise' (fun y x => f x y) (bit n a) (bit b n_1) = bitwise' f (bit b n_1) (bit n a)
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
n : Bool
a : ℕ
ih : ∀ (n : ℕ), bitwise' (fun y x => f x y) a n = bitwise' f n a
m' : ℕ
⊢ bitwise' (fun y x => f x y) (bit n a) m' = bitwise' f m' (bit n a)
apply bitCasesOn m'
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
n : Bool
a : ℕ
ih : ∀ (n : ℕ), bitwise' (fun y x => f x y) a n = bitwise' f n a
m' : ℕ
b : Bool
n' : ℕ
⊢ bitwise' (fun y x => f x y) (bit n a) (bit b n') = bitwise' f (bit b n') (bit n a)
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
n : Bool
a : ℕ
ih : ∀ (n : ℕ), bitwise' (fun y x => f x y) a n = bitwise' f n a
m' : ℕ
⊢ ∀ (b : Bool) (n_1 : ℕ), bitwise' (fun y x => f x y) (bit n a) (bit b n_1) = bitwise' f (bit b n_1) (bit n a)
intro b n'
no goals
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
n : Bool
a : ℕ
ih : ∀ (n : ℕ), bitwise' (fun y x => f x y) a n = bitwise' f n a
m' : ℕ
b : Bool
n' : ℕ
⊢ bitwise' (fun y x => f x y) (bit n a) (bit b n') = bitwise' f (bit b n') (bit n a)
rw [bitwise'_bit, bitwise'_bit, ih] <;> exact h