case h.h
m n : ℤ
⊢ bitwise (fun a b => a && !b) m n = ldiff' m n
⊢ (bitwise fun a b => a && !b) = ldiff'
funext m n
case h.h.ofNat.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise' (fun x y => x && !!y) m n) = ↑(Nat.bitwise' and m n)

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

case h.h.negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise' (fun x y => !x && !!y) m n) = ↑(Nat.bitwise' (fun a b => a && !b) n m)
case h.h
m n : ℤ
⊢ bitwise (fun a b => a && !b) m n = ldiff' 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', Bool.not_true, ldiff', Nat.lor']
case h.h.negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise' (fun x y => !(!x && !y)) m n = Nat.bitwise' or m n

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

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

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

case h.h.negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise' (fun x y => !x && !!y) m n) = ↑(Nat.bitwise' (fun a b => a && !b) n m)
. congr
  funext x y
  cases x <;> cases y <;> rfl
no goals
case h.h.negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise' (fun x y => !x && !!y) m n) = ↑(Nat.bitwise' (fun a b => a && !b) n m)
. rw [Nat.bitwise'_swap, Function.swap]
  congr
  funext x y
  cases x <;> cases y <;> rfl
  rfl
case h.h.ofNat.negSucc.e_a.e_f
m n : ℕ
⊢ (fun x y => x && !!y) = and
case h.h.ofNat.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise' (fun x y => x && !!y) m n) = ↑(Nat.bitwise' and m n)
congr
case h.h.ofNat.negSucc.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (x && !!y) = (x && y)
case h.h.ofNat.negSucc.e_a.e_f
m n : ℕ
⊢ (fun x y => x && !!y) = and
funext x y
no goals
case h.h.ofNat.negSucc.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (x && !!y) = (x && y)
cases x <;> cases y <;> rfl
case h.h.negSucc.ofNat.e_f
m n : ℕ
⊢ (fun x y => !(!x && !y)) = or
case h.h.negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise' (fun x y => !(!x && !y)) m n = Nat.bitwise' or m n
congr
case h.h.negSucc.ofNat.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(!x && !y)) = (x || y)
case h.h.negSucc.ofNat.e_f
m n : ℕ
⊢ (fun x y => !(!x && !y)) = or
funext x y
no goals
case h.h.negSucc.ofNat.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(!x && !y)) = (x || y)
cases x <;> cases y <;> rfl
case h.h.negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise' (fun y x => !x && !!y) n m) = ↑(Nat.bitwise' (fun a b => a && !b) n m)

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

case h.h.negSucc.negSucc
m n : ℕ
⊢ (!false && !!false) = false
case h.h.negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise' (fun y x => !x && !!y) n m) = ↑(Nat.bitwise' (fun a b => a && !b) n m)

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

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

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

case h.h.negSucc.negSucc
m n : ℕ
⊢ (!false && !!false) = false
cases x <;> cases y <;> rfl
no goals
case h.h.negSucc.negSucc
m n : ℕ
⊢ (!false && !!false) = false
rfl