awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
k a a_1 : ℕ
⊢ (bitwise f (ofNat a) -[a_1+1]).testBit k = f ((ofNat a).testBit k) (-[a_1+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 (fun (x y : Bool) ↦ f x !y) 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]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
k a a_1 : ℕ
⊢ (bitwise f -[a+1] (ofNat a_1)).testBit k = f (-[a+1].testBit k) ((ofNat a_1).testBit k)
have negSucc : (match (motive := ℤ → ℕ → Bool)
    bif f (!false) false then -[Nat.bitwise (fun (x y : Bool) ↦ !f (!x) y) a a_1+1]
    else (↑(Nat.bitwise (fun (x y : Bool) ↦ f (!x) y) 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]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
k a a_1 : ℕ
⊢ (bitwise f -[a+1] -[a_1+1]).testBit k = f (-[a+1].testBit k) (-[a_1+1].testBit k)
have negSucc : (match (motive := ℤ → ℕ → Bool)
    bif f (!false) !false then -[Nat.bitwise (fun (x y : Bool) ↦ !f (!x) !y) a a_1+1]
    else (↑(Nat.bitwise (fun (x y : Bool) ↦ f (!x) !y) 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]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
k a a_1 : ℕ
⊢ (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)
have pos : ∀ (h : f false false = true),
  (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: by_cases h : f false false
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
k a a_1 : ℕ
pos :
  ∀ (h : f false false = true),
    (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)
⊢ (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)
have neg : ∀ (h : ¬f false false = true),
  (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: by_cases h : f false false
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
k a a_1 : ℕ
⊢ (match (motive := ℤ → ℕ → Bool)
      bif f false !false then -[Nat.bitwise (fun (x y : Bool) ↦ !f x !y) a a_1+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ f x !y) 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
have pos : ∀ (h : f false true = true),
  (match (motive := ℤ → ℕ → Bool)
      bif f false !false then -[Nat.bitwise (fun (x y : Bool) ↦ !f x !y) a a_1+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ f x !y) 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: by_cases h : f false true
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
k a a_1 : ℕ
pos :
  ∀ (h : f false true = true),
    (match (motive := ℤ → ℕ → Bool)
        bif f false !false then -[Nat.bitwise (fun (x y : Bool) ↦ !f x !y) a a_1+1]
        else (↑(Nat.bitwise (fun (x y : Bool) ↦ f x !y) 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
⊢ (match (motive := ℤ → ℕ → Bool)
      bif f false !false then -[Nat.bitwise (fun (x y : Bool) ↦ !f x !y) a a_1+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ f x !y) 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
have neg : ∀ (h : ¬f false true = true),
  (match (motive := ℤ → ℕ → Bool)
      bif f false !false then -[Nat.bitwise (fun (x y : Bool) ↦ !f x !y) a a_1+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ f x !y) 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: by_cases h : f false true
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
k a a_1 : ℕ
⊢ (match (motive := ℤ → ℕ → Bool)
      bif f (!false) false then -[Nat.bitwise (fun (x y : Bool) ↦ !f (!x) y) a a_1+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ f (!x) y) 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)
have pos : ∀ (h : f true false = true),
  (match (motive := ℤ → ℕ → Bool)
      bif f (!false) false then -[Nat.bitwise (fun (x y : Bool) ↦ !f (!x) y) a a_1+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ f (!x) y) 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: by_cases h : f true false
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
k a a_1 : ℕ
pos :
  ∀ (h : f true false = true),
    (match (motive := ℤ → ℕ → Bool)
        bif f (!false) false then -[Nat.bitwise (fun (x y : Bool) ↦ !f (!x) y) a a_1+1]
        else (↑(Nat.bitwise (fun (x y : Bool) ↦ f (!x) y) 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)
⊢ (match (motive := ℤ → ℕ → Bool)
      bif f (!false) false then -[Nat.bitwise (fun (x y : Bool) ↦ !f (!x) y) a a_1+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ f (!x) y) 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)
have neg : ∀ (h : ¬f true false = true),
  (match (motive := ℤ → ℕ → Bool)
      bif f (!false) false then -[Nat.bitwise (fun (x y : Bool) ↦ !f (!x) y) a a_1+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ f (!x) y) 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: by_cases h : f true false
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
k a a_1 : ℕ
⊢ (match (motive := ℤ → ℕ → Bool)
      bif f (!false) !false then -[Nat.bitwise (fun (x y : Bool) ↦ !f (!x) !y) a a_1+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ f (!x) !y) 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
have pos : ∀ (h : f true true = true),
  (match (motive := ℤ → ℕ → Bool)
      bif f (!false) !false then -[Nat.bitwise (fun (x y : Bool) ↦ !f (!x) !y) a a_1+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ f (!x) !y) 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: by_cases h : f true true
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
k a a_1 : ℕ
pos :
  ∀ (h : f true true = true),
    (match (motive := ℤ → ℕ → Bool)
        bif f (!false) !false then -[Nat.bitwise (fun (x y : Bool) ↦ !f (!x) !y) a a_1+1]
        else (↑(Nat.bitwise (fun (x y : Bool) ↦ f (!x) !y) 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
⊢ (match (motive := ℤ → ℕ → Bool)
      bif f (!false) !false then -[Nat.bitwise (fun (x y : Bool) ↦ !f (!x) !y) a a_1+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ f (!x) !y) 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
have neg : ∀ (h : ¬f true true = true),
  (match (motive := ℤ → ℕ → Bool)
      bif f (!false) !false then -[Nat.bitwise (fun (x y : Bool) ↦ !f (!x) !y) a a_1+1]
      else (↑(Nat.bitwise (fun (x y : Bool) ↦ f (!x) !y) 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: by_cases h : f true true
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℤ
k : ℕ
⊢ (m.lor n).testBit k = (m.testBit k || n.testBit k)
have rw : (bitwise or m n).testBit k = (m.testBit k || n.testBit k)
Tactic: rw [← bitwise_or, testBit_bitwise]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℤ
k : ℕ
rw : (bitwise or m n).testBit k = (m.testBit k || n.testBit k)
⊢ (m.lor n).testBit k = (m.testBit k || n.testBit k)
have rw₁ : (m.testBit k || n.testBit k) = (m.testBit k || n.testBit k)
Tactic: rw [← bitwise_or, testBit_bitwise]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℤ
k : ℕ
⊢ (m.land n).testBit k = (m.testBit k && n.testBit k)
have rw : (bitwise and m n).testBit k = (m.testBit k && n.testBit k)
Tactic: rw [← bitwise_and, testBit_bitwise]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℤ
k : ℕ
rw : (bitwise and m n).testBit k = (m.testBit k && n.testBit k)
⊢ (m.land n).testBit k = (m.testBit k && n.testBit k)
have rw₁ : (m.testBit k && n.testBit k) = (m.testBit k && n.testBit k)
Tactic: rw [← bitwise_and, testBit_bitwise]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℤ
k : ℕ
⊢ (m.ldiff n).testBit k = (m.testBit k && !n.testBit k)
have rw : (bitwise (fun (a b : Bool) ↦ a && !b) m n).testBit k = (m.testBit k && !n.testBit k)
Tactic: rw [← bitwise_diff, testBit_bitwise]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℤ
k : ℕ
rw : (bitwise (fun (a b : Bool) ↦ a && !b) m n).testBit k = (m.testBit k && !n.testBit k)
⊢ (m.ldiff n).testBit k = (m.testBit k && !n.testBit k)
have rw₁ : (m.testBit k && !n.testBit k) = (m.testBit k && !n.testBit k)
Tactic: rw [← bitwise_diff, testBit_bitwise]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℤ
k : ℕ
⊢ (m.xor n).testBit k = (m.testBit k ^^ n.testBit k)
have rw : (bitwise xor m n).testBit k = (m.testBit k ^^ n.testBit k)
Tactic: rw [← bitwise_xor, testBit_bitwise]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℤ
k : ℕ
rw : (bitwise xor m n).testBit k = (m.testBit k ^^ n.testBit k)
⊢ (m.xor n).testBit k = (m.testBit k ^^ n.testBit k)
have rw₁ : (m.testBit k ^^ n.testBit k) = (m.testBit k ^^ n.testBit k)
Tactic: rw [← bitwise_xor, testBit_bitwise]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℤ
⊢ m >>> (-n) = m <<< n
have rw : m <<< (- -n) = m <<< n
Tactic: rw [← shiftLeft_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℤ
rw : m <<< (- -n) = m <<< n
⊢ m >>> (-n) = m <<< n
have rw₁ : m <<< n = m <<< n
Tactic: rw [← shiftLeft_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
⊢ HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑m : ℤ) (↑n : ℤ) = (↑(m >>> n) : ℤ)
have zero : HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑m : ℤ) (↑0 : ℤ) = (↑(HShiftRight.hShiftRight (β := ℕ) m 0) : ℤ)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
zero : HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑m : ℤ) (↑0 : ℤ) = (↑(HShiftRight.hShiftRight (β := ℕ) m 0) : ℤ)
⊢ HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑m : ℤ) (↑n : ℤ) = (↑(m >>> n) : ℤ)
have succ : ∀ (n : ℕ), HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑m : ℤ) (↑(n + 1) : ℤ) = (↑(m >>> (n + 1)) : ℤ)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
⊢ HShiftRight.hShiftRight (β := ℤ) -[m+1] (↑n : ℤ) = -[m >>> n+1]
have zero : HShiftRight.hShiftRight (β := ℤ) -[m+1] (↑0 : ℤ) = -[HShiftRight.hShiftRight (β := ℕ) m 0+1]
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n : ℕ
zero : HShiftRight.hShiftRight (β := ℤ) -[m+1] (↑0 : ℤ) = -[HShiftRight.hShiftRight (β := ℕ) m 0+1]
⊢ HShiftRight.hShiftRight (β := ℤ) -[m+1] (↑n : ℤ) = -[m >>> n+1]
have succ : ∀ (n : ℕ), HShiftRight.hShiftRight (β := ℤ) -[m+1] (↑(n + 1) : ℤ) = -[m >>> (n + 1)+1]
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n k : ℕ
⊢ HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ)) =
    HShiftRight.hShiftRight (β := ℤ) (HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑m : ℤ) (↑n : ℤ)) (↑k : ℤ)
have rw : HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ)) =
  HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑(m >>> n) : ℤ) (↑k : ℤ)
Tactic: rw [shiftRight_natCast, shiftRight_natCast, ← Int.natCast_add, shiftRight_natCast,
      Nat.shiftRight_add]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n k : ℕ
rw :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ)) =
    HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑(m >>> n) : ℤ) (↑k : ℤ)
⊢ HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ)) =
    HShiftRight.hShiftRight (β := ℤ) (HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑m : ℤ) (↑n : ℤ)) (↑k : ℤ)
have rw₁ : HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ)) = (↑(m >>> n >>> k) : ℤ)
Tactic: rw [shiftRight_natCast, shiftRight_natCast, ← Int.natCast_add, shiftRight_natCast,
      Nat.shiftRight_add]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n k : ℕ
rw :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ)) =
    HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑(m >>> n) : ℤ) (↑k : ℤ)
rw₁ : HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ)) = (↑(m >>> n >>> k) : ℤ)
⊢ HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ)) =
    HShiftRight.hShiftRight (β := ℤ) (HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑m : ℤ) (↑n : ℤ)) (↑k : ℤ)
have rw₂ : HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑m : ℤ) (↑(n + k) : ℤ) = (↑(m >>> n >>> k) : ℤ)
Tactic: rw [shiftRight_natCast, shiftRight_natCast, ← Int.natCast_add, shiftRight_natCast,
      Nat.shiftRight_add]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n k : ℕ
rw :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ)) =
    HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑(m >>> n) : ℤ) (↑k : ℤ)
rw₁ : HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ)) = (↑(m >>> n >>> k) : ℤ)
rw₂ : HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑m : ℤ) (↑(n + k) : ℤ) = (↑(m >>> n >>> k) : ℤ)
⊢ HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ)) =
    HShiftRight.hShiftRight (β := ℤ) (HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑m : ℤ) (↑n : ℤ)) (↑k : ℤ)
have rw₃ : Eq (α := ℤ) (↑(m >>> (n + k)) : ℤ) (↑(m >>> n >>> k) : ℤ)
Tactic: rw [shiftRight_natCast, shiftRight_natCast, ← Int.natCast_add, shiftRight_natCast,
      Nat.shiftRight_add]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n k : ℕ
rw :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ)) =
    HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑(m >>> n) : ℤ) (↑k : ℤ)
rw₁ : HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ)) = (↑(m >>> n >>> k) : ℤ)
rw₂ : HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑m : ℤ) (↑(n + k) : ℤ) = (↑(m >>> n >>> k) : ℤ)
rw₃ : Eq (α := ℤ) (↑(m >>> (n + k)) : ℤ) (↑(m >>> n >>> k) : ℤ)
⊢ HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ)) =
    HShiftRight.hShiftRight (β := ℤ) (HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑m : ℤ) (↑n : ℤ)) (↑k : ℤ)
have rw₄ : Eq (α := ℤ) (↑(m >>> n >>> k) : ℤ) (↑(m >>> n >>> k) : ℤ)
Tactic: rw [shiftRight_natCast, shiftRight_natCast, ← Int.natCast_add, shiftRight_natCast,
      Nat.shiftRight_add]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n k : ℕ
⊢ -[m+1] >>> HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ) =
    HShiftRight.hShiftRight (β := ℤ) (HShiftRight.hShiftRight (β := ℤ) -[m+1] (↑n : ℤ)) (↑k : ℤ)
have rw : -[m+1] >>> HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ) = HShiftRight.hShiftRight (β := ℤ) -[m >>> n+1] (↑k : ℤ)
Tactic: rw [shiftRight_negSucc, shiftRight_negSucc, ← Int.natCast_add, shiftRight_negSucc,
      Nat.shiftRight_add]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n k : ℕ
rw : -[m+1] >>> HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ) = HShiftRight.hShiftRight (β := ℤ) -[m >>> n+1] (↑k : ℤ)
⊢ -[m+1] >>> HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ) =
    HShiftRight.hShiftRight (β := ℤ) (HShiftRight.hShiftRight (β := ℤ) -[m+1] (↑n : ℤ)) (↑k : ℤ)
have rw₁ : -[m+1] >>> HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ) = -[m >>> n >>> k+1]
Tactic: rw [shiftRight_negSucc, shiftRight_negSucc, ← Int.natCast_add, shiftRight_negSucc,
      Nat.shiftRight_add]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n k : ℕ
rw : -[m+1] >>> HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ) = HShiftRight.hShiftRight (β := ℤ) -[m >>> n+1] (↑k : ℤ)
rw₁ : -[m+1] >>> HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ) = -[m >>> n >>> k+1]
⊢ -[m+1] >>> HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ) =
    HShiftRight.hShiftRight (β := ℤ) (HShiftRight.hShiftRight (β := ℤ) -[m+1] (↑n : ℤ)) (↑k : ℤ)
have rw₂ : HShiftRight.hShiftRight (β := ℤ) -[m+1] (↑(n + k) : ℤ) = -[m >>> n >>> k+1]
Tactic: rw [shiftRight_negSucc, shiftRight_negSucc, ← Int.natCast_add, shiftRight_negSucc,
      Nat.shiftRight_add]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n k : ℕ
rw : -[m+1] >>> HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ) = HShiftRight.hShiftRight (β := ℤ) -[m >>> n+1] (↑k : ℤ)
rw₁ : -[m+1] >>> HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ) = -[m >>> n >>> k+1]
rw₂ : HShiftRight.hShiftRight (β := ℤ) -[m+1] (↑(n + k) : ℤ) = -[m >>> n >>> k+1]
⊢ -[m+1] >>> HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ) =
    HShiftRight.hShiftRight (β := ℤ) (HShiftRight.hShiftRight (β := ℤ) -[m+1] (↑n : ℤ)) (↑k : ℤ)
have rw₃ : -[m >>> (n + k)+1] = -[m >>> n >>> k+1]
Tactic: rw [shiftRight_negSucc, shiftRight_negSucc, ← Int.natCast_add, shiftRight_negSucc,
      Nat.shiftRight_add]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n k : ℕ
rw : -[m+1] >>> HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ) = HShiftRight.hShiftRight (β := ℤ) -[m >>> n+1] (↑k : ℤ)
rw₁ : -[m+1] >>> HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ) = -[m >>> n >>> k+1]
rw₂ : HShiftRight.hShiftRight (β := ℤ) -[m+1] (↑(n + k) : ℤ) = -[m >>> n >>> k+1]
rw₃ : -[m >>> (n + k)+1] = -[m >>> n >>> k+1]
⊢ -[m+1] >>> HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ) =
    HShiftRight.hShiftRight (β := ℤ) (HShiftRight.hShiftRight (β := ℤ) -[m+1] (↑n : ℤ)) (↑k : ℤ)
have rw₄ : -[m >>> n >>> k+1] = -[m >>> n >>> k+1]
Tactic: rw [shiftRight_negSucc, shiftRight_negSucc, ← Int.natCast_add, shiftRight_negSucc,
      Nat.shiftRight_add]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m : ℤ
n : ℕ
⊢ m <<< (↑n : ℤ) = m <<< n
have rw : m <<< (↑n : ℤ) = m * (↑(HPow.hPow (α := ℕ) 2 n) : ℤ)
Tactic: rw [Int.shiftLeft_eq']
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m : ℤ
n : ℕ
⊢ m <<< (↑n : ℤ) = m * (↑(HPow.hPow (α := ℕ) 2 n) : ℤ)
have unfold_projs : (match (motive := ℤ → ℤ → ℤ) m, (↑n : ℤ) with
  | ofNat m, ofNat n => (↑(Nat.shiftLeft' false m n) : ℤ)
  | ofNat m, -[n+1] => (↑(m.shiftRight n.succ) : ℤ)
  | -[m+1], ofNat n => -[Nat.shiftLeft' true m n+1]
  | -[m+1], -[n+1] => -[m.shiftRight n.succ+1]) =
  m.mul (↑(Nat.pow 2 n) : ℤ)
Tactic: unfold_projs
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m : ℤ
n : ℕ
⊢ (match (motive := ℤ → ℤ → ℤ) m, (↑n : ℤ) with
    | ofNat m, ofNat n => (↑(Nat.shiftLeft' false m n) : ℤ)
    | ofNat m, -[n+1] => (↑(m.shiftRight n.succ) : ℤ)
    | -[m+1], ofNat n => -[Nat.shiftLeft' true m n+1]
    | -[m+1], -[n+1] => -[m.shiftRight n.succ+1]) =
    m.mul (↑(Nat.pow 2 n) : ℤ)
have ofNat : ∀ (a : ℕ),
  (match (motive := ℤ → ℤ → ℤ) ofNat a, (↑n : ℤ) with
    | ofNat m, ofNat n => (↑(Nat.shiftLeft' false m n) : ℤ)
    | ofNat m, -[n+1] => (↑(m.shiftRight n.succ) : ℤ)
    | -[m+1], ofNat n => -[Nat.shiftLeft' true m n+1]
    | -[m+1], -[n+1] => -[m.shiftRight n.succ+1]) =
    (ofNat a).mul (↑(Nat.pow 2 n) : ℤ)
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m : ℤ
n : ℕ
ofNat :
  ∀ (a : ℕ),
    (match (motive := ℤ → ℤ → ℤ) Int.ofNat a, (↑n : ℤ) with
      | Int.ofNat m, Int.ofNat n => (↑(Nat.shiftLeft' false m n) : ℤ)
      | Int.ofNat m, -[n+1] => (↑(m.shiftRight n.succ) : ℤ)
      | -[m+1], Int.ofNat n => -[Nat.shiftLeft' true m n+1]
      | -[m+1], -[n+1] => -[m.shiftRight n.succ+1]) =
      (Int.ofNat a).mul (↑(Nat.pow 2 n) : ℤ)
⊢ (match (motive := ℤ → ℤ → ℤ) m, (↑n : ℤ) with
    | Int.ofNat m, Int.ofNat n => (↑(Nat.shiftLeft' false m n) : ℤ)
    | Int.ofNat m, -[n+1] => (↑(m.shiftRight n.succ) : ℤ)
    | -[m+1], Int.ofNat n => -[Nat.shiftLeft' true m n+1]
    | -[m+1], -[n+1] => -[m.shiftRight n.succ+1]) =
    m.mul (↑(Nat.pow 2 n) : ℤ)
have negSucc : ∀ (a : ℕ),
  (match (motive := ℤ → ℤ → ℤ) -[a+1], (↑n : ℤ) with
    | Int.ofNat m, Int.ofNat n => (↑(Nat.shiftLeft' false m n) : ℤ)
    | Int.ofNat m, -[n+1] => (↑(m.shiftRight n.succ) : ℤ)
    | -[m+1], Int.ofNat n => -[Nat.shiftLeft' true m n+1]
    | -[m+1], -[n+1] => -[m.shiftRight n.succ+1]) =
    -[a+1].mul (↑(Nat.pow 2 n) : ℤ)
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n a : ℕ
⊢ (match (motive := ℤ → ℤ → ℤ) ofNat a, (↑n : ℤ) with
    | ofNat m, ofNat n => (↑(Nat.shiftLeft' false m n) : ℤ)
    | ofNat m, -[n+1] => (↑(m.shiftRight n.succ) : ℤ)
    | -[m+1], ofNat n => -[Nat.shiftLeft' true m n+1]
    | -[m+1], -[n+1] => -[m.shiftRight n.succ+1]) =
    (ofNat a).mul (↑(Nat.pow 2 n) : ℤ)
have ofNat : (↑a : ℤ) <<< n = (↑a : ℤ) * HPow.hPow (α := ℤ) 2 n
Tactic: simp only [Nat.shiftLeft'_false, natCast_shiftLeft, ofNat_eq_natCast,
    Nat.pow_eq, Int.natCast_pow, Nat.cast_ofNat, mul_def]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
n a : ℕ
⊢ -[Nat.shiftLeft' true a n+1] = -[a+1] * HPow.hPow (α := ℤ) 2 n
have negSucc : -(↑((a + 1) * HPow.hPow (α := ℕ) 2 n) : ℤ) = -(↑(a + 1) : ℤ) * HPow.hPow (α := ℤ) 2 n
Tactic: simp only [negSucc_eq, ← natCast_add_one, Nat.shiftLeft'_true_eq_mul_pow]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m : ℤ
n : ℕ
⊢ HShiftRight.hShiftRight (β := ℤ) m (↑n : ℤ) = m >>> n
have ofNat : ∀ (a : ℕ), HShiftRight.hShiftRight (β := ℤ) (ofNat a) (↑n : ℤ) = ofNat a >>> n
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m : ℤ
n : ℕ
ofNat : ∀ (a : ℕ), HShiftRight.hShiftRight (β := ℤ) (Int.ofNat a) (↑n : ℤ) = Int.ofNat a >>> n
⊢ HShiftRight.hShiftRight (β := ℤ) m (↑n : ℤ) = m >>> n
have negSucc : ∀ (a : ℕ), HShiftRight.hShiftRight (β := ℤ) -[a+1] (↑n : ℤ) = -[a+1] >>> n
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n_1 k i n : ℕ
⊢ (↑m : ℤ) <<< -[i+1] = (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
have simp_rw : (↑m : ℤ) <<< (-HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
Tactic: simp_rw [negSucc_eq, shiftLeft_neg, Nat.shiftLeft'_false, Nat.shiftRight_add,
          ← Nat.shiftLeft_sub _ le_rfl, Nat.sub_self, Nat.shiftLeft_zero, ← shiftRight_natCast,
          ← shiftRight_add', Nat.cast_one]