awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
k a a_1 : ℕ
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
    | Int.ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (a.testBit k) (a_1.testBit k)
⊢ (bitwise f (Int.ofNat a) (Int.ofNat a_1)).testBit k = f ((Int.ofNat a).testBit k) ((Int.ofNat a_1).testBit k)

Tactic:
simp only [testBit, bitwise, natBitwise]

Premises used: Int.testBit, Int.natBitwise, Int.bitwise
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
k a a_1 : ℕ
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
    | Int.ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (a.testBit k) !a_1.testBit k
⊢ (bitwise f (Int.ofNat a) -[a_1+1]).testBit k = f ((Int.ofNat a).testBit k) (-[a_1+1].testBit k)

Tactic:
simp only [testBit, bitwise, natBitwise]

Premises used: Int.testBit, Int.natBitwise, Int.bitwise
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
k a a_1 : ℕ
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)
⊢ (bitwise f -[a+1] (ofNat a_1)).testBit k = f (-[a+1].testBit k) ((ofNat a_1).testBit k)

Tactic:
simp only [testBit, bitwise, natBitwise]

Premises used: Int.testBit, Int.natBitwise, Int.bitwise
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
k a a_1 : ℕ
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
⊢ (bitwise f -[a+1] -[a_1+1]).testBit k = f (-[a+1].testBit k) (-[a_1+1].testBit k)

Tactic:
simp only [testBit, bitwise, natBitwise]

Premises used: Int.testBit, Int.natBitwise, Int.bitwise
-- Module: Mathlib.Data.Int.Bitwise
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)
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)
⊢ (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

Premises used: Bool.false
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
k a a_1 : ℕ
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:
simp [h]
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
k a a_1 : ℕ
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:
simp [h]
-- Module: Mathlib.Data.Int.Bitwise
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
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
⊢ (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

Premises used: Bool.true, Bool.false
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
k a a_1 : ℕ
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:
simp [h]
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
k a a_1 : ℕ
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:
simp [h]
-- Module: Mathlib.Data.Int.Bitwise
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)
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)
⊢ (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

Premises used: Bool.true, Bool.false
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
k a a_1 : ℕ
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:
simp [h]
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
k a a_1 : ℕ
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:
simp [h]
-- Module: Mathlib.Data.Int.Bitwise
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
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
⊢ (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

Premises used: Bool.true
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
k a a_1 : ℕ
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:
simp [h]
-- Module: Mathlib.Data.Int.Bitwise
Goal:
f : Bool → Bool → Bool
k a a_1 : ℕ
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:
simp [h]
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℤ
k : ℕ
rw : (bitwise or m n).testBit k = (m.testBit k || n.testBit k)
rw₁ rw₂ : (m.testBit k || n.testBit k) = (m.testBit k || n.testBit k)
⊢ (m.lor n).testBit k = (m.testBit k || n.testBit k)

Tactic:
rw [← bitwise_or, testBit_bitwise]

Premises used: Int.testBit_bitwise, Int.bitwise_or
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℤ
k : ℕ
rw : (bitwise and m n).testBit k = (m.testBit k && n.testBit k)
rw₁ rw₂ : (m.testBit k && n.testBit k) = (m.testBit k && n.testBit k)
⊢ (m.land n).testBit k = (m.testBit k && n.testBit k)

Tactic:
rw [← bitwise_and, testBit_bitwise]

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

Tactic:
rw [← bitwise_diff, testBit_bitwise]

Premises used: Int.bitwise_diff, Int.testBit_bitwise
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℤ
k : ℕ
rw : (bitwise xor m n).testBit k = (m.testBit k ^^ n.testBit k)
rw₁ rw₂ : (m.testBit k ^^ n.testBit k) = (m.testBit k ^^ n.testBit k)
⊢ (m.xor n).testBit k = (m.testBit k ^^ n.testBit k)

Tactic:
rw [← bitwise_xor, testBit_bitwise]

Premises used: Int.testBit_bitwise, Int.bitwise_xor
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n k : ℕ
⊢ (lnot (↑n : ℤ)).testBit k = !testBit (↑n : ℤ) k

Tactic:
simp [lnot, testBit]

Premises used: Int.testBit, Int.lnot
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n k : ℕ
⊢ -[n+1].lnot.testBit k = !-[n+1].testBit k

Tactic:
simp [lnot, testBit]

Premises used: Int.testBit, Int.lnot
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℤ
⊢ m <<< (-n) = m >>> n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℤ
rw : m <<< (- -n) = m <<< n
rw₁ rw₂ : m <<< n = m <<< n
⊢ m >>> (-n) = m <<< n

Tactic:
rw [← shiftLeft_neg, neg_neg]

Premises used: neg_neg, Int.shiftLeft_neg
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ Eq (α := ℤ)
    (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.shiftLeft n) : ℤ) : ℤ)

Tactic:
simp
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
zero : HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑m : ℤ) (↑0 : ℤ) = (↑(HShiftRight.hShiftRight (β := ℕ) m 0) : ℤ)
succ : ∀ (n : ℕ), HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑m : ℤ) (↑(n + 1) : ℤ) = (↑(m >>> (n + 1)) : ℤ)
⊢ HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑m : ℤ) (↑n : ℤ) = (↑(m >>> n) : ℤ)

Tactic:
cases n
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m : ℕ
⊢ HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑m : ℤ) (↑0 : ℤ) = (↑(HShiftRight.hShiftRight (β := ℕ) m 0) : ℤ)

Tactic:
rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑m : ℤ) (↑(n + 1) : ℤ) = (↑(m >>> (n + 1)) : ℤ)

Tactic:
rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ -[m+1] <<< (↑n : ℤ) = -[Nat.shiftLeft' true m n+1]

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
zero : HShiftRight.hShiftRight (β := ℤ) -[m+1] (↑0 : ℤ) = -[HShiftRight.hShiftRight (β := ℕ) m 0+1]
succ : ∀ (n : ℕ), HShiftRight.hShiftRight (β := ℤ) -[m+1] (↑(n + 1) : ℤ) = -[m >>> (n + 1)+1]
⊢ HShiftRight.hShiftRight (β := ℤ) -[m+1] (↑n : ℤ) = -[m >>> n+1]

Tactic:
cases n
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m : ℕ
⊢ HShiftRight.hShiftRight (β := ℤ) -[m+1] (↑0 : ℤ) = -[HShiftRight.hShiftRight (β := ℕ) m 0+1]

Tactic:
rfl
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n : ℕ
⊢ HShiftRight.hShiftRight (β := ℤ) -[m+1] (↑(n + 1) : ℤ) = -[m >>> (n + 1)+1]

Tactic:
rfl
-- Module: Mathlib.Data.Int.Bitwise
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) : ℤ)
rw₄ rw₅ : Eq (α := ℤ) (↑(m >>> n >>> k) : ℤ) (↑(m >>> n >>> k) : ℤ)
⊢ HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ)) =
    HShiftRight.hShiftRight (β := ℤ) (HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑m : ℤ) (↑n : ℤ)) (↑k : ℤ)

Tactic:
rw [shiftRight_natCast, shiftRight_natCast, ← Int.natCast_add, shiftRight_natCast,
      Nat.shiftRight_add]

Premises used: Int.natCast_add, Nat.shiftRight_add, Int.shiftRight_natCast
-- Module: Mathlib.Data.Int.Bitwise
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]
rw₄ rw₅ : -[m >>> n >>> k+1] = -[m >>> n >>> k+1]
⊢ -[m+1] >>> HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑k : ℤ) =
    HShiftRight.hShiftRight (β := ℤ) (HShiftRight.hShiftRight (β := ℤ) -[m+1] (↑n : ℤ)) (↑k : ℤ)

Tactic:
rw [shiftRight_negSucc, shiftRight_negSucc, ← Int.natCast_add, shiftRight_negSucc,
      Nat.shiftRight_add]

Premises used: Int.shiftRight_negSucc, Int.natCast_add, Nat.shiftRight_add
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m : ℤ
n : ℕ
rw : m <<< (↑n : ℤ) = m * (↑(HPow.hPow (α := ℕ) 2 n) : ℤ)
⊢ m <<< (↑n : ℤ) = m <<< n

Tactic:
rw [Int.shiftLeft_eq']

Premises used: Int.shiftLeft_eq'
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m : ℤ
n : ℕ
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) : ℤ)
⊢ m <<< (↑n : ℤ) = m * (↑(HPow.hPow (α := ℕ) 2 n) : ℤ)

Tactic:
unfold_projs
-- Module: Mathlib.Data.Int.Bitwise
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) : ℤ)
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) : ℤ)
⊢ (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) : ℤ)

Tactic:
cases m
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n a : ℕ
ofNat : (↑a : ℤ) <<< n = (↑a : ℤ) * HPow.hPow (α := ℤ) 2 n
⊢ (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) : ℤ)

Tactic:
simp only [Nat.shiftLeft'_false, natCast_shiftLeft, ofNat_eq_natCast,
    Nat.pow_eq, Int.natCast_pow, Nat.cast_ofNat, mul_def]

Premises used: Nat.pow_eq, Nat.cast_ofNat, Nat.shiftLeft'_false, Int.natCast_pow, Int.mul_def, Int.ofNat_eq_natCast, Int.natCast_shiftLeft
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n a : ℕ
⊢ (↑a : ℤ) <<< n = (↑a : ℤ) * HPow.hPow (α := ℤ) 2 n

Tactic:
grind [Int.shiftLeft_eq']

Premises used: Int.shiftLeft_eq'
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n a : ℕ
negSucc : -(↑((a + 1) * HPow.hPow (α := ℕ) 2 n) : ℤ) = -(↑(a + 1) : ℤ) * HPow.hPow (α := ℤ) 2 n
⊢ -[Nat.shiftLeft' true a n+1] = -[a+1] * HPow.hPow (α := ℤ) 2 n

Tactic:
simp only [negSucc_eq, ← natCast_add_one, Nat.shiftLeft'_true_eq_mul_pow]

Premises used: Int.negSucc_eq, Int.natCast_add_one, Nat.shiftLeft'_true_eq_mul_pow
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n a : ℕ
⊢ -(↑((a + 1) * HPow.hPow (α := ℕ) 2 n) : ℤ) = -(↑(a + 1) : ℤ) * HPow.hPow (α := ℤ) 2 n

Tactic:
grind
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m : ℤ
n : ℕ
ofNat : ∀ (a : ℕ), HShiftRight.hShiftRight (β := ℤ) (Int.ofNat a) (↑n : ℤ) = Int.ofNat a >>> n
negSucc : ∀ (a : ℕ), HShiftRight.hShiftRight (β := ℤ) -[a+1] (↑n : ℤ) = -[a+1] >>> n
⊢ HShiftRight.hShiftRight (β := ℤ) m (↑n : ℤ) = m >>> n

Tactic:
cases m
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n a : ℕ
⊢ HShiftRight.hShiftRight (β := ℤ) (ofNat a) (↑n : ℤ) = ofNat a >>> n

Tactic:
simp
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n a : ℕ
⊢ HShiftRight.hShiftRight (β := ℤ) -[a+1] (↑n : ℤ) = -[a+1] >>> n

Tactic:
simp
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n k : ℕ
⊢ Nat.shiftLeft' false m (n + k) = Nat.shiftLeft' false (Nat.shiftLeft' false m n) k

Tactic:
simp [Nat.shiftLeft_eq, Nat.pow_add, mul_assoc]

Premises used: Nat.shiftLeft_eq, Nat.pow_add, mul_assoc
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n_1 k i n : ℕ
⊢ (fun (n k : ℕ) (i : ℤ) ↦ (↑m : ℤ) <<< i = (↑(Nat.shiftLeft' false m n >>> k) : ℤ)) (n + i) n (↑i : ℤ)

Tactic:
simp [← Nat.shiftLeft_sub _]

Premises used: Nat.shiftLeft_sub
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n_1 k i n : ℕ
simp_rw : (↑m : ℤ) <<< (-HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
simp_rw₁ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
simp_rw₂ : HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = (↑(m <<< n >>> (n + i + 1)) : ℤ)
simp_rw₃ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(HShiftRight.hShiftRight (β := ℕ) (m <<< n >>> n >>> i) 1) : ℤ)
simp_rw₄ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(HShiftRight.hShiftRight (β := ℕ) (m <<< (n - n) >>> i) 1) : ℤ)
simp_rw₅ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(HShiftRight.hShiftRight (β := ℕ) (m <<< 0 >>> i) 1) : ℤ)
simp_rw₆ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(HShiftRight.hShiftRight (β := ℕ) (m >>> i) 1) : ℤ)
simp_rw₇ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    HShiftRight.hShiftRight (β := ℤ) (HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑m : ℤ) (↑i : ℤ)) (↑1 : ℤ)
simp_rw₈ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) (↑1 : ℤ))
⊢ (↑m : ℤ) <<< -[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]

Premises used: le_rfl, Nat.shiftLeft'_false, Nat.shiftRight_add, Nat.shiftLeft_sub, Int.shiftRight_natCast, Nat.shiftLeft_zero, Nat.sub_self, Int.shiftRight_add', Int.negSucc_eq, Nat.cast_one, Int.shiftLeft_neg
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n_1 k i n : ℕ
a : n ≤ n + i
⊢ Nat.shiftLeft' true m i = Nat.shiftLeft' true m (n + i) >>> n

Tactic:
rw [← Nat.shiftLeft'_sub, Nat.add_sub_cancel_left]

Premises used: Nat.shiftLeft'_sub, Nat.add_sub_cancel_left
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n_1 k i n : ℕ
⊢ n ≤ n + i

Tactic:
apply Nat.le_add_right

Premises used: Nat.le_add_right
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m n_1 k i n : ℕ
rw : m >>> i.succ = Nat.shiftLeft' true m n >>> (n + (i + 1))
rw₁ : m >>> i.succ = Nat.shiftLeft' true m n >>> n >>> (i + 1)
rw₂ : m >>> i.succ = Nat.shiftLeft' true m (n - n) >>> (i + 1)
rw₃ : m >>> i.succ = Nat.shiftLeft' true m 0 >>> (i + 1)
rw₄ rw₅ : m >>> i.succ = m >>> (i + 1)
⊢ m >>> i.succ = Nat.shiftLeft' true m n >>> (n + i + 1)

Tactic:
rw [add_assoc, Nat.shiftRight_add, ← Nat.shiftLeft'_sub _ _ le_rfl,
          Nat.sub_self, Nat.shiftLeft']

Premises used: le_rfl, add_assoc, Nat.shiftLeft'_sub, Nat.shiftRight_add, Nat.sub_self, Nat.shiftLeft'
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m : ℤ
n : ℕ
k : ℤ
⊢ m <<< ((↑n : ℤ) - k) = m <<< (↑n : ℤ) >>> k

Tactic:
shiftLeft_add' _ _ _

Premises used: Int.shiftLeft_add', Int.sub
-- Module: Mathlib.Data.Int.Bitwise
Goal:
m x : ℕ
⊢ Nat.shiftLeft' false m x = m * HPow.hPow (α := ℕ) 2 x

Tactic:
simp [Nat.shiftLeft_eq]

Premises used: Nat.shiftLeft_eq
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℕ
⊢ Nat.shiftLeft' false 1 n = HPow.hPow (α := ℕ) 2 n

Tactic:
simp [Nat.shiftLeft_eq]

Premises used: Nat.shiftLeft_eq
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℕ
⊢ Nat.shiftLeft' false 0 n = 0

Tactic:
simp
-- Module: Mathlib.Data.Int.Bitwise
Goal:
a : ℕ
⊢ 0 >>> a.succ = 0

Tactic:
simp
-- Module: Mathlib.Data.Int.Bitwise
Goal:
n : ℤ
⊢ HShiftRight.hShiftRight (α := ℤ) 0 n = 0

Tactic:
zero_shiftLeft' _

Premises used: Int.zero_shiftLeft'
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v : ℤ
h :
  ∀ (x : ℤ),
    x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔
      x ∈ map { toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } ({x ∈ Ico (a - v) (b - v) | r ∣ x})
⊢ {x ∈ Ico a b | x ≡ v [ZMOD r]} =
    map { toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } ({x ∈ Ico (a - v) (b - v) | r ∣ x})

Tactic:
ext x