case h.h
m n : ℤ
⊢ bitwise and m n = land m n
⊢ bitwise and = land
funext m n
case h.h.negSucc.ofNat
m n : ℕ
⊢ ↑(Nat.bitwise' (fun x y => !x && y) m n) = land -[m+1] (ofNat n)

case h.h.negSucc.negSucc
m n : ℕ
⊢ -[Nat.bitwise' (fun x y => !(!x && !y)) m n+1] = land -[m+1] -[n+1]
case h.h
m n : ℤ
⊢ bitwise and m n = land 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.and_false, Nat.land']
case h.h.negSucc.negSucc
m n : ℕ
⊢ -[Nat.bitwise' (fun x y => !(!x && !y)) m n+1] = land -[m+1] -[n+1]
case h.h.negSucc.ofNat
m n : ℕ
⊢ ↑(Nat.bitwise' (fun x y => !x && y) m n) = land -[m+1] (ofNat n)

case h.h.negSucc.negSucc
m n : ℕ
⊢ -[Nat.bitwise' (fun x y => !(!x && !y)) m n+1] = land -[m+1] -[n+1]
. rw [Nat.bitwise'_swap, Function.swap]
  congr
  funext x y
  cases x <;> cases y <;> rfl
  rfl
no goals
case h.h.negSucc.negSucc
m n : ℕ
⊢ -[Nat.bitwise' (fun x y => !(!x && !y)) m n+1] = land -[m+1] -[n+1]
. congr
  funext x y
  cases x <;> cases y <;> rfl
case h.h.negSucc.ofNat
m n : ℕ
⊢ ↑(Nat.bitwise' (fun y x => !x && y) n m) = land -[m+1] (ofNat n)

case h.h.negSucc.ofNat
m n : ℕ
⊢ (!false && false) = false
case h.h.negSucc.ofNat
m n : ℕ
⊢ ↑(Nat.bitwise' (fun x y => !x && y) m n) = land -[m+1] (ofNat n)
rw [Nat.bitwise'_swap, Function.swap]
case h.h.negSucc.ofNat.e_a.e_f
m n : ℕ
⊢ (fun y x => !x && y) = fun a b => a && !b

case h.h.negSucc.ofNat
m n : ℕ
⊢ (!false && false) = false
case h.h.negSucc.ofNat
m n : ℕ
⊢ ↑(Nat.bitwise' (fun y x => !x && y) n m) = land -[m+1] (ofNat n)

case h.h.negSucc.ofNat
m n : ℕ
⊢ (!false && false) = false
congr
case h.h.negSucc.ofNat.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!y && x) = (x && !y)

case h.h.negSucc.ofNat
m n : ℕ
⊢ (!false && false) = false
case h.h.negSucc.ofNat.e_a.e_f
m n : ℕ
⊢ (fun y x => !x && y) = fun a b => a && !b

case h.h.negSucc.ofNat
m n : ℕ
⊢ (!false && false) = false
funext x y
case h.h.negSucc.ofNat
m n : ℕ
⊢ (!false && false) = false
case h.h.negSucc.ofNat.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!y && x) = (x && !y)

case h.h.negSucc.ofNat
m n : ℕ
⊢ (!false && false) = false
cases x <;> cases y <;> rfl
no goals
case h.h.negSucc.ofNat
m n : ℕ
⊢ (!false && false) = false
rfl
case h.h.negSucc.negSucc.e_a.e_f
m n : ℕ
⊢ (fun x y => !(!x && !y)) = or
case h.h.negSucc.negSucc
m n : ℕ
⊢ -[Nat.bitwise' (fun x y => !(!x && !y)) m n+1] = land -[m+1] -[n+1]
congr
case h.h.negSucc.negSucc.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(!x && !y)) = (x || y)
case h.h.negSucc.negSucc.e_a.e_f
m n : ℕ
⊢ (fun x y => !(!x && !y)) = or
funext x y
no goals
case h.h.negSucc.negSucc.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(!x && !y)) = (x || y)
cases x <;> cases y <;> rfl