awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℤ
⊢ (-n).bodd = n.bodd
have ofNat : ∀ (a : ℕ), (-ofNat a).bodd = (ofNat a).bodd
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℤ
ofNat : ∀ (a : ℕ), (-Int.ofNat a).bodd = (Int.ofNat a).bodd
⊢ (-n).bodd = n.bodd
have negSucc : ∀ (a : ℕ), (- -[a+1]).bodd = -[a+1].bodd
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
a : ℕ
⊢ (-ofNat a).bodd = (ofNat a).bodd
have ofNat : a.bodd = (ofNat a).bodd
Tactic: simp only [← negOfNat_eq, bodd_negOfNat, neg_negSucc]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℤ
⊢ (m + n).bodd = (m.bodd ^^ n.bodd)
have ofNat : ∀ (m : ℕ), (ofNat m + n).bodd = ((ofNat m).bodd ^^ n.bodd)
Tactic: rcases m with m | m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℤ
ofNat : ∀ (m : ℕ), (Int.ofNat m + n).bodd = ((Int.ofNat m).bodd ^^ n.bodd)
⊢ (m + n).bodd = (m.bodd ^^ n.bodd)
have negSucc : ∀ (m : ℕ), (-[m+1] + n).bodd = (-[m+1].bodd ^^ n.bodd)
Tactic: rcases m with m | m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℤ
m : ℕ
⊢ (ofNat m + n).bodd = ((ofNat m).bodd ^^ n.bodd)
have ofNat : ∀ (n : ℕ), (ofNat m + ofNat n).bodd = ((ofNat m).bodd ^^ (ofNat n).bodd)
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℤ
m : ℕ
ofNat : ∀ (n : ℕ), (Int.ofNat m + Int.ofNat n).bodd = ((Int.ofNat m).bodd ^^ (Int.ofNat n).bodd)
⊢ (Int.ofNat m + n).bodd = ((Int.ofNat m).bodd ^^ n.bodd)
have ofNat₁ : ∀ (n : ℕ), (Int.ofNat m + -[n+1]).bodd = ((Int.ofNat m).bodd ^^ -[n+1].bodd)
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℤ
m : ℕ
⊢ (-[m+1] + n).bodd = (-[m+1].bodd ^^ n.bodd)
have negSucc : ∀ (n : ℕ), (-[m+1] + ofNat n).bodd = (-[m+1].bodd ^^ (ofNat n).bodd)
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℤ
m : ℕ
negSucc : ∀ (n : ℕ), (-[m+1] + ofNat n).bodd = (-[m+1].bodd ^^ (ofNat n).bodd)
⊢ (-[m+1] + n).bodd = (-[m+1].bodd ^^ n.bodd)
have negSucc₁ : ∀ (n : ℕ), (-[m+1] + -[n+1]).bodd = (-[m+1].bodd ^^ -[n+1].bodd)
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
⊢ (ofNat m + -[n+1]).bodd = ((ofNat m).bodd ^^ -[n+1].bodd)
have ofNat : (m.bodd ^^ n.succ.bodd) = (bodd (↑m : ℤ) ^^ -[n+1].bodd)
Tactic: simp only [ofNat_eq_natCast, ofNat_add_negSucc, negSucc_add_ofNat,
             negSucc_add_negSucc, bodd_subNatNat, ← Nat.cast_add]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
⊢ (-[m+1] + ofNat n).bodd = (-[m+1].bodd ^^ (ofNat n).bodd)
have negSucc : (n.bodd ^^ m.succ.bodd) = (-[m+1].bodd ^^ bodd (↑n : ℤ))
Tactic: simp only [ofNat_eq_natCast, ofNat_add_negSucc, negSucc_add_ofNat,
             negSucc_add_negSucc, bodd_subNatNat, ← Nat.cast_add]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℤ
⊢ (m * n).bodd = (m.bodd && n.bodd)
have ofNat : ∀ (m : ℕ), (ofNat m * n).bodd = ((ofNat m).bodd && n.bodd)
Tactic: rcases m with m | m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℤ
ofNat : ∀ (m : ℕ), (Int.ofNat m * n).bodd = ((Int.ofNat m).bodd && n.bodd)
⊢ (m * n).bodd = (m.bodd && n.bodd)
have negSucc : ∀ (m : ℕ), (-[m+1] * n).bodd = (-[m+1].bodd && n.bodd)
Tactic: rcases m with m | m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℤ
m : ℕ
⊢ (ofNat m * n).bodd = ((ofNat m).bodd && n.bodd)
have ofNat : ∀ (n : ℕ), (ofNat m * ofNat n).bodd = ((ofNat m).bodd && (ofNat n).bodd)
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℤ
m : ℕ
ofNat : ∀ (n : ℕ), (Int.ofNat m * Int.ofNat n).bodd = ((Int.ofNat m).bodd && (Int.ofNat n).bodd)
⊢ (Int.ofNat m * n).bodd = ((Int.ofNat m).bodd && n.bodd)
have ofNat₁ : ∀ (n : ℕ), (Int.ofNat m * -[n+1]).bodd = ((Int.ofNat m).bodd && -[n+1].bodd)
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℤ
m : ℕ
⊢ (-[m+1] * n).bodd = (-[m+1].bodd && n.bodd)
have negSucc : ∀ (n : ℕ), (-[m+1] * ofNat n).bodd = (-[m+1].bodd && (ofNat n).bodd)
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℤ
m : ℕ
negSucc : ∀ (n : ℕ), (-[m+1] * ofNat n).bodd = (-[m+1].bodd && (ofNat n).bodd)
⊢ (-[m+1] * n).bodd = (-[m+1].bodd && n.bodd)
have negSucc₁ : ∀ (n : ℕ), (-[m+1] * -[n+1]).bodd = (-[m+1].bodd && -[n+1].bodd)
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
⊢ (ofNat m * -[n+1]).bodd = ((ofNat m).bodd && -[n+1].bodd)
have ofNat : bodd (-(↑(m * n.succ) : ℤ)) = (bodd (↑m : ℤ) && -[n+1].bodd)
Tactic: simp only [ofNat_eq_natCast, ofNat_mul_negSucc, negSucc_mul_ofNat, ofNat_mul_ofNat,
             negSucc_mul_negSucc]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
⊢ (-[m+1] * ofNat n).bodd = (-[m+1].bodd && (ofNat n).bodd)
have negSucc : bodd (-(↑(m.succ * n) : ℤ)) = (-[m+1].bodd && bodd (↑n : ℤ))
Tactic: simp only [ofNat_eq_natCast, ofNat_mul_negSucc, negSucc_mul_ofNat, ofNat_mul_ofNat,
             negSucc_mul_negSucc]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℕ
⊢ Eq (α := ℤ) (bif bodd (↑n : ℤ) then 1 else 0) (↑(bif bodd (↑n : ℤ) then 1 else 0) : ℤ)
have false : Eq (α := ℤ) (bif false then 1 else 0) (↑(bif false then 1 else 0) : ℤ)
Tactic: cases bodd n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℕ
false : Eq (α := ℤ) (bif Bool.false then 1 else 0) (↑(bif Bool.false then 1 else 0) : ℤ)
⊢ Eq (α := ℤ) (bif bodd (↑n : ℤ) then 1 else 0) (↑(bif bodd (↑n : ℤ) then 1 else 0) : ℤ)
have true : Eq (α := ℤ) (bif true then 1 else 0) (↑(bif true then 1 else 0) : ℤ)
Tactic: cases bodd n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℕ
⊢ (bif bodd (↑n : ℤ) then 1 else 0) + 2 * div2 (↑n : ℤ) = (↑n : ℤ)
have rw : (↑(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]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℕ
⊢ (bif -[n+1].bodd then 1 else 0) + 2 * -[n+1].div2 = -[n+1]
have refine : (bif -[n+1].bodd then 1 else 0) + 2 * -[n+1].div2 = -[n.bodd.toNat + 2 * n.div2+1]
Tactic: refine Eq.trans ?_ (congr_arg negSucc n.bodd_add_div2)
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℕ
⊢ (bif !n.bodd then 1 else 0) + 2 * -[n+1].div2 = -[n.bodd.toNat + 2 * n.div2+1]
have false : (bif !false then 1 else 0) + 2 * -[n+1].div2 = -[false.toNat + 2 * n.div2+1]
Tactic: cases Nat.bodd n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℕ
false : (bif !Bool.false then 1 else 0) + 2 * -[n+1].div2 = -[Bool.false.toNat + 2 * n.div2+1]
⊢ (bif !n.bodd then 1 else 0) + 2 * -[n+1].div2 = -[n.bodd.toNat + 2 * n.div2+1]
have true : (bif !true then 1 else 0) + 2 * -[n+1].div2 = -[true.toNat + 2 * n.div2+1]
Tactic: cases Nat.bodd n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℕ
⊢ -[2 * n.div2+1] = -[0 + 2 * n.div2+1]
have false : -[2 * n.div2+1] = -[2 * n.div2+1]
Tactic: rw [zero_add]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℕ
⊢ 0 + 2 * -[n.div2+1] = -[1 + 2 * n.div2+1]
have true : 2 * -[n.div2+1] = -[2 * n.div2 + 1+1]
Tactic: rw [zero_add, add_comm]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
b : Bool
n : ℤ
⊢ bit b n = 2 * n + bif b then 1 else 0
have false : bit false n = 2 * n + bif false then 1 else 0
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
b : Bool
n : ℤ
false : bit Bool.false n = 2 * n + bif Bool.false then 1 else 0
⊢ bit b n = 2 * n + bif b then 1 else 0
have true : bit true n = 2 * n + bif true then 1 else 0
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
C : ℤ → Sort u
n : ℤ
h : (b : Bool) → (n : ℤ) → C (bit b n)
⊢ C n
have rw : C (bit n.bodd n.div2)
Tactic: rw [← bit_decomp n]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
b : Bool
n : ℕ
⊢ bit b (↑n : ℤ) = (↑(Nat.bit b n) : ℤ)
have rw : (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + bif b then 1 else 0) = (↑(2 * n + b.toNat) : ℤ)
Tactic: rw [bit_val, Nat.bit_val]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
b : Bool
n : ℕ
⊢ (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + bif b then 1 else 0) = (↑(2 * n + b.toNat) : ℤ)
have false : (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + bif false then 1 else 0) = (↑(2 * n + false.toNat) : ℤ)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
b : Bool
n : ℕ
false : (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + bif Bool.false then 1 else 0) = (↑(2 * n + Bool.false.toNat) : ℤ)
⊢ (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + bif b then 1 else 0) = (↑(2 * n + b.toNat) : ℤ)
have true : (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + bif true then 1 else 0) = (↑(2 * n + true.toNat) : ℤ)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
b : Bool
n : ℕ
⊢ bit b -[n+1] = -[Nat.bit (!b) n+1]
have rw : (2 * -[n+1] + bif b then 1 else 0) = -[2 * n + (!b).toNat+1]
Tactic: rw [bit_val, Nat.bit_val]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
b : Bool
n : ℕ
⊢ (2 * -[n+1] + bif b then 1 else 0) = -[2 * n + (!b).toNat+1]
have false : (2 * -[n+1] + bif false then 1 else 0) = -[2 * n + (!false).toNat+1]
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
b : Bool
n : ℕ
false : (2 * -[n+1] + bif Bool.false then 1 else 0) = -[2 * n + (!Bool.false).toNat+1]
⊢ (2 * -[n+1] + bif b then 1 else 0) = -[2 * n + (!b).toNat+1]
have true : (2 * -[n+1] + bif true then 1 else 0) = -[2 * n + (!true).toNat+1]
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
b : Bool
n : ℤ
⊢ (bit b n).bodd = b
have rw : (2 * n + bif b then 1 else 0).bodd = b
Tactic: rw [bit_val]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
b : Bool
n : ℤ
⊢ (2 * n + bif b then 1 else 0).bodd = b
have false : (2 * n + bif false then 1 else 0).bodd = false
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
b : Bool
n : ℤ
false : (2 * n + bif Bool.false then 1 else 0).bodd = Bool.false
⊢ (2 * n + bif b then 1 else 0).bodd = b
have true : (2 * n + bif true then 1 else 0).bodd = true
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
b : Bool
n : ℕ
⊢ (bit b (↑n : ℤ)).testBit 0 = b
have rw : testBit (↑(Nat.bit b n) : ℤ) 0 = b
Tactic: rw [bit_coe_nat]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
b : Bool
n : ℕ
⊢ (bit b -[n+1]).testBit 0 = b
have rw : -[Nat.bit (!b) n+1].testBit 0 = b
Tactic: rw [bit_negSucc]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
b : Bool
n : ℕ
⊢ (!(Nat.bit (!b) n).testBit 0) = b
have rw : (!!b) = b
Tactic: rw [Nat.testBit_bit_zero, Bool.not_not]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
b : Bool
n : ℕ
rw : (!!b) = b
⊢ (!(Nat.bit (!b) n).testBit 0) = b
have rw₁ : b = b
Tactic: rw [Nat.testBit_bit_zero, Bool.not_not]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m : ℕ
b : Bool
n : ℕ
⊢ (bit b (↑n : ℤ)).testBit m.succ = testBit (↑n : ℤ) m
have rw : testBit (↑(Nat.bit b n) : ℤ) m.succ = testBit (↑n : ℤ) m
Tactic: rw [bit_coe_nat]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m : ℕ
b : Bool
n : ℕ
⊢ (bit b -[n+1]).testBit m.succ = -[n+1].testBit m
have 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
Tactic: dsimp only [testBit]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m : ℕ
b : Bool
n : ℕ
⊢ (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
have simp : (!(Nat.bit (!b) n).testBit m.succ) = !n.testBit m
Tactic: simp only [bit_negSucc]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m : ℕ
b : Bool
n : ℕ
⊢ (!(Nat.bit (!b) n).testBit m.succ) = !n.testBit m
have false : (!(Nat.bit (!false) n).testBit m.succ) = !n.testBit m
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m : ℕ
b : Bool
n : ℕ
false : (!(Nat.bit (!Bool.false) n).testBit m.succ) = !n.testBit m
⊢ (!(Nat.bit (!b) n).testBit m.succ) = !n.testBit m
have true : (!(Nat.bit (!true) n).testBit m.succ) = !n.testBit m
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
⊢ bitwise or = lor
have h : ∀ (m n : ℤ), bitwise or m n = m.lor n
Tactic: funext m n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℤ
⊢ bitwise or m n = m.lor n
have h : ∀ (m : ℕ), bitwise or (ofNat m) n = (ofNat m).lor n
Tactic: rcases m with m | m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℤ
h : ∀ (m : ℕ), bitwise or (ofNat m) n = (ofNat m).lor n
⊢ bitwise or m n = m.lor n
have h₁ : ∀ (m : ℕ), bitwise or -[m+1] n = -[m+1].lor n
Tactic: rcases m with m | m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℤ
m : ℕ
⊢ bitwise or (ofNat m) n = (ofNat m).lor n
have h : ∀ (n : ℕ), bitwise or (ofNat m) (ofNat n) = (ofNat m).lor (ofNat n)
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℤ
m : ℕ
h : ∀ (n : ℕ), bitwise or (ofNat m) (ofNat n) = (ofNat m).lor (ofNat n)
⊢ bitwise or (ofNat m) n = (ofNat m).lor n
have h₁ : ∀ (n : ℕ), bitwise or (ofNat m) -[n+1] = (ofNat m).lor -[n+1]
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℤ
m : ℕ
⊢ bitwise or -[m+1] n = -[m+1].lor n
have h : ∀ (n : ℕ), bitwise or -[m+1] (ofNat n) = -[m+1].lor (ofNat n)
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℤ
m : ℕ
h : ∀ (n : ℕ), bitwise or -[m+1] (ofNat n) = -[m+1].lor (ofNat n)
⊢ bitwise or -[m+1] n = -[m+1].lor n
have h₁ : ∀ (n : ℕ), bitwise or -[m+1] -[n+1] = -[m+1].lor -[n+1]
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
⊢ bitwise or (ofNat m) -[n+1] = (ofNat m).lor -[n+1]
have h : Nat.bitwise (fun (x y : Bool) ↦ !(x || !y)) m n = Nat.bitwise (fun (a b : Bool) ↦ a && !b) n m
Tactic: simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_true, lor, Nat.ldiff,
      negSucc.injEq, Bool.true_or]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
⊢ bitwise or -[m+1] (ofNat n) = -[m+1].lor (ofNat n)
have h : Nat.bitwise (fun (x y : Bool) ↦ !(!x || y)) m n = Nat.bitwise (fun (a b : Bool) ↦ a && !b) m n
Tactic: simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_true, lor, Nat.ldiff,
      negSucc.injEq, Bool.true_or]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
⊢ bitwise or -[m+1] -[n+1] = -[m+1].lor -[n+1]
have h : Nat.bitwise (fun (x y : Bool) ↦ !(!x || !y)) m n = m &&& n
Tactic: simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_true, lor, Nat.ldiff,
      negSucc.injEq, Bool.true_or]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
⊢ Nat.bitwise (fun (x y : Bool) ↦ !(x || !y)) m n = Nat.bitwise (fun (a b : Bool) ↦ a && !b) n m
have h : Nat.bitwise (fun (y x : Bool) ↦ !(x || !y)) n m = Nat.bitwise (fun (a b : Bool) ↦ a && !b) n m
Tactic: rw [Nat.bitwise_swap, Function.swap]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
⊢ Nat.bitwise (fun (y x : Bool) ↦ !(x || !y)) n m = Nat.bitwise (fun (a b : Bool) ↦ a && !b) n m
have h : Eq (α := Bool → Bool → Bool) (fun (y x : Bool) ↦ !(x || !y)) fun (a b : Bool) ↦ a && !b
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
⊢ Eq (α := Bool → Bool → Bool) (fun (y x : Bool) ↦ !(x || !y)) fun (a b : Bool) ↦ a && !b
have h : ∀ (x y : Bool), (!(y || !x)) = (x && !y)
Tactic: funext x y
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
x y : Bool
⊢ (!(y || !x)) = (x && !y)
have h : (!(y || !false)) = (false && !y)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
x y : Bool
h : (!(y || !false)) = (false && !y)
⊢ (!(y || !x)) = (x && !y)
have h₁ : (!(y || !true)) = (true && !y)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
y : Bool
⊢ (!(y || !false)) = (false && !y)
have h : (!(false || !false)) = (false && !false)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
y : Bool
h : (!(false || !false)) = (false && !false)
⊢ (!(y || !false)) = (false && !y)
have h₁ : (!(true || !false)) = (false && !true)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
y : Bool
⊢ (!(y || !true)) = (true && !y)
have h : (!(false || !true)) = (true && !false)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
y : Bool
h : (!(false || !true)) = (true && !false)
⊢ (!(y || !true)) = (true && !y)
have h₁ : (!(true || !true)) = (true && !true)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
⊢ Nat.bitwise (fun (x y : Bool) ↦ !(!x || !y)) m n = m &&& n
have h : (fun (x y : Bool) ↦ !(!x || !y)) = and
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
⊢ bitwise and = land
have h : ∀ (m n : ℤ), bitwise and m n = m.land n
Tactic: funext m n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℤ
⊢ bitwise and m n = m.land n
have h : ∀ (m : ℕ), bitwise and (ofNat m) n = (ofNat m).land n
Tactic: rcases m with m | m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℤ
h : ∀ (m : ℕ), bitwise and (ofNat m) n = (ofNat m).land n
⊢ bitwise and m n = m.land n
have h₁ : ∀ (m : ℕ), bitwise and -[m+1] n = -[m+1].land n
Tactic: rcases m with m | m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℤ
m : ℕ
⊢ bitwise and (ofNat m) n = (ofNat m).land n
have h : ∀ (n : ℕ), bitwise and (ofNat m) (ofNat n) = (ofNat m).land (ofNat n)
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℤ
m : ℕ
h : ∀ (n : ℕ), bitwise and (ofNat m) (ofNat n) = (ofNat m).land (ofNat n)
⊢ bitwise and (ofNat m) n = (ofNat m).land n
have h₁ : ∀ (n : ℕ), bitwise and (ofNat m) -[n+1] = (ofNat m).land -[n+1]
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℤ
m : ℕ
⊢ bitwise and -[m+1] n = -[m+1].land n
have h : ∀ (n : ℕ), bitwise and -[m+1] (ofNat n) = -[m+1].land (ofNat n)
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℤ
m : ℕ
h : ∀ (n : ℕ), bitwise and -[m+1] (ofNat n) = -[m+1].land (ofNat n)
⊢ bitwise and -[m+1] n = -[m+1].land n
have h₁ : ∀ (n : ℕ), bitwise and -[m+1] -[n+1] = -[m+1].land -[n+1]
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
⊢ (↑(Nat.bitwise (fun (x y : Bool) ↦ !x && y) m n) : ℤ) = -[m+1].land (ofNat n)
have h : (↑(Nat.bitwise (fun (y x : Bool) ↦ !x && y) n m) : ℤ) = -[m+1].land (ofNat n)
Tactic: rw [Nat.bitwise_swap, Function.swap]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
⊢ (↑(Nat.bitwise (fun (y x : Bool) ↦ !x && y) n m) : ℤ) = -[m+1].land (ofNat n)
have h : Eq (α := Bool → Bool → Bool) (fun (y x : Bool) ↦ !x && y) fun (a b : Bool) ↦ a && !b
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
⊢ Eq (α := Bool → Bool → Bool) (fun (y x : Bool) ↦ !x && y) fun (a b : Bool) ↦ a && !b
have h : ∀ (x y : Bool), (!y && x) = (x && !y)
Tactic: funext x y
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
x y : Bool
⊢ (!y && x) = (x && !y)
have h : (!y && false) = (false && !y)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
x y : Bool
h : (!y && false) = (false && !y)
⊢ (!y && x) = (x && !y)
have h₁ : (!y && true) = (true && !y)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
y : Bool
⊢ (!y && false) = (false && !y)
have h : (!false && false) = (false && !false)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
y : Bool
h : (!false && false) = (false && !false)
⊢ (!y && false) = (false && !y)
have h₁ : (!true && false) = (false && !true)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
y : Bool
⊢ (!y && true) = (true && !y)
have h : (!false && true) = (true && !false)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
y : Bool
h : (!false && true) = (true && !false)
⊢ (!y && true) = (true && !y)
have h₁ : (!true && true) = (true && !true)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
⊢ -[Nat.bitwise (fun (x y : Bool) ↦ !(!x && !y)) m n+1] = -[m+1].land -[n+1]
have h : (fun (x y : Bool) ↦ !(!x && !y)) = or
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
⊢ (bitwise fun (a b : Bool) ↦ a && !b) = ldiff
have h : ∀ (m n : ℤ), bitwise (fun (a b : Bool) ↦ a && !b) m n = m.ldiff n
Tactic: funext m n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℤ
⊢ bitwise (fun (a b : Bool) ↦ a && !b) m n = m.ldiff n
have h : ∀ (m : ℕ), bitwise (fun (a b : Bool) ↦ a && !b) (ofNat m) n = (ofNat m).ldiff n
Tactic: rcases m with m | m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℤ
h : ∀ (m : ℕ), bitwise (fun (a b : Bool) ↦ a && !b) (ofNat m) n = (ofNat m).ldiff n
⊢ bitwise (fun (a b : Bool) ↦ a && !b) m n = m.ldiff n
have h₁ : ∀ (m : ℕ), bitwise (fun (a b : Bool) ↦ a && !b) -[m+1] n = -[m+1].ldiff n
Tactic: rcases m with m | m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℤ
m : ℕ
⊢ bitwise (fun (a b : Bool) ↦ a && !b) (ofNat m) n = (ofNat m).ldiff n
have h : ∀ (n : ℕ), bitwise (fun (a b : Bool) ↦ a && !b) (ofNat m) (ofNat n) = (ofNat m).ldiff (ofNat n)
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℤ
m : ℕ
h : ∀ (n : ℕ), bitwise (fun (a b : Bool) ↦ a && !b) (ofNat m) (ofNat n) = (ofNat m).ldiff (ofNat n)
⊢ bitwise (fun (a b : Bool) ↦ a && !b) (ofNat m) n = (ofNat m).ldiff n
have h₁ : ∀ (n : ℕ), bitwise (fun (a b : Bool) ↦ a && !b) (ofNat m) -[n+1] = (ofNat m).ldiff -[n+1]
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℤ
m : ℕ
⊢ bitwise (fun (a b : Bool) ↦ a && !b) -[m+1] n = -[m+1].ldiff n
have h : ∀ (n : ℕ), bitwise (fun (a b : Bool) ↦ a && !b) -[m+1] (ofNat n) = -[m+1].ldiff (ofNat n)
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℤ
m : ℕ
h : ∀ (n : ℕ), bitwise (fun (a b : Bool) ↦ a && !b) -[m+1] (ofNat n) = -[m+1].ldiff (ofNat n)
⊢ bitwise (fun (a b : Bool) ↦ a && !b) -[m+1] n = -[m+1].ldiff n
have h₁ : ∀ (n : ℕ), bitwise (fun (a b : Bool) ↦ a && !b) -[m+1] -[n+1] = -[m+1].ldiff -[n+1]
Tactic: rcases n with n | n
Cleared hypotheses: n