awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ (!true && false) = (false && !true)

Tactic:
rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ (!false && true) = (true && !false)

Tactic:
rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ (!true && true) = (true && !true)

Tactic:
rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
h : (fun (x y : Bool) ↦ !(!x && !y)) = or
⊢ -[Nat.bitwise (fun (x y : Bool) ↦ !(!x && !y)) m n+1] = -[m+1].land -[n+1]

Tactic:
congr
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ (fun (x y : Bool) ↦ !(!x && !y)) = or

Tactic:
simp
-- Module: Mathlib.Data.Int.Bitwise
Goal:
h : ∀ (m n : ℤ), bitwise (fun (a b : Bool) ↦ a && !b) m n = m.ldiff n
⊢ (bitwise fun (a b : Bool) ↦ a && !b) = ldiff

Tactic:
funext m n
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℤ
h : ∀ (m : ℕ), bitwise (fun (a b : Bool) ↦ a && !b) (ofNat m) n = (ofNat m).ldiff n
h₁ : ∀ (m : ℕ), bitwise (fun (a b : Bool) ↦ a && !b) -[m+1] n = -[m+1].ldiff n
⊢ bitwise (fun (a b : Bool) ↦ a && !b) m n = m.ldiff n

Tactic:
rcases m with m | m
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℤ
m : ℕ
h : ∀ (n : ℕ), bitwise (fun (a b : Bool) ↦ a && !b) (ofNat m) (ofNat n) = (ofNat m).ldiff (ofNat n)
h₁ : ∀ (n : ℕ), bitwise (fun (a b : Bool) ↦ a && !b) (ofNat m) -[n+1] = (ofNat m).ldiff -[n+1]
⊢ bitwise (fun (a b : Bool) ↦ a && !b) (ofNat m) n = (ofNat m).ldiff n

Tactic:
rcases n with n | n
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℤ
m : ℕ
h : ∀ (n : ℕ), bitwise (fun (a b : Bool) ↦ a && !b) -[m+1] (ofNat n) = -[m+1].ldiff (ofNat n)
h₁ : ∀ (n : ℕ), bitwise (fun (a b : Bool) ↦ a && !b) -[m+1] -[n+1] = -[m+1].ldiff -[n+1]
⊢ bitwise (fun (a b : Bool) ↦ a && !b) -[m+1] n = -[m+1].ldiff n

Tactic:
rcases n with n | n
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ bitwise (fun (a b : Bool) ↦ a && !b) (ofNat m) (ofNat n) = (ofNat m).ldiff (ofNat n)

Tactic:
rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ bitwise (fun (a b : Bool) ↦ a && !b) (ofNat m) (ofNat n) = (ofNat m).ldiff (ofNat n)

Tactic:
{rfl}
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ bitwise (fun (a b : Bool) ↦ a && !b) (ofNat m) (ofNat n) = (ofNat m).ldiff (ofNat n)

Tactic:
try {rfl}
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
h : Nat.bitwise (fun (x y : Bool) ↦ !(!x && !y)) m n = m ||| n
⊢ bitwise (fun (a b : Bool) ↦ a && !b) -[m+1] (ofNat n) = -[m+1].ldiff (ofNat n)

Tactic:
simp only [bitwise, natBitwise, Bool.not_false,
      cond_false, cond_true, Nat.ldiff, Bool.and_true, negSucc.injEq,
      Bool.and_false, Bool.not_true, ldiff]

Premises used: Int.natBitwise, Bool.not_false, Bool.and_false, Int.bitwise, Bool.and_true, Int.ldiff, cond_true, Int.negSucc.injEq, Nat.ldiff, cond_false, Bool.not_true
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
h : (fun (x y : Bool) ↦ x && !!y) = and
⊢ Eq (α := ℤ) (↑(Nat.bitwise (fun (x y : Bool) ↦ x && !!y) m n) : ℤ) (↑(m &&& n) : ℤ)

Tactic:
congr
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ (fun (x y : Bool) ↦ x && !!y) = and

Tactic:
simp
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
h : (fun (x y : Bool) ↦ !(!x && !y)) = or
⊢ Nat.bitwise (fun (x y : Bool) ↦ !(!x && !y)) m n = m ||| n

Tactic:
congr
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
h :
  Eq (α := ℤ) (↑(Nat.bitwise (fun (y x : Bool) ↦ !x && !!y) n m) : ℤ)
    (↑(Nat.bitwise (fun (a b : Bool) ↦ a && !b) n m) : ℤ)
⊢ Eq (α := ℤ) (↑(Nat.bitwise (fun (x y : Bool) ↦ !x && !!y) m n) : ℤ)
    (↑(Nat.bitwise (fun (a b : Bool) ↦ a && !b) n m) : ℤ)

Tactic:
rw [Nat.bitwise_swap, Function.swap]

Premises used: Function.swap, Nat.bitwise_swap
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
h : Eq (α := Bool → Bool → Bool) (fun (y x : Bool) ↦ !x && !!y) fun (a b : Bool) ↦ a && !b
⊢ Eq (α := ℤ) (↑(Nat.bitwise (fun (y x : Bool) ↦ !x && !!y) n m) : ℤ)
    (↑(Nat.bitwise (fun (a b : Bool) ↦ a && !b) n m) : ℤ)

Tactic:
congr
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
h : ∀ (x y : Bool), (!y && !!x) = (x && !y)
⊢ Eq (α := Bool → Bool → Bool) (fun (y x : Bool) ↦ !x && !!y) fun (a b : Bool) ↦ a && !b

Tactic:
funext x y
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
x y : Bool
h : (!y && !!false) = (false && !y)
h₁ : (!y && !!true) = (true && !y)
⊢ (!y && !!x) = (x && !y)

Tactic:
cases x
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
y : Bool
h : (!false && !!false) = (false && !false)
h₁ : (!true && !!false) = (false && !true)
⊢ (!y && !!false) = (false && !y)

Tactic:
cases y
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
y : Bool
h : (!false && !!true) = (true && !false)
h₁ : (!true && !!true) = (true && !true)
⊢ (!y && !!true) = (true && !y)

Tactic:
cases y
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ (!false && !!false) = (false && !false)

Tactic:
rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ (!true && !!false) = (false && !true)

Tactic:
rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ (!false && !!true) = (true && !false)

Tactic:
rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ (!true && !!true) = (true && !true)

Tactic:
rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
h : ∀ (m n : ℤ), bitwise xor m n = m.xor n
⊢ bitwise xor = Int.xor

Tactic:
funext m n
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℤ
h : ∀ (m : ℕ), bitwise xor (ofNat m) n = (ofNat m).xor n
h₁ : ∀ (m : ℕ), bitwise xor -[m+1] n = -[m+1].xor n
⊢ bitwise xor m n = m.xor n

Tactic:
rcases m with m | m
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℤ
m : ℕ
h : ∀ (n : ℕ), bitwise xor (ofNat m) (ofNat n) = (ofNat m).xor (ofNat n)
h₁ : ∀ (n : ℕ), bitwise xor (ofNat m) -[n+1] = (ofNat m).xor -[n+1]
⊢ bitwise xor (ofNat m) n = (ofNat m).xor n

Tactic:
rcases n with n | n
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℤ
m : ℕ
h : ∀ (n : ℕ), bitwise xor -[m+1] (ofNat n) = -[m+1].xor (ofNat n)
h₁ : ∀ (n : ℕ), bitwise xor -[m+1] -[n+1] = -[m+1].xor -[n+1]
⊢ bitwise xor -[m+1] n = -[m+1].xor n

Tactic:
rcases n with n | n
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ bitwise xor (ofNat m) (ofNat n) = (ofNat m).xor (ofNat n)

Tactic:
rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ bitwise xor (ofNat m) (ofNat n) = (ofNat m).xor (ofNat n)

Tactic:
{rfl}
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ bitwise xor (ofNat m) (ofNat n) = (ofNat m).xor (ofNat n)

Tactic:
try {rfl}
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
h : Nat.bitwise (fun (x y : Bool) ↦ !(x ^^ !y)) m n = Nat.bitwise xor m n
⊢ bitwise xor (ofNat m) -[n+1] = (ofNat m).xor -[n+1]

Tactic:
simp only [bitwise, natBitwise, Bool.not_false, Bool.bne_eq_xor,
      cond_false, cond_true, negSucc.injEq, Bool.false_xor,
      Bool.true_xor, Bool.not_true,
      Int.xor, HXor.hXor, XorOp.xor, Nat.xor]

Premises used: Bool.false_xor, Int.natBitwise, Bool.not_false, Int.bitwise, cond_true, XorOp.xor, Bool.true_xor, Int.negSucc.injEq, HXor.hXor, Nat.xor, Int.xor, cond_false, Bool.bne_eq_xor, Bool.not_true
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
h : Nat.bitwise (fun (x y : Bool) ↦ !(!x ^^ y)) m n = Nat.bitwise xor m n
⊢ bitwise xor -[m+1] (ofNat n) = -[m+1].xor (ofNat n)

Tactic:
simp only [bitwise, natBitwise, Bool.not_false, Bool.bne_eq_xor,
      cond_false, cond_true, negSucc.injEq, Bool.false_xor,
      Bool.true_xor, Bool.not_true,
      Int.xor, HXor.hXor, XorOp.xor, Nat.xor]

Premises used: Bool.false_xor, Int.natBitwise, Bool.not_false, Int.bitwise, cond_true, XorOp.xor, Bool.true_xor, Int.negSucc.injEq, HXor.hXor, Nat.xor, Int.xor, cond_false, Bool.bne_eq_xor, Bool.not_true
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ Nat.bitwise (fun (x y : Bool) ↦ !(x ^^ !y)) m n = Nat.bitwise xor m n

Tactic:
simp
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ Nat.bitwise (fun (x y : Bool) ↦ !(!x ^^ y)) m n = Nat.bitwise xor m n

Tactic:
simp
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ Eq (α := ℤ) (↑(Nat.bitwise (fun (x y : Bool) ↦ !x ^^ !y) m n) : ℤ) (↑(Nat.bitwise xor m n) : ℤ)

Tactic:
simp
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
a : Bool
m : ℤ
b : Bool
n : ℤ
ofNat : ∀ (m : ℕ), bitwise f (bit a (Int.ofNat m)) (bit b n) = bit (f a b) (bitwise f (Int.ofNat m) n)
negSucc : ∀ (m : ℕ), bitwise f (bit a -[m+1]) (bit b n) = bit (f a b) (bitwise f -[m+1] n)
⊢ bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n)

Tactic:
rcases m with m | m
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
a b : Bool
n : ℤ
m : ℕ
ofNat :
  ∀ (n : ℕ), bitwise f (bit a (Int.ofNat m)) (bit b (Int.ofNat n)) = bit (f a b) (bitwise f (Int.ofNat m) (Int.ofNat n))
ofNat₁ : ∀ (n : ℕ), bitwise f (bit a (Int.ofNat m)) (bit b -[n+1]) = bit (f a b) (bitwise f (Int.ofNat m) -[n+1])
⊢ bitwise f (bit a (Int.ofNat m)) (bit b n) = bit (f a b) (bitwise f (Int.ofNat m) n)

Tactic:
rcases n with n | n
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
a b : Bool
n : ℤ
m : ℕ
negSucc : ∀ (n : ℕ), bitwise f (bit a -[m+1]) (bit b (ofNat n)) = bit (f a b) (bitwise f -[m+1] (ofNat n))
negSucc₁ : ∀ (n : ℕ), bitwise f (bit a -[m+1]) (bit b -[n+1]) = bit (f a b) (bitwise f -[m+1] -[n+1])
⊢ bitwise f (bit a -[m+1]) (bit b n) = bit (f a b) (bitwise f -[m+1] n)

Tactic:
rcases n with n | n
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
ofNat :
  (bif f false false then -[Nat.bitwise (fun (x y : Bool) ↦ !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 : Bool) ↦ !f x y) m n+1] else (↑(Nat.bitwise f m n) : ℤ))
⊢ bitwise f (bit a (Int.ofNat m)) (bit b (Int.ofNat n)) = bit (f a b) (bitwise f (Int.ofNat m) (Int.ofNat n))

Tactic:
simp [bitwise, ofNat_eq_natCast, bit_coe_nat, natBitwise, Bool.not_false,
    bit_negSucc]

Premises used: Int.natBitwise, Bool.not_false, Int.bitwise, Int.bit_negSucc, Int.ofNat_eq_natCast, Int.bit_coe_nat
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
ofNat :
  (bif f false true then -[Nat.bitwise (fun (x y : Bool) ↦ !f x !y) (Nat.bit a m) (Nat.bit (!b) n)+1]
    else (↑(Nat.bitwise (fun (x y : Bool) ↦ 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 : Bool) ↦ !f x !y) m n+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ f x !y) m n) : ℤ))
⊢ bitwise f (bit a (Int.ofNat m)) (bit b -[n+1]) = bit (f a b) (bitwise f (Int.ofNat m) -[n+1])

Tactic:
simp [bitwise, ofNat_eq_natCast, bit_coe_nat, natBitwise, Bool.not_false,
    bit_negSucc]

Premises used: Int.natBitwise, Bool.not_false, Int.bitwise, Int.bit_negSucc, Int.ofNat_eq_natCast, Int.bit_coe_nat
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
negSucc :
  (bif f true false then -[Nat.bitwise (fun (x y : Bool) ↦ !f (!x) y) (Nat.bit (!a) m) (Nat.bit b n)+1]
    else (↑(Nat.bitwise (fun (x y : Bool) ↦ 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 : Bool) ↦ !f (!x) y) m n+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ f (!x) y) m n) : ℤ))
⊢ bitwise f (bit a -[m+1]) (bit b (ofNat n)) = bit (f a b) (bitwise f -[m+1] (ofNat n))

Tactic:
simp [bitwise, ofNat_eq_natCast, bit_coe_nat, natBitwise, Bool.not_false,
    bit_negSucc]

Premises used: Int.natBitwise, Bool.not_false, Int.bitwise, Int.bit_negSucc, Int.ofNat_eq_natCast, Int.bit_coe_nat
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
negSucc :
  (bif f true true then -[Nat.bitwise (fun (x y : Bool) ↦ !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
    else (↑(Nat.bitwise (fun (x y : Bool) ↦ 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 : Bool) ↦ !f (!x) !y) m n+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ f (!x) !y) m n) : ℤ))
⊢ bitwise f (bit a -[m+1]) (bit b -[n+1]) = bit (f a b) (bitwise f -[m+1] -[n+1])

Tactic:
simp [bitwise, ofNat_eq_natCast, bit_coe_nat, natBitwise, Bool.not_false,
    bit_negSucc]

Premises used: Int.natBitwise, Bool.not_false, Int.bitwise, Int.bit_negSucc, Int.ofNat_eq_natCast, Int.bit_coe_nat
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
pos :
  ∀ (h : f false false = true),
    (bif f false false then -[Nat.bitwise (fun (x y : Bool) ↦ !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 : Bool) ↦ !f x y) m n+1] else (↑(Nat.bitwise f m n) : ℤ))
neg :
  ∀ (h : ¬f false false = true),
    (bif f false false then -[Nat.bitwise (fun (x y : Bool) ↦ !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 : Bool) ↦ !f x y) m n+1] else (↑(Nat.bitwise f m n) : ℤ))
⊢ (bif f false false then -[Nat.bitwise (fun (x y : Bool) ↦ !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 : Bool) ↦ !f x y) m n+1] else (↑(Nat.bitwise f m n) : ℤ))

Tactic:
by_cases h : f false false

Premises used: Bool.false
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : f false false = true
⊢ (bif f false false then -[Nat.bitwise (fun (x y : Bool) ↦ !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 : Bool) ↦ !f x y) m n+1] else (↑(Nat.bitwise f m n) : ℤ))

Tactic:
simp +decide [h]

Premises used: Decidable.decide
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : ¬f false false = true
⊢ (bif f false false then -[Nat.bitwise (fun (x y : Bool) ↦ !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 : Bool) ↦ !f x y) m n+1] else (↑(Nat.bitwise f m n) : ℤ))

Tactic:
simp +decide [h]

Premises used: Decidable.decide
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
pos :
  ∀ (h : f false true = true),
    (bif f false true then -[Nat.bitwise (fun (x y : Bool) ↦ !f x !y) (Nat.bit a m) (Nat.bit (!b) n)+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ 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 : Bool) ↦ !f x !y) m n+1]
        else (↑(Nat.bitwise (fun (x y : Bool) ↦ f x !y) m n) : ℤ))
neg :
  ∀ (h : ¬f false true = true),
    (bif f false true then -[Nat.bitwise (fun (x y : Bool) ↦ !f x !y) (Nat.bit a m) (Nat.bit (!b) n)+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ 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 : Bool) ↦ !f x !y) m n+1]
        else (↑(Nat.bitwise (fun (x y : Bool) ↦ f x !y) m n) : ℤ))
⊢ (bif f false true then -[Nat.bitwise (fun (x y : Bool) ↦ !f x !y) (Nat.bit a m) (Nat.bit (!b) n)+1]
    else (↑(Nat.bitwise (fun (x y : Bool) ↦ 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 : Bool) ↦ !f x !y) m n+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ f x !y) m n) : ℤ))

Tactic:
by_cases h : f false true

Premises used: Bool.true, Bool.false
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : f false true = true
⊢ (bif f false true then -[Nat.bitwise (fun (x y : Bool) ↦ !f x !y) (Nat.bit a m) (Nat.bit (!b) n)+1]
    else (↑(Nat.bitwise (fun (x y : Bool) ↦ 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 : Bool) ↦ !f x !y) m n+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ f x !y) m n) : ℤ))

Tactic:
simp +decide [h]

Premises used: Decidable.decide
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : ¬f false true = true
⊢ (bif f false true then -[Nat.bitwise (fun (x y : Bool) ↦ !f x !y) (Nat.bit a m) (Nat.bit (!b) n)+1]
    else (↑(Nat.bitwise (fun (x y : Bool) ↦ 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 : Bool) ↦ !f x !y) m n+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ f x !y) m n) : ℤ))

Tactic:
simp +decide [h]

Premises used: Decidable.decide
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
pos :
  ∀ (h : f true false = true),
    (bif f true false then -[Nat.bitwise (fun (x y : Bool) ↦ !f (!x) y) (Nat.bit (!a) m) (Nat.bit b n)+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ 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 : Bool) ↦ !f (!x) y) m n+1]
        else (↑(Nat.bitwise (fun (x y : Bool) ↦ f (!x) y) m n) : ℤ))
neg :
  ∀ (h : ¬f true false = true),
    (bif f true false then -[Nat.bitwise (fun (x y : Bool) ↦ !f (!x) y) (Nat.bit (!a) m) (Nat.bit b n)+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ 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 : Bool) ↦ !f (!x) y) m n+1]
        else (↑(Nat.bitwise (fun (x y : Bool) ↦ f (!x) y) m n) : ℤ))
⊢ (bif f true false then -[Nat.bitwise (fun (x y : Bool) ↦ !f (!x) y) (Nat.bit (!a) m) (Nat.bit b n)+1]
    else (↑(Nat.bitwise (fun (x y : Bool) ↦ 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 : Bool) ↦ !f (!x) y) m n+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ f (!x) y) m n) : ℤ))

Tactic:
by_cases h : f true false

Premises used: Bool.true, Bool.false
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : f true false = true
⊢ (bif f true false then -[Nat.bitwise (fun (x y : Bool) ↦ !f (!x) y) (Nat.bit (!a) m) (Nat.bit b n)+1]
    else (↑(Nat.bitwise (fun (x y : Bool) ↦ 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 : Bool) ↦ !f (!x) y) m n+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ f (!x) y) m n) : ℤ))

Tactic:
simp +decide [h]

Premises used: Decidable.decide
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : ¬f true false = true
⊢ (bif f true false then -[Nat.bitwise (fun (x y : Bool) ↦ !f (!x) y) (Nat.bit (!a) m) (Nat.bit b n)+1]
    else (↑(Nat.bitwise (fun (x y : Bool) ↦ 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 : Bool) ↦ !f (!x) y) m n+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ f (!x) y) m n) : ℤ))

Tactic:
simp +decide [h]

Premises used: Decidable.decide
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
pos :
  ∀ (h : f true true = true),
    (bif f true true then -[Nat.bitwise (fun (x y : Bool) ↦ !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ 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 : Bool) ↦ !f (!x) !y) m n+1]
        else (↑(Nat.bitwise (fun (x y : Bool) ↦ f (!x) !y) m n) : ℤ))
neg :
  ∀ (h : ¬f true true = true),
    (bif f true true then -[Nat.bitwise (fun (x y : Bool) ↦ !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ 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 : Bool) ↦ !f (!x) !y) m n+1]
        else (↑(Nat.bitwise (fun (x y : Bool) ↦ f (!x) !y) m n) : ℤ))
⊢ (bif f true true then -[Nat.bitwise (fun (x y : Bool) ↦ !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
    else (↑(Nat.bitwise (fun (x y : Bool) ↦ 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 : Bool) ↦ !f (!x) !y) m n+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ f (!x) !y) m n) : ℤ))

Tactic:
by_cases h : f true true

Premises used: Bool.true
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : f true true = true
⊢ (bif f true true then -[Nat.bitwise (fun (x y : Bool) ↦ !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
    else (↑(Nat.bitwise (fun (x y : Bool) ↦ 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 : Bool) ↦ !f (!x) !y) m n+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ f (!x) !y) m n) : ℤ))

Tactic:
simp +decide [h]

Premises used: Decidable.decide
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : ¬f true true = true
⊢ (bif f true true then -[Nat.bitwise (fun (x y : Bool) ↦ !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1]
    else (↑(Nat.bitwise (fun (x y : Bool) ↦ 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 : Bool) ↦ !f (!x) !y) m n+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ f (!x) !y) m n) : ℤ))

Tactic:
simp +decide [h]

Premises used: Decidable.decide
-- Module: Mathlib.Data.Int.Bitwise
Goal:
a : Bool
m : ℤ
b : Bool
n : ℤ
rw : bitwise or (bit a m) (bit b n) = bit (a || b) (bitwise or m n)
rw₁ rw₂ : bit (a || b) (bitwise or m n) = bit (a || b) (bitwise or m n)
⊢ (bit a m).lor (bit b n) = bit (a || b) (m.lor n)

Tactic:
rw [← bitwise_or, bitwise_bit]

Premises used: Int.bitwise_or, Int.bitwise_bit
-- Module: Mathlib.Data.Int.Bitwise
Goal:
a : Bool
m : ℤ
b : Bool
n : ℤ
rw : bitwise and (bit a m) (bit b n) = bit (a && b) (bitwise and m n)
rw₁ rw₂ : bit (a && b) (bitwise and m n) = bit (a && b) (bitwise and m n)
⊢ (bit a m).land (bit b n) = bit (a && b) (m.land n)

Tactic:
rw [← bitwise_and, bitwise_bit]

Premises used: Int.bitwise_bit, Int.bitwise_and
-- Module: Mathlib.Data.Int.Bitwise
Goal:
a : Bool
m : ℤ
b : Bool
n : ℤ
rw : bitwise (fun (a b : Bool) ↦ a && !b) (bit a m) (bit b n) = bit (a && !b) (bitwise (fun (a b : Bool) ↦ a && !b) m n)
rw₁ rw₂ :
  bit (a && !b) (bitwise (fun (a b : Bool) ↦ a && !b) m n) = bit (a && !b) (bitwise (fun (a b : Bool) ↦ a && !b) m n)
⊢ (bit a m).ldiff (bit b n) = bit (a && !b) (m.ldiff n)

Tactic:
rw [← bitwise_diff, bitwise_bit]

Premises used: Int.bitwise_diff, Int.bitwise_bit
-- Module: Mathlib.Data.Int.Bitwise
Goal:
a : Bool
m : ℤ
b : Bool
n : ℤ
rw : bitwise xor (bit a m) (bit b n) = bit (a ^^ b) (bitwise xor m n)
rw₁ rw₂ : bit (a ^^ b) (bitwise xor m n) = bit (a ^^ b) (bitwise xor m n)
⊢ (bit a m).xor (bit b n) = bit (a ^^ b) (m.xor n)

Tactic:
rw [← bitwise_xor, bitwise_bit]

Premises used: Int.bitwise_bit, Int.bitwise_xor
-- Module: Mathlib.Data.Int.Bitwise
Goal:
b : Bool
n : ℕ
⊢ (bit b (↑n : ℤ)).lnot = bit (!b) (lnot (↑n : ℤ))

Tactic:
simp [lnot]

Premises used: Int.lnot
-- Module: Mathlib.Data.Int.Bitwise
Goal:
b : Bool
n : ℕ
⊢ (bit b -[n+1]).lnot = bit (!b) -[n+1].lnot

Tactic:
simp [lnot]

Premises used: Int.lnot
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
m n : ℤ
k : ℕ
ofNat : ∀ (a : ℕ), (bitwise f (Int.ofNat a) n).testBit k = f ((Int.ofNat a).testBit k) (n.testBit k)
negSucc : ∀ (a : ℕ), (bitwise f -[a+1] n).testBit k = f (-[a+1].testBit k) (n.testBit k)
⊢ (bitwise f m n).testBit k = f (m.testBit k) (n.testBit k)

Tactic:
cases m
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
n : ℤ
k a : ℕ
ofNat :
  ∀ (a_1 : ℕ),
    (bitwise f (Int.ofNat a) (Int.ofNat a_1)).testBit k = f ((Int.ofNat a).testBit k) ((Int.ofNat a_1).testBit k)
ofNat₁ : ∀ (a_1 : ℕ), (bitwise f (Int.ofNat a) -[a_1+1]).testBit k = f ((Int.ofNat a).testBit k) (-[a_1+1].testBit k)
⊢ (bitwise f (Int.ofNat a) n).testBit k = f ((Int.ofNat a).testBit k) (n.testBit k)

Tactic:
cases n
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
n : ℤ
k a : ℕ
negSucc : ∀ (a_1 : ℕ), (bitwise f -[a+1] (ofNat a_1)).testBit k = f (-[a+1].testBit k) ((ofNat a_1).testBit k)
negSucc₁ : ∀ (a_1 : ℕ), (bitwise f -[a+1] -[a_1+1]).testBit k = f (-[a+1].testBit k) (-[a_1+1].testBit k)
⊢ (bitwise f -[a+1] n).testBit k = f (-[a+1].testBit k) (n.testBit k)

Tactic:
cases n