awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n i j : ℕ
⊢ true = (j.bodd ^^ true ^^ j.bodd)

Tactic:
simp
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n i j : ℕ
⊢ (!false) = (j.bodd ^^ (j.bodd ^^ false ^^ Nat.bodd 1))

Tactic:
simp
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n i j : ℕ
⊢ (!true) = (j.bodd ^^ (j.bodd ^^ true ^^ Nat.bodd 1))

Tactic:
simp
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℕ
zero : (negOfNat 0).bodd = Nat.bodd 0
succ : ∀ (n : ℕ), (negOfNat (n + 1)).bodd = (n + 1).bodd
⊢ (negOfNat n).bodd = n.bodd

Tactic:
cases n
-- Module: Mathlib.Data.Int.Bitwise
Goal:
⊢ (negOfNat 0).bodd = Nat.bodd 0

Tactic:
simp +decide

Premises used: Decidable.decide
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℕ
succ : (negOfNat (n + 1)).bodd = !n.bodd
⊢ (negOfNat (n + 1)).bodd = (n + 1).bodd

Tactic:
simp +decide

Premises used: Decidable.decide
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℕ
⊢ (negOfNat (n + 1)).bodd = !n.bodd

Tactic:
rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℤ
ofNat : ∀ (a : ℕ), (-Int.ofNat a).bodd = (Int.ofNat a).bodd
negSucc : ∀ (a : ℕ), (- -[a+1]).bodd = -[a+1].bodd
⊢ (-n).bodd = n.bodd

Tactic:
cases n
-- Module: Mathlib.Data.Int.Bitwise
Goal:
a : ℕ
ofNat : a.bodd = (Int.ofNat a).bodd
⊢ (-Int.ofNat a).bodd = (Int.ofNat a).bodd

Tactic:
simp only [← negOfNat_eq, bodd_negOfNat, neg_negSucc]

Premises used: Int.neg_negSucc, Int.bodd_negOfNat, Int.negOfNat_eq
-- Module: Mathlib.Data.Int.Bitwise
Goal:
a : ℕ
⊢ a.bodd = (ofNat a).bodd

Tactic:
simp [bodd]

Premises used: Int.bodd
-- Module: Mathlib.Data.Int.Bitwise
Goal:
a : ℕ
⊢ bodd (↑(a + 1) : ℤ) = -[a+1].bodd

Tactic:
simp [bodd]

Premises used: Int.bodd
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℤ
ofNat : ∀ (m : ℕ), (Int.ofNat m + n).bodd = ((Int.ofNat m).bodd ^^ n.bodd)
negSucc : ∀ (m : ℕ), (-[m+1] + n).bodd = (-[m+1].bodd ^^ n.bodd)
⊢ (m + n).bodd = (m.bodd ^^ n.bodd)

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

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

Tactic:
rcases n with n | n
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
ofNat : (m.bodd ^^ n.succ.bodd) = (bodd (↑m : ℤ) ^^ -[n+1].bodd)
⊢ (Int.ofNat m + -[n+1]).bodd = ((Int.ofNat m).bodd ^^ -[n+1].bodd)

Tactic:
simp only [ofNat_eq_natCast, ofNat_add_negSucc, negSucc_add_ofNat,
             negSucc_add_negSucc, bodd_subNatNat, ← Nat.cast_add]

Premises used: Int.negSucc_add_ofNat, Int.ofNat_eq_natCast, Nat.cast_add, Int.bodd_subNatNat, Int.ofNat_add_negSucc, Int.negSucc_add_negSucc
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
negSucc : (n.bodd ^^ m.succ.bodd) = (-[m+1].bodd ^^ bodd (↑n : ℤ))
⊢ (-[m+1] + ofNat n).bodd = (-[m+1].bodd ^^ (ofNat n).bodd)

Tactic:
simp only [ofNat_eq_natCast, ofNat_add_negSucc, negSucc_add_ofNat,
             negSucc_add_negSucc, bodd_subNatNat, ← Nat.cast_add]

Premises used: Int.negSucc_add_ofNat, Int.ofNat_eq_natCast, Nat.cast_add, Int.bodd_subNatNat, Int.ofNat_add_negSucc, Int.negSucc_add_negSucc
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ bodd (↑(m + n) : ℤ) = (bodd (↑m : ℤ) ^^ bodd (↑n : ℤ))

Tactic:
simp [bodd, Bool.xor_comm]

Premises used: Int.bodd, Bool.xor_comm
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ (m.bodd ^^ n.succ.bodd) = (bodd (↑m : ℤ) ^^ -[n+1].bodd)

Tactic:
simp [bodd, Bool.xor_comm]

Premises used: Int.bodd, Bool.xor_comm
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ (n.bodd ^^ m.succ.bodd) = (-[m+1].bodd ^^ bodd (↑n : ℤ))

Tactic:
simp [bodd, Bool.xor_comm]

Premises used: Int.bodd, Bool.xor_comm
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ -[(m + n).succ+1].bodd = (-[m+1].bodd ^^ -[n+1].bodd)

Tactic:
simp [bodd, Bool.xor_comm]

Premises used: Int.bodd, Bool.xor_comm
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℤ
ofNat : ∀ (m : ℕ), (Int.ofNat m * n).bodd = ((Int.ofNat m).bodd && n.bodd)
negSucc : ∀ (m : ℕ), (-[m+1] * n).bodd = (-[m+1].bodd && n.bodd)
⊢ (m * n).bodd = (m.bodd && n.bodd)

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

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

Tactic:
rcases n with n | n
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
ofNat : bodd (-(↑(m * n.succ) : ℤ)) = (bodd (↑m : ℤ) && -[n+1].bodd)
⊢ (Int.ofNat m * -[n+1]).bodd = ((Int.ofNat m).bodd && -[n+1].bodd)

Tactic:
simp only [ofNat_eq_natCast, ofNat_mul_negSucc, negSucc_mul_ofNat, ofNat_mul_ofNat,
             negSucc_mul_negSucc]

Premises used: Int.negSucc_mul_ofNat, Int.ofNat_mul_negSucc, Int.ofNat_eq_natCast, Int.ofNat_mul_ofNat, Int.negSucc_mul_negSucc
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
negSucc : bodd (-(↑(m.succ * n) : ℤ)) = (-[m+1].bodd && bodd (↑n : ℤ))
⊢ (-[m+1] * ofNat n).bodd = (-[m+1].bodd && (ofNat n).bodd)

Tactic:
simp only [ofNat_eq_natCast, ofNat_mul_negSucc, negSucc_mul_ofNat, ofNat_mul_ofNat,
             negSucc_mul_negSucc]

Premises used: Int.negSucc_mul_ofNat, Int.ofNat_mul_negSucc, Int.ofNat_eq_natCast, Int.ofNat_mul_ofNat, Int.negSucc_mul_negSucc
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ bodd (↑(m * n) : ℤ) = (bodd (↑m : ℤ) && bodd (↑n : ℤ))

Tactic:
simp only [negSucc_eq, ← Int.natCast_succ, bodd_neg, bodd_coe, Nat.bodd_mul]

Premises used: Nat.bodd_mul, Int.natCast_succ, Int.negSucc_eq, Int.bodd_neg, Int.bodd_coe
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ bodd (-(↑(m * n.succ) : ℤ)) = (bodd (↑m : ℤ) && -[n+1].bodd)

Tactic:
simp only [negSucc_eq, ← Int.natCast_succ, bodd_neg, bodd_coe, Nat.bodd_mul]

Premises used: Nat.bodd_mul, Int.natCast_succ, Int.negSucc_eq, Int.bodd_neg, Int.bodd_coe
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ bodd (-(↑(m.succ * n) : ℤ)) = (-[m+1].bodd && bodd (↑n : ℤ))

Tactic:
simp only [negSucc_eq, ← Int.natCast_succ, bodd_neg, bodd_coe, Nat.bodd_mul]

Premises used: Nat.bodd_mul, Int.natCast_succ, Int.negSucc_eq, Int.bodd_neg, Int.bodd_coe
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ bodd (↑(m.succ * n.succ) : ℤ) = (-[m+1].bodd && -[n+1].bodd)

Tactic:
simp only [negSucc_eq, ← Int.natCast_succ, bodd_neg, bodd_coe, Nat.bodd_mul]

Premises used: Nat.bodd_mul, Int.natCast_succ, Int.negSucc_eq, Int.bodd_neg, Int.bodd_coe
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℕ
false : Eq (α := ℤ) (bif Bool.false then 1 else 0) (↑(bif Bool.false then 1 else 0) : ℤ)
true : Eq (α := ℤ) (bif Bool.true then 1 else 0) (↑(bif Bool.true then 1 else 0) : ℤ)
⊢ Eq (α := ℤ) (bif bodd (↑n : ℤ) then 1 else 0) (↑(bif bodd (↑n : ℤ) then 1 else 0) : ℤ)

Tactic:
cases bodd n

Premises used: Int.bodd, Nat.cast
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℕ
⊢ Eq (α := ℤ) (bif false then 1 else 0) (↑(bif false then 1 else 0) : ℤ)

Tactic:
rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℕ
⊢ Eq (α := ℤ) (bif true then 1 else 0) (↑(bif true then 1 else 0) : ℤ)

Tactic:
rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℕ
rw : (↑(bif bodd (↑n : ℤ) then 1 else 0) : ℤ) + 2 * div2 (↑n : ℤ) = (↑n : ℤ)
⊢ (bif bodd (↑n : ℤ) then 1 else 0) + 2 * div2 (↑n : ℤ) = (↑n : ℤ)

Tactic:
rw [show (cond (bodd n) 1 0 : ℤ) = (cond (bodd n) 1 0 : ℕ) by cases bodd n <;> rfl]
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℕ
⊢ (↑(bif bodd (↑n : ℤ) then 1 else 0) : ℤ) + 2 * div2 (↑n : ℤ) = (↑n : ℤ)

Tactic:
congr_arg ofNat n.bodd_add_div2

Premises used: Int.ofNat, congr_arg, Int.add, Nat.bodd_add_div2
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℕ
⊢ (↑(bif bodd (↑n : ℤ) then 1 else 0) : ℤ) + 2 * div2 (↑n : ℤ) = (↑n : ℤ)

Tactic:
exact congr_arg ofNat n.bodd_add_div2

Premises used: Int.ofNat, congr_arg, Nat.bodd_add_div2
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℕ
⊢ (bif -[n+1].bodd then 1 else 0) + 2 * -[n+1].div2 = -[n+1]

Tactic:
Eq.trans ?_ (congr_arg negSucc n.bodd_add_div2)

Premises used: congr_arg, Int.negSucc, Nat.bodd_add_div2, Eq.trans
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℕ
refine : (bif -[n+1].bodd then 1 else 0) + 2 * -[n+1].div2 = -[n.bodd.toNat + 2 * n.div2+1]
⊢ (bif -[n+1].bodd then 1 else 0) + 2 * -[n+1].div2 = -[n+1]

Tactic:
refine Eq.trans ?_ (congr_arg negSucc n.bodd_add_div2)

Premises used: congr_arg, Int.negSucc, Nat.bodd_add_div2, Eq.trans
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℕ
false : (bif !Bool.false then 1 else 0) + 2 * -[n+1].div2 = -[Bool.false.toNat + 2 * n.div2+1]
true : (bif !Bool.true then 1 else 0) + 2 * -[n+1].div2 = -[Bool.true.toNat + 2 * n.div2+1]
⊢ (bif !n.bodd then 1 else 0) + 2 * -[n+1].div2 = -[n.bodd.toNat + 2 * n.div2+1]

Tactic:
cases Nat.bodd n

Premises used: Nat.bodd
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℕ
false false₁ : -[2 * n.div2+1] = -[2 * n.div2+1]
⊢ -[2 * n.div2+1] = -[0 + 2 * n.div2+1]

Tactic:
rw [zero_add]

Premises used: zero_add
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℕ
true : 2 * -[n.div2+1] = -[2 * n.div2 + 1+1]
⊢ 0 + 2 * -[n.div2+1] = -[1 + 2 * n.div2+1]

Tactic:
rw [zero_add, add_comm]

Premises used: zero_add, add_comm
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℕ
⊢ 2 * -[n.div2+1] = -[2 * n.div2 + 1+1]

Tactic:
rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
b : Bool
n : ℤ
false : bit Bool.false n = 2 * n + bif Bool.false then 1 else 0
true : bit Bool.true n = 2 * n + bif Bool.true then 1 else 0
⊢ bit b n = 2 * n + bif b then 1 else 0

Tactic:
cases b
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℤ
⊢ bit false n = 2 * n + bif false then 1 else 0

Tactic:
apply (add_zero _).symm

Premises used: add_zero, Eq.symm
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℤ
⊢ bit true n = 2 * n + bif true then 1 else 0

Tactic:
rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℤ
⊢ bit n.bodd n.div2 = n

Tactic:
(bit_val _ _).trans <| (add_comm _ _).trans <| bodd_add_div2 _

Premises used: add_comm, Int.bodd_add_div2, Int.bit_val, Eq.trans
-- Module: Mathlib.Data.Int.Bitwise
Goal:
C : ℤ → Sort u
n : ℤ
h : (b : Bool) → (n : ℤ) → C (bit b n)
rw : C (bit n.bodd n.div2)
⊢ C n

Tactic:
rw [← bit_decomp n]

Premises used: Int.bit_decomp
-- Module: Mathlib.Data.Int.Bitwise
Goal:
C : ℤ → Sort u
n : ℤ
h : (b : Bool) → (n : ℤ) → C (bit b n)
⊢ C (bit n.bodd n.div2)

Tactic:
apply h
-- Module: Mathlib.Data.Int.Bitwise
Goal:
⊢ bit false 0 = 0

Tactic:
rfl

Premises used: cond, Int.mul, Int.bit, rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
b : Bool
n : ℕ
rw : (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + bif b then 1 else 0) = (↑(2 * n + b.toNat) : ℤ)
⊢ bit b (↑n : ℤ) = (↑(Nat.bit b n) : ℤ)

Tactic:
rw [bit_val, Nat.bit_val]

Premises used: Nat.bit_val, Int.bit_val
-- Module: Mathlib.Data.Int.Bitwise
Goal:
b : Bool
n : ℕ
false : (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + bif Bool.false then 1 else 0) = (↑(2 * n + Bool.false.toNat) : ℤ)
true : (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + bif Bool.true then 1 else 0) = (↑(2 * n + Bool.true.toNat) : ℤ)
⊢ (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + bif b then 1 else 0) = (↑(2 * n + b.toNat) : ℤ)

Tactic:
cases b
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℕ
⊢ (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + bif false then 1 else 0) = (↑(2 * n + false.toNat) : ℤ)

Tactic:
rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℕ
⊢ (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + bif true then 1 else 0) = (↑(2 * n + true.toNat) : ℤ)

Tactic:
rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
b : Bool
n : ℕ
rw : (2 * -[n+1] + bif b then 1 else 0) = -[2 * n + (!b).toNat+1]
⊢ bit b -[n+1] = -[Nat.bit (!b) n+1]

Tactic:
rw [bit_val, Nat.bit_val]

Premises used: Nat.bit_val, Int.bit_val
-- Module: Mathlib.Data.Int.Bitwise
Goal:
b : Bool
n : ℕ
false : (2 * -[n+1] + bif Bool.false then 1 else 0) = -[2 * n + (!Bool.false).toNat+1]
true : (2 * -[n+1] + bif Bool.true then 1 else 0) = -[2 * n + (!Bool.true).toNat+1]
⊢ (2 * -[n+1] + bif b then 1 else 0) = -[2 * n + (!b).toNat+1]

Tactic:
cases b
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℕ
⊢ (2 * -[n+1] + bif false then 1 else 0) = -[2 * n + (!false).toNat+1]

Tactic:
rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℕ
⊢ (2 * -[n+1] + bif true then 1 else 0) = -[2 * n + (!true).toNat+1]

Tactic:
rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
b : Bool
n : ℤ
rw : (2 * n + bif b then 1 else 0).bodd = b
⊢ (bit b n).bodd = b

Tactic:
rw [bit_val]

Premises used: Int.bit_val
-- Module: Mathlib.Data.Int.Bitwise
Goal:
b : Bool
n : ℤ
false : (2 * n + bif Bool.false then 1 else 0).bodd = Bool.false
true : (2 * n + bif Bool.true then 1 else 0).bodd = Bool.true
⊢ (2 * n + bif b then 1 else 0).bodd = b

Tactic:
cases b
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℤ
false false₁ : (2 * n + bif Bool.false then 1 else 0).bodd = Bool.false
⊢ (2 * n + bif Bool.false then 1 else 0).bodd = Bool.false

Tactic:
cases bodd n

Premises used: Int.bodd
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℤ
true true₁ : (2 * n + bif Bool.true then 1 else 0).bodd = Bool.true
⊢ (2 * n + bif Bool.true then 1 else 0).bodd = Bool.true

Tactic:
cases bodd n

Premises used: Int.bodd
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℤ
⊢ bodd 2 = false

Tactic:
rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℤ
⊢ (2 * n + bif false then 1 else 0).bodd = false

Tactic:
simp [(show bodd 2 = false by rfl)]
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℤ
⊢ (2 * n + bif true then 1 else 0).bodd = true

Tactic:
simp [(show bodd 2 = false by rfl)]
-- Module: Mathlib.Data.Int.Bitwise
Goal:
b : Bool
n : ℕ
rw : testBit (↑(Nat.bit b n) : ℤ) 0 = b
⊢ (bit b (↑n : ℤ)).testBit 0 = b

Tactic:
rw [bit_coe_nat]

Premises used: Int.bit_coe_nat
-- Module: Mathlib.Data.Int.Bitwise
Goal:
b : Bool
n : ℕ
⊢ testBit (↑(Nat.bit b n) : ℤ) 0 = b

Tactic:
apply Nat.testBit_bit_zero

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

Tactic:
rw [bit_negSucc]

Premises used: Int.bit_negSucc
-- Module: Mathlib.Data.Int.Bitwise
Goal:
b : Bool
n : ℕ
rw : (!!b) = b
rw₁ rw₂ : b = b
⊢ (!(Nat.bit (!b) n).testBit 0) = b

Tactic:
rw [Nat.testBit_bit_zero, Bool.not_not]

Premises used: Bool.not_not, Nat.testBit_bit_zero
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m : ℕ
b : Bool
n : ℕ
rw : testBit (↑(Nat.bit b n) : ℤ) m.succ = testBit (↑n : ℤ) m
⊢ (bit b (↑n : ℤ)).testBit m.succ = testBit (↑n : ℤ) m

Tactic:
rw [bit_coe_nat]

Premises used: Int.bit_coe_nat
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m : ℕ
b : Bool
n : ℕ
⊢ testBit (↑(Nat.bit b n) : ℤ) m.succ = testBit (↑n : ℤ) m

Tactic:
apply Nat.testBit_bit_succ

Premises used: Nat.testBit_bit_succ
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m : ℕ
b : Bool
n : ℕ
dsimp :
  (match (motive := ℤ → ℕ → Bool) bit b -[n+1], m.succ with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    !n.testBit m
⊢ (bit b -[n+1]).testBit m.succ = -[n+1].testBit m

Tactic:
dsimp only [testBit]

Premises used: Int.testBit
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m : ℕ
b : Bool
n : ℕ
simp : (!(Nat.bit (!b) n).testBit m.succ) = !n.testBit m
⊢ (match (motive := ℤ → ℕ → Bool) bit b -[n+1], m.succ with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    !n.testBit m

Tactic:
simp only [bit_negSucc]

Premises used: Int.bit_negSucc
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m : ℕ
b : Bool
n : ℕ
false : (!(Nat.bit (!Bool.false) n).testBit m.succ) = !n.testBit m
true : (!(Nat.bit (!Bool.true) n).testBit m.succ) = !n.testBit m
⊢ (!(Nat.bit (!b) n).testBit m.succ) = !n.testBit m

Tactic:
cases b
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ (!(Nat.bit (!false) n).testBit m.succ) = !n.testBit m

Tactic:
simp only [Bool.not_false, Bool.not_true, Nat.testBit_bit_succ]

Premises used: Bool.not_false, Nat.testBit_bit_succ, Bool.not_true
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ (!(Nat.bit (!true) n).testBit m.succ) = !n.testBit m

Tactic:
simp only [Bool.not_false, Bool.not_true, Nat.testBit_bit_succ]

Premises used: Bool.not_false, Nat.testBit_bit_succ, Bool.not_true
-- Module: Mathlib.Data.Int.Bitwise
Goal:
h : ∀ (m n : ℤ), bitwise or m n = m.lor n
⊢ bitwise or = lor

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

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

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

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

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

Tactic:
{rfl}
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ bitwise or (ofNat m) (ofNat n) = (ofNat m).lor (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 (fun (a b : Bool) ↦ a && !b) n m
⊢ bitwise or (ofNat m) -[n+1] = (ofNat m).lor -[n+1]

Tactic:
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_true, lor, Nat.ldiff,
      negSucc.injEq, Bool.true_or]

Premises used: Int.natBitwise, Bool.or_true, Bool.not_false, Int.bitwise, cond_true, Int.lor, Int.negSucc.injEq, Nat.ldiff, Bool.true_or
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
h : Nat.bitwise (fun (x y : Bool) ↦ !(!x || y)) m n = Nat.bitwise (fun (a b : Bool) ↦ a && !b) m n
⊢ bitwise or -[m+1] (ofNat n) = -[m+1].lor (ofNat n)

Tactic:
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_true, lor, Nat.ldiff,
      negSucc.injEq, Bool.true_or]

Premises used: Int.natBitwise, Bool.or_true, Bool.not_false, Int.bitwise, cond_true, Int.lor, Int.negSucc.injEq, Nat.ldiff, Bool.true_or
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
h : Nat.bitwise (fun (x y : Bool) ↦ !(!x || !y)) m n = m &&& n
⊢ bitwise or -[m+1] -[n+1] = -[m+1].lor -[n+1]

Tactic:
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_true, lor, Nat.ldiff,
      negSucc.injEq, Bool.true_or]

Premises used: Int.natBitwise, Bool.or_true, Bool.not_false, Int.bitwise, cond_true, Int.lor, Int.negSucc.injEq, Nat.ldiff, Bool.true_or
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
h : Nat.bitwise (fun (y x : Bool) ↦ !(x || !y)) n m = Nat.bitwise (fun (a b : Bool) ↦ a && !b) n m
⊢ 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
⊢ 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:
m n : ℕ
⊢ Nat.bitwise (fun (x y : Bool) ↦ !(!x || y)) m n = Nat.bitwise (fun (a b : Bool) ↦ a && !b) m n

Tactic:
simp
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
h : (fun (x y : Bool) ↦ !(!x || !y)) = and
⊢ 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:
h : ∀ (m n : ℤ), bitwise and m n = m.land n
⊢ bitwise and = land

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

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

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

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

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

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

Tactic:
try {rfl}
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ bitwise and (ofNat m) -[n+1] = (ofNat m).land -[n+1]

Tactic:
rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ bitwise and (ofNat m) -[n+1] = (ofNat m).land -[n+1]

Tactic:
{rfl}
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ bitwise and (ofNat m) -[n+1] = (ofNat m).land -[n+1]

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

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
⊢ (↑(Nat.bitwise (fun (y x : Bool) ↦ !x && y) n m) : ℤ) = -[m+1].land (ofNat n)

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