awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
⊢ (bit true n + 1).div2 = bif (bit true n).bodd then (bit true n).div2.succ else (bit true n).div2

Tactic:
simp [bit_val, div2_val, Nat.succ_div, Nat.add_assoc, Nat.dvd_add_right (Nat.dvd_mul_right _ _)]

Premises used: Nat.dvd_add_right, Nat.div2_val, Nat.succ_div, Nat.bit_val, Nat.add_assoc, Nat.dvd_mul_right
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
bit :
  ∀ (b : Bool) (n : ℕ),
    (Nat.bit b n + 1).div2 = bif (Nat.bit b n).bodd then (Nat.bit b n).div2.succ else (Nat.bit b n).div2
⊢ (n + 1).div2 = bif n.bodd then n.div2.succ else n.div2

Tactic:
cases n using bitCasesOn with
  | bit b n => cases b <;>
    simp [bit_val, div2_val, Nat.succ_div, Nat.add_assoc, Nat.dvd_add_right (Nat.dvd_mul_right _ _)]

Premises used: Nat.bit, Nat.dvd_add_right, Nat.bitCasesOn, Nat.div2_val, Nat.succ_div, Nat.bit_val, Nat.add_assoc, Nat.dvd_mul_right
-- Module: Mathlib.Data.Nat.Bits
Goal:
b : Bool
n : ℕ
rw : bit b n / 2 = n
rw₁ rw₂ : n = n
⊢ (bit b n).div2 = n

Tactic:
rw [div2_val, bit_div_two]

Premises used: Nat.div2_val, Nat.bit_div_two
-- Module: Mathlib.Data.Nat.Bits
Goal:
b : Bool
n : ℕ
⊢ (bit b n).bodd.toNat + 2 * (bit b n).div2 = bit b n

Tactic:
simpa using (bit_val b n).symm

Premises used: Nat.bit_val, Eq.symm
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
bit : ∀ (b : Bool) (n : ℕ), (Nat.bit b n).bodd.toNat + 2 * (Nat.bit b n).div2 = Nat.bit b n
⊢ n.bodd.toNat + 2 * n.div2 = n

Tactic:
cases n using bitCasesOn with
  | bit b n => simpa using (bit_val b n).symm

Premises used: Nat.bit, Nat.bitCasesOn
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
⊢ bit n.bodd n.div2 = n

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

Premises used: Nat.bit_val, Nat.bodd_add_div2, Eq.trans, Nat.add_comm
-- Module: Mathlib.Data.Nat.Bits
Goal:
⊢ bit false 0 = 0

Tactic:
rfl

Premises used: cond, Nat.bit, rfl
-- Module: Mathlib.Data.Nat.Bits
Goal:
m n : ℕ
rw : m * HPow.hPow (α := ℕ) 2 n.succ = HPow.hPow (α := ℕ) 2 (n + 1) * m
⊢ 2 * (m * HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n + 1) * m

Tactic:
rw [Nat.mul_comm, Nat.mul_assoc, ← Nat.pow_succ]

Premises used: Nat.pow_succ, Nat.mul_comm, Nat.mul_assoc
-- Module: Mathlib.Data.Nat.Bits
Goal:
m n : ℕ
⊢ m * HPow.hPow (α := ℕ) 2 n.succ = HPow.hPow (α := ℕ) 2 (n + 1) * m

Tactic:
simp
-- Module: Mathlib.Data.Nat.Bits
Goal:
m n : ℕ
⊢ 2 * (m * HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n + 1) * m

Tactic:
have : 2 * (m * 2 ^ n) = 2 ^ (n + 1) * m := by
      rw [Nat.mul_comm, Nat.mul_assoc, ← Nat.pow_succ]; simp
-- Module: Mathlib.Data.Nat.Bits
Goal:
m n : ℕ
this : 2 * (m * HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n + 1) * m
⊢ shiftLeft' false m (n + 1) = m <<< (n + 1)

Tactic:
simp [shiftLeft_eq, shiftLeft', bit_val, shiftLeft'_false, this]

Premises used: Nat.shiftLeft_eq, Nat.shiftLeft', Nat.bit_val
-- Module: Mathlib.Data.Nat.Bits
Goal:
m n : ℕ
⊢ m.shiftRight n = m >>> n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
h : n ≠ 0
⊢ n.div2 < n

Tactic:
grind
-- Module: Mathlib.Data.Nat.Bits
Goal:
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
rw : shiftLeft' b m (n - k) = HShiftRight.hShiftRight (β := ℕ) (bit b (shiftLeft' b m n)) 1 >>> k
⊢ shiftLeft' b m (n + 1 - (k + 1)) = shiftLeft' b m (n + 1) >>> (k + 1)

Tactic:
rw [succ_sub_succ_eq_sub, shiftLeft', Nat.add_comm, shiftRight_add]

Premises used: Nat.shiftRight_add, Nat.shiftLeft', Nat.succ_sub_succ_eq_sub, Nat.add_comm
-- Module: Mathlib.Data.Nat.Bits
Goal:
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
simp : shiftLeft' b m n >>> k = (bit b (shiftLeft' b m n) / 2) >>> k
⊢ shiftLeft' b m (n - k) = HShiftRight.hShiftRight (β := ℕ) (bit b (shiftLeft' b m n)) 1 >>> k

Tactic:
simp only [shiftLeft'_sub, Nat.le_of_succ_le_succ h, shiftRight_succ, shiftRight_zero]

Premises used: Nat.shiftRight_succ, Nat.shiftRight_zero, Nat.le_of_succ_le_succ
-- Module: Mathlib.Data.Nat.Bits
Goal:
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftLeft' b m n >>> k = (bit b (shiftLeft' b m n) / 2) >>> k

Tactic:
simp [← div2_val, div2_bit]

Premises used: Nat.div2_bit, Nat.div2_val
-- Module: Mathlib.Data.Nat.Bits
Goal:
x x_1 x_2 : ℕ
hk : x_2 ≤ x_1
⊢ x <<< (x_1 - x_2) = x <<< x_1 >>> x_2

Tactic:
simp only [← shiftLeft'_false, shiftLeft'_sub false _ hk]

Premises used: Nat.shiftLeft'_false, Nat.shiftLeft'_sub, Bool.false
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
⊢ (n + 2).bodd = (1 &&& n + 2 != 0)

Tactic:
simpa using bodd_eq_one_and_ne_zero n
-- Module: Mathlib.Data.Nat.Bits
Goal:
m : ℕ
b : Bool
n : ℕ
simp : (bit b n / HPow.hPow (α := ℕ) (β := ℕ) 2 1 / HPow.hPow (α := ℕ) 2 m).bodd = (n / HPow.hPow (α := ℕ) 2 m).bodd
⊢ (HShiftRight.hShiftRight (β := ℕ) (bit b n) 1 >>> m).bodd = (n >>> m).bodd

Tactic:
simp only [shiftRight_eq_div_pow]

Premises used: Nat.shiftRight_eq_div_pow
-- Module: Mathlib.Data.Nat.Bits
Goal:
m : ℕ
b : Bool
n : ℕ
⊢ (bit b n / HPow.hPow (α := ℕ) (β := ℕ) 2 1 / HPow.hPow (α := ℕ) 2 m).bodd = (n / HPow.hPow (α := ℕ) 2 m).bodd

Tactic:
simp [← div2_val, div2_bit]

Premises used: Nat.div2_bit, Nat.div2_val
-- Module: Mathlib.Data.Nat.Bits
Goal:
m : ℕ
b : Bool
n : ℕ
⊢ (HShiftRight.hShiftRight (β := ℕ) (bit b n) 1 >>> m).bodd = (n >>> m).bodd

Tactic:
have : bodd (((bit b n) >>> 1) >>> m) = bodd (n >>> m) := by
    simp only [shiftRight_eq_div_pow]
    simp [← div2_val, div2_bit]
-- Module: Mathlib.Data.Nat.Bits
Goal:
m : ℕ
b : Bool
n : ℕ
this : (HShiftRight.hShiftRight (β := ℕ) (bit b n) 1 >>> m).bodd = (n >>> m).bodd
⊢ (bit b n >>> (m + 1)).bodd = (n >>> m).bodd

Tactic:
rw [← shiftRight_add, Nat.add_comm] at this

Premises used: Nat.shiftRight_add, Nat.add_comm
-- Module: Mathlib.Data.Nat.Bits
Goal:
m : ℕ
b : Bool
n : ℕ
this : (bit b n >>> (m + 1)).bodd = (n >>> m).bodd
⊢ (1 &&& bit b n >>> (m + 1) != 0) = (1 &&& n >>> m != 0)

Tactic:
simp only [bodd_eq_one_and_ne_zero] at this

Premises used: Nat.bodd_eq_one_and_ne_zero
-- Module: Mathlib.Data.Nat.Bits
Goal:
m : ℕ
b : Bool
n : ℕ
this : (1 &&& bit b n >>> (m + 1) != 0) = (1 &&& n >>> m != 0)
⊢ (bit b n).testBit m.succ = n.testBit m

Tactic:
this

Premises used: Nat.testBit
-- Module: Mathlib.Data.Nat.Bits
Goal:
m : ℕ
b : Bool
n : ℕ
this : (1 &&& bit b n >>> (m + 1) != 0) = (1 &&& n >>> m != 0)
⊢ (bit b n).testBit m.succ = n.testBit m

Tactic:
exact this
-- Module: Mathlib.Data.Nat.Bits
Goal:
⊢ boddDiv2 0 = (bodd 0, div2 0)

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
ih : n.boddDiv2 = (n.bodd, n.div2)
succ :
  (match (motive := Bool × ℕ → Bool × ℕ) (n.bodd, n.div2) with
    | (false, m) => (true, m)
    | (true, m) => (false, m.succ)) =
    ((n + 1).bodd, (n + 1).div2)
⊢ (n + 1).boddDiv2 = ((n + 1).bodd, (n + 1).div2)

Tactic:
rw [boddDiv2, ih]

Premises used: Nat.boddDiv2
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
ih : n.boddDiv2 = (n.bodd, n.div2)
succ :
  ∀ (hn : n.bodd = false),
    (match (motive := Bool × ℕ → Bool × ℕ) (false, n.div2) with
      | (false, m) => (true, m)
      | (true, m) => (false, m.succ)) =
      ((n + 1).bodd, (n + 1).div2)
succ₁ :
  ∀ (hn : n.bodd = true),
    (match (motive := Bool × ℕ → Bool × ℕ) (true, n.div2) with
      | (false, m) => (true, m)
      | (true, m) => (false, m.succ)) =
      ((n + 1).bodd, (n + 1).div2)
⊢ (match (motive := Bool × ℕ → Bool × ℕ) (n.bodd, n.div2) with
    | (false, m) => (true, m)
    | (true, m) => (false, m.succ)) =
    ((n + 1).bodd, (n + 1).div2)

Tactic:
cases hn : n.bodd

Premises used: Nat.bodd
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
ih : n.boddDiv2 = (n.bodd, n.div2)
hn : n.bodd = false
⊢ (match (motive := Bool × ℕ → Bool × ℕ) (false, n.div2) with
    | (false, m) => (true, m)
    | (true, m) => (false, m.succ)) =
    ((n + 1).bodd, (n + 1).div2)

Tactic:
simp [hn]
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
ih : n.boddDiv2 = (n.bodd, n.div2)
hn : n.bodd = true
⊢ (match (motive := Bool × ℕ → Bool × ℕ) (true, n.div2) with
    | (false, m) => (true, m)
    | (true, m) => (false, m.succ)) =
    ((n + 1).bodd, (n + 1).div2)

Tactic:
simp [hn]
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
zero : boddDiv2 0 = (bodd 0, div2 0)
succ : ∀ (n : ℕ) (ih : n.boddDiv2 = (n.bodd, n.div2)), (n + 1).boddDiv2 = ((n + 1).bodd, (n + 1).div2)
⊢ n.boddDiv2 = (n.bodd, n.div2)

Tactic:
induction n with
  | zero => rfl
  | succ n ih =>
    rw [boddDiv2, ih]
    cases hn : n.bodd <;> simp [hn]

Premises used: Nat.zero, Nat.boddDiv2, Nat.bodd, Nat.succ
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
⊢ (2 * n).div2 = n

Tactic:
div2_bit false n

Premises used: cond, Nat.bit, Nat.div2_bit, Bool.false
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
⊢ (2 * n + 1).div2 = n

Tactic:
div2_bit true n

Premises used: cond, Nat.bit, Nat.div2_bit, Bool.true
-- Module: Mathlib.Data.Nat.Bits
Goal:
x x_1 : ℕ
⊢ 2 * (x + x_1) + 1 = 2 * x + (2 * x_1 + 1)

Tactic:
lia
-- Module: Mathlib.Data.Nat.Bits
Goal:
x x_1 : ℕ
⊢ 2 * (x + x_1) = 2 * x + 2 * x_1

Tactic:
lia
-- Module: Mathlib.Data.Nat.Bits
Goal:
x x_1 : ℕ
⊢ 2 * (x + x_1) + 1 = 2 * x + 1 + 2 * x_1

Tactic:
lia
-- Module: Mathlib.Data.Nat.Bits
Goal:
b : Bool
n : ℕ
h : n ≠ 0
false : bit Bool.false n ≠ 0
true : bit Bool.true n ≠ 0
⊢ bit b n ≠ 0

Tactic:
cases b
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
h : n ≠ 0
⊢ ¬2 * n = 0

Tactic:
lia
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
h : n ≠ 0
⊢ ¬2 * n + 1 = 0

Tactic:
lia
-- Module: Mathlib.Data.Nat.Bits
Goal:
motive : ℕ → Sort u
H : (b : Bool) → (n : ℕ) → motive (bit b n)
n : ℕ
⊢ bitCasesOn (motive := motive) (2 * n) H = H false n

Tactic:
bitCasesOn_bit H false n

Premises used: cond, Nat.bit, Nat.bitCasesOn_bit, Bool.false
-- Module: Mathlib.Data.Nat.Bits
Goal:
motive : ℕ → Sort u
H : (b : Bool) → (n : ℕ) → motive (bit b n)
n : ℕ
⊢ bitCasesOn (motive := motive) (2 * n + 1) H = H true n

Tactic:
bitCasesOn_bit H true n

Premises used: cond, Nat.bit, Nat.bitCasesOn_bit, Bool.true
-- Module: Mathlib.Data.Nat.Bits
Goal:
motive : ℕ → Sort u
H₁ H₂ : (b : Bool) → (n : ℕ) → motive (bit b n)
h :
  Eq.{u} (α := (n : ℕ) → motive n)
    ((fun (H : (b : Bool) → (n : ℕ) → motive (bit b n)) (n : ℕ) ↦ bitCasesOn (motive := motive) n H) H₁)
    ((fun (H : (b : Bool) → (n : ℕ) → motive (bit b n)) (n : ℕ) ↦ bitCasesOn (motive := motive) n H) H₂)
h₁ : ∀ (b : Bool) (n : ℕ), H₁ b n = H₂ b n
⊢ H₁ = H₂

Tactic:
ext b n
-- Module: Mathlib.Data.Nat.Bits
Goal:
motive : ℕ → Sort u
H₁ H₂ : (b : Bool) → (n : ℕ) → motive (bit b n)
h :
  Eq.{u} (α := (n : ℕ) → motive n)
    ((fun (H : (b : Bool) → (n : ℕ) → motive (bit b n)) (n : ℕ) ↦ bitCasesOn (motive := motive) n H) H₁)
    ((fun (H : (b : Bool) → (n : ℕ) → motive (bit b n)) (n : ℕ) ↦ bitCasesOn (motive := motive) n H) H₂)
b : Bool
n : ℕ
⊢ H₁ b n = H₂ b n

Tactic:
simpa only [bitCasesOn_bit] using congr_fun h (bit b n)

Premises used: Nat.bit, Nat.bitCasesOn_bit, congr_fun
-- Module: Mathlib.Data.Nat.Bits
Goal:
motive : ℕ → Sort u
H₁ H₂ : (b : Bool) → (n : ℕ) → motive (bit b n)
⊢ (Eq.{u} (α := (n : ℕ) → motive n) (fun (n : ℕ) ↦ bitCasesOn (motive := motive) n H₁) fun (n : ℕ) ↦
      bitCasesOn (motive := motive) n H₂) ↔
    H₁ = H₂

Tactic:
bit_cases_on_injective.eq_iff

Premises used: Nat.bit_cases_on_injective, Function.Injective.eq_iff
-- Module: Mathlib.Data.Nat.Bits
Goal:
x x_1 : ℕ
h : x ≤ x_1
⊢ 2 * x + 1 ≤ 2 * x_1 + 1

Tactic:
lia
-- Module: Mathlib.Data.Nat.Bits
Goal:
x x_1 : ℕ
h : x ≤ x_1
⊢ 2 * x ≤ 2 * x_1

Tactic:
lia
-- Module: Mathlib.Data.Nat.Bits
Goal:
m n : ℕ
a b : Bool
h : m < n
false : bit Bool.false m < 2 * n
true : bit Bool.true m < 2 * n
⊢ bit a m < 2 * n

Tactic:
cases a
-- Module: Mathlib.Data.Nat.Bits
Goal:
m n : ℕ
b : Bool
h : m < n
⊢ 2 * m < 2 * n

Tactic:
lia
-- Module: Mathlib.Data.Nat.Bits
Goal:
m n : ℕ
b : Bool
h : m < n
⊢ 2 * m + 1 < 2 * n

Tactic:
lia
-- Module: Mathlib.Data.Nat.Bits
Goal:
m n : ℕ
a b : Bool
h : m < n
false : 2 * n ≤ bit Bool.false n
true : 2 * n ≤ bit Bool.true n
⊢ 2 * n ≤ bit b n

Tactic:
cases b
-- Module: Mathlib.Data.Nat.Bits
Goal:
m n : ℕ
a : Bool
h : m < n
⊢ 2 * n ≤ 2 * n

Tactic:
lia
-- Module: Mathlib.Data.Nat.Bits
Goal:
m n : ℕ
a : Bool
h : m < n
⊢ 2 * n ≤ 2 * n + 1

Tactic:
lia
-- Module: Mathlib.Data.Nat.Bits
Goal:
⊢ bits 0 = []

Tactic:
simp [Nat.bits]

Premises used: Nat.bits
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
b : Bool
hn : n = 0 → b = true
h : [false] = [] ∨ (n = 0 → b = true)
⊢ (bit b n).bits = b :: n.bits

Tactic:
rw [Nat.bits, Nat.bits, binaryRec_eq]

Premises used: Nat.bits, Nat.binaryRec_eq
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
b : Bool
hn : n = 0 → b = true
⊢ [false] = [] ∨ (n = 0 → b = true)

Tactic:
simpa
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
hn : n ≠ 0
⊢ (2 * n).bits = false :: n.bits

Tactic:
bits_append_bit n false fun hn' => absurd hn' hn

Premises used: cond, Nat.bit, Nat.bits_append_bit, absurd, Bool.false
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
⊢ (2 * n + 1).bits = true :: n.bits

Tactic:
bits_append_bit n true fun _ => rfl

Premises used: cond, Nat.bit, Bool.true, Nat.bits_append_bit, rfl
-- Module: Mathlib.Data.Nat.Bits
Goal:
⊢ bits 1 = [true]

Tactic:
bit1_bits 0

Premises used: WellFounded.Nat.fix, Nat.bits, Nat.bit1_bits, dite, WellFounded.Nat.fix.go, OfNat.ofNat, Nat.binaryRec
-- Module: Mathlib.Data.Nat.Bits
Goal:
⊢ bodd 0 = (bits 0).headI

Tactic:
simp
-- Module: Mathlib.Data.Nat.Bits
Goal:
b : Bool
n : ℕ
h : n = 0 → b = true
h_1 : n.bodd = n.bits.headI
⊢ (bit b n).bodd = (bit b n).bits.headI

Tactic:
simp [bodd_bit, bits_append_bit _ _ h]

Premises used: Nat.bodd_bit, Nat.bits_append_bit
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
zero : bodd 0 = (bits 0).headI
bit : ∀ (b : Bool) (n : ℕ) (h : n = 0 → b = true), n.bodd = n.bits.headI → (Nat.bit b n).bodd = (Nat.bit b n).bits.headI
⊢ n.bodd = n.bits.headI

Tactic:
induction n using Nat.binaryRec' with
  | zero => simp
  | bit _ _ h => simp [bodd_bit, bits_append_bit _ _ h]

Premises used: Nat.bit, Nat.bodd_bit, Nat.zero
-- Module: Mathlib.Data.Nat.Bits
Goal:
⊢ (div2 0).bits = (bits 0).tail

Tactic:
simp
-- Module: Mathlib.Data.Nat.Bits
Goal:
b : Bool
n : ℕ
h : n = 0 → b = true
h_1 : n.div2.bits = n.bits.tail
⊢ (bit b n).div2.bits = (bit b n).bits.tail

Tactic:
simp [div2_bit, bits_append_bit _ _ h]

Premises used: Nat.div2_bit, Nat.bits_append_bit
-- Module: Mathlib.Data.Nat.Bits
Goal:
n : ℕ
zero : (div2 0).bits = (bits 0).tail
bit :
  ∀ (b : Bool) (n : ℕ) (h : n = 0 → b = true),
    n.div2.bits = n.bits.tail → (Nat.bit b n).div2.bits = (Nat.bit b n).bits.tail
⊢ n.div2.bits = n.bits.tail

Tactic:
induction n using Nat.binaryRec' with
  | zero => simp
  | bit _ _ h => simp [div2_bit, bits_append_bit _ _ h]

Premises used: Nat.bit, Nat.div2_bit, Nat.zero
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
m : ℕ
⊢ bitwise f 0 m = if f false true = true then m else 0

Tactic:
simp [bitwise]

Premises used: Nat.bitwise
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
n : ℕ
unfold :
  (if n = 0 then if f false true = true then 0 else 0
    else
      if Eq (α := ℕ) 0 0 then if f true false = true then n else 0
      else
        have n' := n / 2;
        have m' := 0 / 2;
        let b₁ := n % 2 = 1;
        let b₂ := HMod.hMod (α := ℕ) 0 2 = 1;
        have r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    if f true false = true then n else 0
⊢ bitwise f n 0 = if f true false = true then n else 0

Tactic:
unfold bitwise

Premises used: Nat.bitwise
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
n : ℕ
simp : n = 0 → 0 = if f true false = true then n else 0
⊢ (if n = 0 then if f false true = true then 0 else 0
    else
      if Eq (α := ℕ) 0 0 then if f true false = true then n else 0
      else
        have n' := n / 2;
        have m' := 0 / 2;
        let b₁ := n % 2 = 1;
        let b₂ := HMod.hMod (α := ℕ) 0 2 = 1;
        have r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    if f true false = true then n else 0

Tactic:
simp only [ite_self, Nat.zero_div, ite_true, ite_eq_right_iff]

Premises used: ite_self, Nat.zero_div, ite_true, ite_eq_right_iff
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
pos : f true false = true → Eq (α := ℕ) 0 0
neg : ¬f true false = true → Eq (α := ℕ) 0 0
⊢ Eq (α := ℕ) 0 (if f true false = true then 0 else 0)

Tactic:
split_ifs
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f true false = true
⊢ Eq (α := ℕ) 0 0

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : ¬f true false = true
⊢ Eq (α := ℕ) 0 0

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
⊢ bitwise f 0 0 = 0

Tactic:
simp only [bitwise_zero_right, ite_self]

Premises used: ite_self, Nat.bitwise_zero_right
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
unfold :
  if n = 0 then if f false true = true then m else 0
  else
    if m = 0 then if f true false = true then n else 0
    else
      have n' := n / 2;
      have m' := m / 2;
      let b₁ := n % 2 = 1;
      let b₂ := m % 2 = 1;
      have r := bitwise f n' m';
      if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r
| bitwise f n m

Tactic:
unfold bitwise

Premises used: Nat.bitwise
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
conv_lhs :
  (if n = 0 then if f false true = true then m else 0
    else
      if m = 0 then if f true false = true then n else 0
      else
        have n' := n / 2;
        have m' := m / 2;
        let b₁ := n % 2 = 1;
        let b₂ := m % 2 = 1;
        have r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    bit (f n.bodd m.bodd) (bitwise f (n / 2) (m / 2))
⊢ bitwise f n m = bit (f n.bodd m.bodd) (bitwise f (n / 2) (m / 2))

Tactic:
conv_lhs => unfold bitwise

Premises used: Nat.bitwise
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
x : ℕ
simp : decide (x.bodd.toNat = 1) = x.bodd
⊢ decide (x % 2 = 1) = x.bodd

Tactic:
simp only [mod_two_of_bodd]

Premises used: Nat.mod_two_of_bodd
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
x : ℕ
false : decide (Bool.false.toNat = 1) = Bool.false
true : decide (Bool.true.toNat = 1) = Bool.true
⊢ decide (x.bodd.toNat = 1) = x.bodd

Tactic:
cases bodd x

Premises used: Nat.bodd
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
x : ℕ
⊢ decide (false.toNat = 1) = false

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
x : ℕ
⊢ decide (true.toNat = 1) = true

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
⊢ ∀ (x : ℕ), decide (x % 2 = 1) = x.bodd

Tactic:
have mod_two_iff_bod x : (x % 2 = 1 : Bool) = bodd x := by
    simp only [mod_two_of_bodd]; cases bodd x <;> rfl
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
mod_two_iff_bod : ∀ (x : ℕ), decide (x % 2 = 1) = x.bodd
⊢ (if n = 0 then if f false true = true then m else 0
    else
      if m = 0 then if f true false = true then n else 0
      else
        have n' := n / 2;
        have m' := m / 2;
        let b₁ := n % 2 = 1;
        let b₂ := m % 2 = 1;
        have r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    bit (f n.bodd m.bodd) (bitwise f (n / 2) (m / 2))

Tactic:
simp [hn, hm, mod_two_iff_bod, bit, two_mul]

Premises used: Nat.bit, two_mul
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
n : ℕ
h : n ≠ 0
rw :
  Eq.{u_1} (α := C n)
    (cast (α := C (bit (n.testBit 0) (HShiftRight.hShiftRight (β := ℕ) n 1))) ⋯
        (f (1 &&& n != 0) (HShiftRight.hShiftRight (β := ℕ) n 1)
          (binaryRec (motive := fun (x : ℕ) ↦ C x) z f (HShiftRight.hShiftRight (β := ℕ) n 1))) :
      C n)
    (cast (α := C (bit n.bodd n.div2)) ⋯ (f n.bodd n.div2 (binaryRec (motive := fun (x : ℕ) ↦ C x) z f n.div2)) : C n)
⊢ binaryRec (motive := fun (x : ℕ) ↦ C x) z f n =
    Eq.rec (motive := fun (x : ℕ) (h : bit n.bodd n.div2 = x) ↦ C x)
      (f n.bodd n.div2 (binaryRec (motive := fun (x : ℕ) ↦ C x) z f n.div2)) ⋯

Tactic:
rw [binaryRec, dif_neg h, eqRec_eq_cast, eqRec_eq_cast]

Premises used: eqRec_eq_cast, dif_neg
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
C : ℕ → Sort u_1
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
n : ℕ
h : n ≠ 0
⊢ Eq.{u_1} (α := C n)
    (cast (α := C (bit (n.testBit 0) (HShiftRight.hShiftRight (β := ℕ) n 1))) ⋯
        (f (1 &&& n != 0) (HShiftRight.hShiftRight (β := ℕ) n 1)
          (binaryRec (motive := fun (x : ℕ) ↦ C x) z f (HShiftRight.hShiftRight (β := ℕ) n 1))) :
      C n)
    (cast (α := C (bit n.bodd n.div2)) ⋯ (f n.bodd n.div2 (binaryRec (motive := fun (x : ℕ) ↦ C x) z f n.div2)) : C n)

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
unfold :
  if bit a m = 0 then if f false true = true then bit b n else 0
  else
    if bit b n = 0 then if f true false = true then bit a m else 0
    else
      have n' := bit a m / 2;
      have m' := bit b n / 2;
      let b₁ := bit a m % 2 = 1;
      let b₂ := bit b n % 2 = 1;
      have r := bitwise f n' m';
      if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r
| bitwise f (bit a m) (bit b n)

Tactic:
unfold bitwise

Premises used: Nat.bitwise
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
conv_lhs :
  (if bit a m = 0 then if f false true = true then bit b n else 0
    else
      if bit b n = 0 then if f true false = true then bit a m else 0
      else
        have n' := bit a m / 2;
        have m' := bit b n / 2;
        let b₁ := bit a m % 2 = 1;
        let b₂ := bit b n % 2 = 1;
        have r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    bit (f a b) (bitwise f m n)
⊢ bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n)

Tactic:
conv_lhs => unfold bitwise

Premises used: Nat.bitwise
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
simp :
  (if (if a = true then 2 * m + 1 else 2 * m) = 0 then
      if f false true = true then if b = true then 2 * n + 1 else 2 * n else 0
    else
      if (if b = true then 2 * n + 1 else 2 * n) = 0 then
        if f true false = true then if a = true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if a = true then 2 * m + 1 else 2 * m) % 2 = 1))
                (decide ((if b = true then 2 * n + 1 else 2 * n) % 2 = 1)) =
              true then
          bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) +
            1
        else
          bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if a = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2)) =
    if f a b = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
⊢ (if bit a m = 0 then if f false true = true then bit b n else 0
    else
      if bit b n = 0 then if f true false = true then bit a m else 0
      else
        have n' := bit a m / 2;
        have m' := bit b n / 2;
        let b₁ := bit a m % 2 = 1;
        let b₂ := bit b n % 2 = 1;
        have r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    bit (f a b) (bitwise f m n)

Tactic:
simp only [bit, Bool.cond_eq_ite]

Premises used: Nat.bit, Bool.cond_eq_ite
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n x : ℕ
rw : (1 + 2 * x) / 2 = x
⊢ (x + x + 1) / 2 = x

Tactic:
rw [← two_mul, add_comm]

Premises used: two_mul, add_comm
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n x : ℕ
⊢ (1 + 2 * x) / 2 = x

Tactic:
simp [add_mul_div_left]

Premises used: Nat.add_mul_div_left