case ofNat.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f false false then -[Nat.bitwise' (fun x y => !f x y) (Nat.bit a m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise' f (Nat.bit a m) (Nat.bit b n))) =
    bit (f a b) (bif f false false then -[Nat.bitwise' (fun x y => !f x y) m n+1] else ↑(Nat.bitwise' f m n))

case ofNat.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f false true then -[Nat.bitwise' (fun x y => !f x !y) (Nat.bit a m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f x !y) (Nat.bit a m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f false true then -[Nat.bitwise' (fun x y => !f x !y) m n+1] else ↑(Nat.bitwise' (fun x y => f x !y) m n))

case negSucc.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) (Nat.bit (!a) m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) y) (Nat.bit (!a) m) (Nat.bit b n))) =
    bit (f a b)
      (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) y) m n))

case negSucc.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) !y) m n))
f : Bool → Bool → Bool
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n)
cases' m with m m <;> cases' n with n n <;>
simp only [bitwise, ofNat_eq_coe, bit_coe_nat, natBitwise, Bool.not_false, Bool.not_eq_false',
  bit_negSucc]
case ofNat.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f false true then -[Nat.bitwise' (fun x y => !f x !y) (Nat.bit a m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f x !y) (Nat.bit a m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f false true then -[Nat.bitwise' (fun x y => !f x !y) m n+1] else ↑(Nat.bitwise' (fun x y => f x !y) m n))

case negSucc.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) (Nat.bit (!a) m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) y) (Nat.bit (!a) m) (Nat.bit b n))) =
    bit (f a b)
      (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) y) m n))

case negSucc.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) !y) m n))
case ofNat.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f false false then -[Nat.bitwise' (fun x y => !f x y) (Nat.bit a m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise' f (Nat.bit a m) (Nat.bit b n))) =
    bit (f a b) (bif f false false then -[Nat.bitwise' (fun x y => !f x y) m n+1] else ↑(Nat.bitwise' f m n))

case ofNat.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f false true then -[Nat.bitwise' (fun x y => !f x !y) (Nat.bit a m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f x !y) (Nat.bit a m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f false true then -[Nat.bitwise' (fun x y => !f x !y) m n+1] else ↑(Nat.bitwise' (fun x y => f x !y) m n))

case negSucc.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) (Nat.bit (!a) m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) y) (Nat.bit (!a) m) (Nat.bit b n))) =
    bit (f a b)
      (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) y) m n))

case negSucc.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) !y) m n))
. by_cases h : f false false <;> simp [h]
case negSucc.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) (Nat.bit (!a) m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) y) (Nat.bit (!a) m) (Nat.bit b n))) =
    bit (f a b)
      (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) y) m n))

case negSucc.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) !y) m n))
case ofNat.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f false true then -[Nat.bitwise' (fun x y => !f x !y) (Nat.bit a m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f x !y) (Nat.bit a m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f false true then -[Nat.bitwise' (fun x y => !f x !y) m n+1] else ↑(Nat.bitwise' (fun x y => f x !y) m n))

case negSucc.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) (Nat.bit (!a) m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) y) (Nat.bit (!a) m) (Nat.bit b n))) =
    bit (f a b)
      (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) y) m n))

case negSucc.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) !y) m n))
. by_cases h : f false true <;> simp [h]
case negSucc.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) !y) m n))
case negSucc.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) (Nat.bit (!a) m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) y) (Nat.bit (!a) m) (Nat.bit b n))) =
    bit (f a b)
      (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) y) m n))

case negSucc.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) !y) m n))
. by_cases h : f true false <;> simp [h]
no goals
case negSucc.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) !y) m n))
. by_cases h : f true true <;> simp [h]
no goals
case ofNat.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f false false then -[Nat.bitwise' (fun x y => !f x y) (Nat.bit a m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise' f (Nat.bit a m) (Nat.bit b n))) =
    bit (f a b) (bif f false false then -[Nat.bitwise' (fun x y => !f x y) m n+1] else ↑(Nat.bitwise' f m n))
by_cases h : f false false <;> simp [h]
no goals
case ofNat.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f false true then -[Nat.bitwise' (fun x y => !f x !y) (Nat.bit a m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f x !y) (Nat.bit a m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f false true then -[Nat.bitwise' (fun x y => !f x !y) m n+1] else ↑(Nat.bitwise' (fun x y => f x !y) m n))
by_cases h : f false true <;> simp [h]
no goals
case negSucc.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) (Nat.bit (!a) m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) y) (Nat.bit (!a) m) (Nat.bit b n))) =
    bit (f a b)
      (bif f true false then -[Nat.bitwise' (fun x y => !f (!x) y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) y) m n))
by_cases h : f true false <;> simp [h]
no goals
case negSucc.negSucc
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
    else ↑(Nat.bitwise' (fun x y => f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n))) =
    bit (f a b)
      (bif f true true then -[Nat.bitwise' (fun x y => !f (!x) !y) m n+1]
      else ↑(Nat.bitwise' (fun x y => f (!x) !y) m n))
by_cases h : f true true <;> simp [h]