case h.h
m n : ℤ
⊢ bitwise xor m n = lxor' m n
⊢ bitwise xor = lxor'
funext m n
case h.h.ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise' (fun x y => !xor x !y) m n = Nat.bitwise' xor m n

case h.h.negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise' (fun x y => !xor (!x) y) m n = Nat.bitwise' xor m n

case h.h.negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise' (fun x y => xor (!x) !y) m n) = ↑(Nat.bitwise' xor m n)
case h.h
m n : ℤ
⊢ bitwise xor m n = lxor' m n
cases' m with m m <;> cases' n with n n <;> try {rfl}
  <;> simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true,
    cond_false, cond_true, lor, Nat.ldiff', Bool.and_true, negSucc.injEq, Bool.false_xor,
    Bool.true_xor, Bool.and_false, Nat.land', Bool.not_true, ldiff', Nat.lor', lxor', Nat.lxor']
case h.h.negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise' (fun x y => !xor (!x) y) m n = Nat.bitwise' xor m n

case h.h.negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise' (fun x y => xor (!x) !y) m n) = ↑(Nat.bitwise' xor m n)
case h.h.ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise' (fun x y => !xor x !y) m n = Nat.bitwise' xor m n

case h.h.negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise' (fun x y => !xor (!x) y) m n = Nat.bitwise' xor m n

case h.h.negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise' (fun x y => xor (!x) !y) m n) = ↑(Nat.bitwise' xor m n)
. congr
  funext x y
  cases x <;> cases y <;> rfl
case h.h.negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise' (fun x y => xor (!x) !y) m n) = ↑(Nat.bitwise' xor m n)
case h.h.negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise' (fun x y => !xor (!x) y) m n = Nat.bitwise' xor m n

case h.h.negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise' (fun x y => xor (!x) !y) m n) = ↑(Nat.bitwise' xor m n)
. congr
  funext x y
  cases x <;> cases y <;> rfl
no goals
case h.h.negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise' (fun x y => xor (!x) !y) m n) = ↑(Nat.bitwise' xor m n)
. congr
  funext x y
  cases x <;> cases y <;> rfl
case h.h.ofNat.negSucc.e_f
m n : ℕ
⊢ (fun x y => !xor x !y) = xor
case h.h.ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise' (fun x y => !xor x !y) m n = Nat.bitwise' xor m n
congr
case h.h.ofNat.negSucc.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!xor x !y) = xor x y
case h.h.ofNat.negSucc.e_f
m n : ℕ
⊢ (fun x y => !xor x !y) = xor
funext x y
no goals
case h.h.ofNat.negSucc.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!xor x !y) = xor x y
cases x <;> cases y <;> rfl
case h.h.negSucc.ofNat.e_f
m n : ℕ
⊢ (fun x y => !xor (!x) y) = xor
case h.h.negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise' (fun x y => !xor (!x) y) m n = Nat.bitwise' xor m n
congr
case h.h.negSucc.ofNat.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!xor (!x) y) = xor x y
case h.h.negSucc.ofNat.e_f
m n : ℕ
⊢ (fun x y => !xor (!x) y) = xor
funext x y
no goals
case h.h.negSucc.ofNat.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!xor (!x) y) = xor x y
cases x <;> cases y <;> rfl
case h.h.negSucc.negSucc.e_a.e_f
m n : ℕ
⊢ (fun x y => xor (!x) !y) = xor
case h.h.negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise' (fun x y => xor (!x) !y) m n) = ↑(Nat.bitwise' xor m n)
congr
case h.h.negSucc.negSucc.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (xor (!x) !y) = xor x y
case h.h.negSucc.negSucc.e_a.e_f
m n : ℕ
⊢ (fun x y => xor (!x) !y) = xor
funext x y
no goals
case h.h.negSucc.negSucc.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (xor (!x) !y) = xor x y
cases x <;> cases y <;> rfl