awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
⊢ bitwise (fun (a b : Bool) ↦ a && !b) -[m+1] (ofNat n) = -[m+1].ldiff (ofNat n)
have h : Nat.bitwise (fun (x y : Bool) ↦ !(!x && !y)) m n = m ||| 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]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
⊢ Eq (α := ℤ) (↑(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:
m n : ℕ
⊢ Nat.bitwise (fun (x y : Bool) ↦ !(!x && !y)) m n = m ||| n
have h : (fun (x y : Bool) ↦ !(!x && !y)) = or
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
⊢ Eq (α := ℤ) (↑(Nat.bitwise (fun (x y : Bool) ↦ !x && !!y) m n) : ℤ)
    (↑(Nat.bitwise (fun (a b : Bool) ↦ a && !b) n m) : ℤ)
have h : Eq (α := ℤ) (↑(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 : ℕ
⊢ Eq (α := ℤ) (↑(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:
⊢ bitwise xor = Int.xor
have h : ∀ (m n : ℤ), bitwise xor m n = m.xor n
Tactic: funext m n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℤ
⊢ bitwise xor m n = m.xor n
have h : ∀ (m : ℕ), bitwise xor (ofNat m) n = (ofNat m).xor 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 xor (ofNat m) n = (ofNat m).xor n
⊢ bitwise xor m n = m.xor n
have h₁ : ∀ (m : ℕ), bitwise xor -[m+1] n = -[m+1].xor n
Tactic: rcases m with m | m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n : ℤ
m : ℕ
⊢ bitwise xor (ofNat m) n = (ofNat m).xor n
have h : ∀ (n : ℕ), bitwise xor (ofNat m) (ofNat n) = (ofNat m).xor (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 xor (ofNat m) (ofNat n) = (ofNat m).xor (ofNat n)
⊢ bitwise xor (ofNat m) n = (ofNat m).xor n
have h₁ : ∀ (n : ℕ), bitwise xor (ofNat m) -[n+1] = (ofNat m).xor -[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 xor -[m+1] n = -[m+1].xor n
have h : ∀ (n : ℕ), bitwise xor -[m+1] (ofNat n) = -[m+1].xor (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 xor -[m+1] (ofNat n) = -[m+1].xor (ofNat n)
⊢ bitwise xor -[m+1] n = -[m+1].xor n
have h₁ : ∀ (n : ℕ), bitwise xor -[m+1] -[n+1] = -[m+1].xor -[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 xor (ofNat m) -[n+1] = (ofNat m).xor -[n+1]
have h : Nat.bitwise (fun (x y : Bool) ↦ !(x ^^ !y)) m n = Nat.bitwise xor m 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]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
⊢ bitwise xor -[m+1] (ofNat n) = -[m+1].xor (ofNat n)
have h : Nat.bitwise (fun (x y : Bool) ↦ !(!x ^^ y)) m n = Nat.bitwise xor m 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]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
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)
have ofNat : ∀ (m : ℕ), bitwise f (bit a (ofNat m)) (bit b n) = bit (f a b) (bitwise f (ofNat m) n)
Tactic: rcases m with m | m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
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)
⊢ bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n)
have negSucc : ∀ (m : ℕ), bitwise f (bit a -[m+1]) (bit b n) = bit (f a b) (bitwise f -[m+1] n)
Tactic: rcases m with m | m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
a b : Bool
n : ℤ
m : ℕ
⊢ bitwise f (bit a (ofNat m)) (bit b n) = bit (f a b) (bitwise f (ofNat m) n)
have ofNat : ∀ (n : ℕ), bitwise f (bit a (ofNat m)) (bit b (ofNat n)) = bit (f a b) (bitwise f (ofNat m) (ofNat n))
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
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))
⊢ bitwise f (bit a (Int.ofNat m)) (bit b n) = bit (f a b) (bitwise f (Int.ofNat m) n)
have ofNat₁ : ∀ (n : ℕ), bitwise f (bit a (Int.ofNat m)) (bit b -[n+1]) = bit (f a b) (bitwise f (Int.ofNat m) -[n+1])
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
a b : Bool
n : ℤ
m : ℕ
⊢ bitwise f (bit a -[m+1]) (bit b n) = bit (f a b) (bitwise f -[m+1] n)
have negSucc : ∀ (n : ℕ), bitwise f (bit a -[m+1]) (bit b (ofNat n)) = bit (f a b) (bitwise f -[m+1] (ofNat n))
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
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))
⊢ bitwise f (bit a -[m+1]) (bit b n) = bit (f a b) (bitwise f -[m+1] n)
have negSucc₁ : ∀ (n : ℕ), bitwise f (bit a -[m+1]) (bit b -[n+1]) = bit (f a b) (bitwise f -[m+1] -[n+1])
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a (ofNat m)) (bit b (ofNat n)) = bit (f a b) (bitwise f (ofNat m) (ofNat n))
have 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) : ℤ))
Tactic: simp [bitwise, ofNat_eq_natCast, bit_coe_nat, natBitwise, Bool.not_false,
    bit_negSucc]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a (ofNat m)) (bit b -[n+1]) = bit (f a b) (bitwise f (ofNat m) -[n+1])
have 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) : ℤ))
Tactic: simp [bitwise, ofNat_eq_natCast, bit_coe_nat, natBitwise, Bool.not_false,
    bit_negSucc]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a -[m+1]) (bit b (ofNat n)) = bit (f a b) (bitwise f -[m+1] (ofNat n))
have 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) : ℤ))
Tactic: simp [bitwise, ofNat_eq_natCast, bit_coe_nat, natBitwise, Bool.not_false,
    bit_negSucc]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ bitwise f (bit a -[m+1]) (bit b -[n+1]) = bit (f a b) (bitwise f -[m+1] -[n+1])
have 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) : ℤ))
Tactic: simp [bitwise, ofNat_eq_natCast, bit_coe_nat, natBitwise, Bool.not_false,
    bit_negSucc]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
a b : Bool
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) : ℤ))
have 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) : ℤ))
Tactic: by_cases h : f false false
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
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) : ℤ))
⊢ (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) : ℤ))
have 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) : ℤ))
Tactic: by_cases h : f false false
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
a b : Bool
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) : ℤ))
have 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) : ℤ))
Tactic: by_cases h : f false true
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
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) : ℤ))
⊢ (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) : ℤ))
have 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) : ℤ))
Tactic: by_cases h : f false true
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
a b : Bool
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) : ℤ))
have 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) : ℤ))
Tactic: by_cases h : f true false
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
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) : ℤ))
⊢ (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) : ℤ))
have 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) : ℤ))
Tactic: by_cases h : f true false
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
a b : Bool
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) : ℤ))
have 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) : ℤ))
Tactic: by_cases h : f true true
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
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) : ℤ))
⊢ (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) : ℤ))
have 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) : ℤ))
Tactic: by_cases h : f true true
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ (bit a m).lor (bit b n) = bit (a || b) (m.lor n)
have rw : bitwise or (bit a m) (bit b n) = bit (a || b) (bitwise or m n)
Tactic: rw [← bitwise_or, bitwise_bit]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
a : Bool
m : ℤ
b : Bool
n : ℤ
rw : bitwise or (bit a m) (bit b n) = bit (a || b) (bitwise or m n)
⊢ (bit a m).lor (bit b n) = bit (a || b) (m.lor n)
have rw₁ : bit (a || b) (bitwise or m n) = bit (a || b) (bitwise or m n)
Tactic: rw [← bitwise_or, bitwise_bit]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ (bit a m).land (bit b n) = bit (a && b) (m.land n)
have rw : bitwise and (bit a m) (bit b n) = bit (a && b) (bitwise and m n)
Tactic: rw [← bitwise_and, bitwise_bit]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
a : Bool
m : ℤ
b : Bool
n : ℤ
rw : bitwise and (bit a m) (bit b n) = bit (a && b) (bitwise and m n)
⊢ (bit a m).land (bit b n) = bit (a && b) (m.land n)
have rw₁ : bit (a && b) (bitwise and m n) = bit (a && b) (bitwise and m n)
Tactic: rw [← bitwise_and, bitwise_bit]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ (bit a m).ldiff (bit b n) = bit (a && !b) (m.ldiff n)
have 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)
Tactic: rw [← bitwise_diff, bitwise_bit]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
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)
⊢ (bit a m).ldiff (bit b n) = bit (a && !b) (m.ldiff n)
have 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)
Tactic: rw [← bitwise_diff, bitwise_bit]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ (bit a m).xor (bit b n) = bit (a ^^ b) (m.xor n)
have rw : bitwise xor (bit a m) (bit b n) = bit (a ^^ b) (bitwise xor m n)
Tactic: rw [← bitwise_xor, bitwise_bit]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
a : Bool
m : ℤ
b : Bool
n : ℤ
rw : bitwise xor (bit a m) (bit b n) = bit (a ^^ b) (bitwise xor m n)
⊢ (bit a m).xor (bit b n) = bit (a ^^ b) (m.xor n)
have rw₁ : bit (a ^^ b) (bitwise xor m n) = bit (a ^^ b) (bitwise xor m n)
Tactic: rw [← bitwise_xor, bitwise_bit]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
m n : ℤ
k : ℕ
⊢ (bitwise f m n).testBit k = f (m.testBit k) (n.testBit k)
have ofNat : ∀ (a : ℕ), (bitwise f (ofNat a) n).testBit k = f ((ofNat a).testBit k) (n.testBit k)
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
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)
⊢ (bitwise f m n).testBit k = f (m.testBit k) (n.testBit k)
have negSucc : ∀ (a : ℕ), (bitwise f -[a+1] n).testBit k = f (-[a+1].testBit k) (n.testBit k)
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
n : ℤ
k a : ℕ
⊢ (bitwise f (ofNat a) n).testBit k = f ((ofNat a).testBit k) (n.testBit k)
have ofNat : ∀ (a_1 : ℕ), (bitwise f (ofNat a) (ofNat a_1)).testBit k = f ((ofNat a).testBit k) ((ofNat a_1).testBit k)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
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)
⊢ (bitwise f (Int.ofNat a) n).testBit k = f ((Int.ofNat a).testBit k) (n.testBit k)
have ofNat₁ : ∀ (a_1 : ℕ), (bitwise f (Int.ofNat a) -[a_1+1]).testBit k = f ((Int.ofNat a).testBit k) (-[a_1+1].testBit k)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
n : ℤ
k a : ℕ
⊢ (bitwise f -[a+1] n).testBit k = f (-[a+1].testBit k) (n.testBit k)
have negSucc : ∀ (a_1 : ℕ), (bitwise f -[a+1] (ofNat a_1)).testBit k = f (-[a+1].testBit k) ((ofNat a_1).testBit k)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
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)
⊢ (bitwise f -[a+1] n).testBit k = f (-[a+1].testBit k) (n.testBit k)
have negSucc₁ : ∀ (a_1 : ℕ), (bitwise f -[a+1] -[a_1+1]).testBit k = f (-[a+1].testBit k) (-[a_1+1].testBit k)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
k a a_1 : ℕ
⊢ (bitwise f (ofNat a) (ofNat a_1)).testBit k = f ((ofNat a).testBit k) ((ofNat a_1).testBit k)
have ofNat : (match (motive := ℤ → ℕ → Bool)
    bif f false false then -[Nat.bitwise (fun (x y : Bool) ↦ !f x y) a a_1+1] else (↑(Nat.bitwise f a a_1) : ℤ), k with
  | ofNat m, n => m.testBit n
  | -[m+1], n => !m.testBit n) =
  f (a.testBit k) (a_1.testBit k)
Tactic: simp only [testBit, bitwise, natBitwise]