case h.h
m n : ℤ
⊢ bitwise or m n = lor m n
⊢ bitwise or = lor
funext m n
case h.h.ofNat.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' (fun a b => a && !b) m n

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

case h.h.negSucc.negSucc
m n : ℕ
⊢ Nat.bitwise' (fun x y => !(!x || !y)) m n = Nat.bitwise' and m n
case h.h.ofNat.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' (fun a b => a && !b) m n

case h.h.negSucc.negSucc
m n : ℕ
⊢ Nat.bitwise' (fun x y => !(!x || !y)) m n = Nat.bitwise' and m n
. rw [Nat.bitwise'_swap, Function.swap]
  congr
  funext x y
  cases x <;> cases y <;> rfl
  rfl
case h.h.negSucc.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' (fun a b => a && !b) m n

case h.h.negSucc.negSucc
m n : ℕ
⊢ Nat.bitwise' (fun x y => !(!x || !y)) m n = Nat.bitwise' and 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 => !(!x || !y)) m n = Nat.bitwise' and m n
. congr
  funext x y
  cases x <;> cases y <;> rfl
case h.h.ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise' (fun y x => !(x || !y)) n m = Nat.bitwise' (fun a b => a && !b) n m

case h.h.ofNat.negSucc
m n : ℕ
⊢ (!(false || !false)) = false
case h.h.ofNat.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.ofNat.negSucc.e_f
m n : ℕ
⊢ (fun y x => !(x || !y)) = fun a b => a && !b

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

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

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

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

case h.h.ofNat.negSucc
m n : ℕ
⊢ (!(false || !false)) = false
cases x <;> cases y <;> rfl
no goals
case h.h.ofNat.negSucc
m n : ℕ
⊢ (!(false || !false)) = false
rfl
case h.h.negSucc.ofNat.e_f
m n : ℕ
⊢ (fun x y => !(!x || y)) = fun a b => a && !b
case h.h.negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise' (fun x y => !(!x || y)) m n = Nat.bitwise' (fun a b => a && !b) 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)) = fun a b => a && !b
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.e_f
m n : ℕ
⊢ (fun x y => !(!x || !y)) = and
case h.h.negSucc.negSucc
m n : ℕ
⊢ Nat.bitwise' (fun x y => !(!x || !y)) m n = Nat.bitwise' and m n
congr
case h.h.negSucc.negSucc.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(!x || !y)) = (x && y)
case h.h.negSucc.negSucc.e_f
m n : ℕ
⊢ (fun x y => !(!x || !y)) = and
funext x y
no goals
case h.h.negSucc.negSucc.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(!x || !y)) = (x && y)
cases x <;> cases y <;> rfl