awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
y : ℕ
⊢ bitwise f 0 y =
    binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
      (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
        binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
          (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
      0 y

Tactic:
simp only [bitwise_zero_left, binaryRec_zero, Bool.cond_eq_ite]

Premises used: Nat.bitwise_zero_left, Nat.binaryRec_zero, Bool.cond_eq_ite
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
xb : Bool
x : ℕ
hxb : x = 0 → xb = true
ih :
  ∀ (y : ℕ),
    bitwise f x y =
      binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
        (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
          binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
            (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
        x y
y : ℕ
h :
  ∀ (hxb : bit xb x ≠ 0)
    (ih :
      ∀ (y : ℕ),
        bitwise f x y =
          binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
            (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
              binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
                (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
            x y)
    (y : ℕ),
    bitwise f (bit xb x) y =
      binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
        (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
          binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
            (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
        (bit xb x) y
⊢ bitwise f (bit xb x) y =
    binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
      (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
        binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
          (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
      (bit xb x) y

Tactic:
rw [← bit_ne_zero_iff] at hxb

Premises used: Nat.bit_ne_zero_iff
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
xb : Bool
x : ℕ
hxb : bit xb x ≠ 0
ih :
  ∀ (y : ℕ),
    bitwise f x y =
      binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
        (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
          binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
            (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
        x y
y : ℕ
h :
  bitwise f (bit xb x) y =
    binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit xb x else 0)
      (fun (b : Bool) (n x_1 : ℕ) ↦
        bit (f xb b)
          (binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
            (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
              binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
                (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
            x n))
      y
⊢ bitwise f (bit xb x) y =
    binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
      (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
        binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
          (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
      (bit xb x) y

Tactic:
simp_rw [binaryRec_of_ne_zero _ _ hxb, bodd_bit, div2_bit, eq_rec_constant]

Premises used: Nat.bodd_bit, Nat.div2_bit, Nat.binaryRec_of_ne_zero, eq_rec_constant
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
xb : Bool
x : ℕ
hxb : bit xb x ≠ 0
ih :
  ∀ (y : ℕ),
    bitwise f x y =
      binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
        (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
          binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
            (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
        x y
⊢ bitwise f (bit xb x) 0 =
    binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit xb x else 0)
      (fun (b : Bool) (n x_1 : ℕ) ↦
        bit (f xb b)
          (binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
            (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
              binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
                (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
            x n))
      0

Tactic:
simp only [bitwise_zero_right, binaryRec_zero, Bool.cond_eq_ite]

Premises used: Nat.binaryRec_zero, Nat.bitwise_zero_right, Bool.cond_eq_ite
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
xb : Bool
x : ℕ
hxb : bit xb x ≠ 0
ih :
  ∀ (y : ℕ),
    bitwise f x y =
      binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
        (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
          binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
            (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
        x y
yb : Bool
y : ℕ
hyb : y = 0 → yb = true
h :
  bitwise f (bit xb x) y =
    binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit xb x else 0)
      (fun (b : Bool) (n x_1 : ℕ) ↦
        bit (f xb b)
          (binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
            (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
              binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
                (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
            x n))
      y
⊢ bit yb y ≠ 0

Tactic:
rw [← bit_ne_zero_iff] at hyb

Premises used: Nat.bit_ne_zero_iff
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
xb : Bool
x : ℕ
hxb : bit xb x ≠ 0
ih :
  ∀ (y : ℕ),
    bitwise f x y =
      binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
        (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
          binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
            (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
        x y
yb : Bool
y : ℕ
hyb : y = 0 → yb = true
h :
  bitwise f (bit xb x) y =
    binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit xb x else 0)
      (fun (b : Bool) (n x_1 : ℕ) ↦
        bit (f xb b)
          (binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
            (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
              binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
                (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
            x n))
      y
hyb₁ : bit yb y ≠ 0
⊢ bitwise f (bit xb x) y =
    binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit xb x else 0)
      (fun (b : Bool) (n x_1 : ℕ) ↦
        bit (f xb b)
          (binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
            (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
              binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
                (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
            x n))
      y

Tactic:
rw [← bit_ne_zero_iff] at hyb

Premises used: Nat.bit_ne_zero_iff
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
x y : ℕ
h :
  ∀ (y : ℕ),
    bitwise f 0 y =
      binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
        (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
          binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
            (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
        0 y
h₁ :
  ∀ (xb : Bool) (x : ℕ) (hxb : x = 0 → xb = true)
    (ih :
      ∀ (y : ℕ),
        bitwise f x y =
          binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
            (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
              binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
                (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
            x y)
    (y : ℕ),
    bitwise f (bit xb x) y =
      binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
        (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
          binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
            (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
        (bit xb x) y
⊢ bitwise f x y =
    binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
      (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
        binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
          (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
      x y

Tactic:
induction x using binaryRec' generalizing y with
  | zero => simp only [bitwise_zero_left, binaryRec_zero, Bool.cond_eq_ite]
  | bit xb x hxb ih =>
    rw [← bit_ne_zero_iff] at hxb
    simp_rw [binaryRec_of_ne_zero _ _ hxb, bodd_bit, div2_bit, eq_rec_constant]
    induction y using binaryRec' with
    | zero => simp only [bitwise_zero_right, binaryRec_zero, Bool.cond_eq_ite]
    | bit yb y hyb =>
      rw [← bit_ne_zero_iff] at hyb
      simp_rw [binaryRec_of_ne_zero _ _ hyb, bitwise_of_ne_zero hxb hyb, bodd_bit, div2_bit,
        bit_div_two, eq_rec_constant, ih]

Premises used: Nat.bit, Nat.bodd_bit, Nat.div2_bit, Nat.bit_div_two, Nat.bitwise_zero_left, Nat.binaryRec_zero, Nat.zero, eq_rec_constant, Nat.bitwise_zero_right, Nat.bit_ne_zero_iff, Bool.cond_eq_ite
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
h : ∀ (i : ℕ), testBit 0 i = false
⊢ Eq (α := ℕ) 0 0

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
b : Bool
n : ℕ
hn : ∀ (h : ∀ (i : ℕ), n.testBit i = false), n = 0
h : ∀ (i : ℕ), (bit b n).testBit i = false
⊢ bit b n = 0

Tactic:
?_
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n : ℕ
h : ∀ (i : ℕ), n.testBit i = false
bit :
  ∀ (b : Bool) (n : ℕ) (hn : ∀ (h : ∀ (i : ℕ), n.testBit i = false), n = 0)
    (h : ∀ (i : ℕ), (Nat.bit b n).testBit i = false), Nat.bit b n = 0
⊢ n = 0

Tactic:
induction n using Nat.binaryRec with | zero => rfl | bit b n hn => ?_

Premises used: Nat.bit, Nat.zero
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
b : Bool
n : ℕ
hn : ∀ (h : ∀ (i : ℕ), n.testBit i = false), n = 0
h : ∀ (i : ℕ), (bit b n).testBit i = false
⊢ b = false

Tactic:
simpa using h 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
b : Bool
n : ℕ
hn : ∀ (h : ∀ (i : ℕ), n.testBit i = false), n = 0
h : ∀ (i : ℕ), (bit b n).testBit i = false
⊢ b = false

Tactic:
have : b = false := by simpa using h 0
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
b : Bool
n : ℕ
hn : ∀ (h : ∀ (i : ℕ), n.testBit i = false), n = 0
h : ∀ (i : ℕ), (bit b n).testBit i = false
this : b = false
i : ℕ
rw : n.testBit i = (bit b n).testBit (i + 1)
rw₁ rw₂ : n.testBit i = n.testBit i
⊢ n.testBit i = false

Tactic:
rw [← h (i + 1), testBit_bit_succ]

Premises used: HAdd.hAdd, Nat.testBit_bit_succ, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
b : Bool
n : ℕ
hn : ∀ (h : ∀ (i : ℕ), n.testBit i = false), n = 0
h : ∀ (i : ℕ), (Nat.bit b n).testBit i = false
this : b = false
bit : Nat.bit false n = 0
bit₁ : Eq (α := ℕ) ((fun (x : ℕ) ↦ 2 * x) n) 0
bit₂ bit₃ : Eq (α := ℕ) ((fun (x : ℕ) ↦ 2 * x) 0) 0
⊢ Nat.bit b n = 0

Tactic:
rw [this, bit_false, hn fun i => by rw [← h (i + 1), testBit_bit_succ]]

Premises used: Nat.bit_false
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n i : ℕ
h : n < HPow.hPow (α := ℕ) 2 i
⊢ n.testBit i = false

Tactic:
simp [testBit, shiftRight_eq_div_pow, Nat.div_eq_of_lt h]

Premises used: Nat.testBit, Nat.div_eq_of_lt, Nat.shiftRight_eq_div_pow
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n : ℕ
zero : (n.bits.headI.toNat != 0) = n.bits.headI
⊢ n.testBit 0 = n.bits.getI 0

Tactic:
simp only [testBit, shiftRight_zero, one_and_eq_mod_two, mod_two_of_bodd,
      bodd_eq_bits_head, List.getI_zero_eq_headI]

Premises used: List.getI_zero_eq_headI, Nat.shiftRight_zero, Nat.one_and_eq_mod_two, Nat.testBit, Nat.bodd_eq_bits_head, Nat.mod_two_of_bodd
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n : ℕ
zero : (false.toNat != 0) = false
zero₁ : (true.toNat != 0) = true
⊢ (n.bits.headI.toNat != 0) = n.bits.headI

Tactic:
cases List.headI (bits n)

Premises used: Nat.bits, List.headI
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n : ℕ
⊢ (false.toNat != 0) = false

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n : ℕ
⊢ (true.toNat != 0) = true

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
rw : (bit n.bodd n.div2).testBit (i + 1)
| n.testBit (i + 1)

Tactic:
rw [← bit_bodd_div2 n]

Premises used: Nat.bit_bodd_div2
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
succ : (bit n.bodd n.div2).testBit (i + 1) = n.bits.getI (i + 1)
⊢ n.testBit (i + 1) = n.bits.getI (i + 1)

Tactic:
conv_lhs => rw [← bit_bodd_div2 n]

Premises used: Nat.bit_bodd_div2
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
succ : n.bits.tail.getI i = n.bits.getI (i + 1)
⊢ (bit n.bodd n.div2).testBit (i + 1) = n.bits.getI (i + 1)

Tactic:
rw [testBit_bit_succ, ih n.div2, div2_bits_eq_tail]

Premises used: Nat.div2, Nat.testBit_bit_succ, Nat.div2_bits_eq_tail
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
succ : Eq (α := Bool) (List.getI (List.tail []) i) (List.getI [] (i + 1))
succ₁ : ∀ (head : Bool) (tail : List Bool), (head :: tail).tail.getI i = (head :: tail).getI (i + 1)
⊢ n.bits.tail.getI i = n.bits.getI (i + 1)

Tactic:
cases n.bits

Premises used: Nat.bits
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
⊢ Eq (α := Bool) (List.getI (List.tail []) i) (List.getI [] (i + 1))

Tactic:
simp
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
head : Bool
tail : List Bool
⊢ (head :: tail).tail.getI i = (head :: tail).getI (i + 1)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n i : ℕ
zero : ∀ (n : ℕ), n.testBit 0 = n.bits.getI 0
succ : ∀ (i : ℕ) (ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i) (n : ℕ), n.testBit (i + 1) = n.bits.getI (i + 1)
⊢ n.testBit i = n.bits.getI i

Tactic:
induction i generalizing n with
  | zero =>
    simp only [testBit, shiftRight_zero, one_and_eq_mod_two, mod_two_of_bodd,
      bodd_eq_bits_head, List.getI_zero_eq_headI]
    cases List.headI (bits n) <;> rfl
  | succ i ih =>
    conv_lhs => rw [← bit_bodd_div2 n]
    rw [testBit_bit_succ, ih n.div2, div2_bits_eq_tail]
    cases n.bits <;> simp

Premises used: Nat.bit_bodd_div2, Nat.bits, List.getI_zero_eq_headI, Nat.shiftRight_zero, Nat.one_and_eq_mod_two, Nat.testBit_bit_succ, Nat.testBit, Nat.zero, Nat.bodd_eq_bits_head, Nat.div2_bits_eq_tail, List.headI, Nat.mod_two_of_bodd, Nat.succ
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
h : Ne (α := ℕ) 0 0
⊢ ∃ (i : ℕ), testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false

Tactic:
False.elim (h rfl)

Premises used: False.elim, rfl
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
h : Ne (α := ℕ) 0 0
⊢ ∃ (i : ℕ), testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false

Tactic:
exact False.elim (h rfl)

Premises used: False.elim, rfl
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
b : Bool
n : ℕ
hn : ∀ (h : n ≠ 0), ∃ (i : ℕ), n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
⊢ ∃ (i : ℕ), (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false

Tactic:
?_
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n : ℕ
h : n ≠ 0
bit :
  ∀ (b : Bool) (n : ℕ) (hn : ∀ (h : n ≠ 0), ∃ (i : ℕ), n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false)
    (h : Nat.bit b n ≠ 0),
    ∃ (i : ℕ), (Nat.bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (Nat.bit b n).testBit j = false
⊢ ∃ (i : ℕ), n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false

Tactic:
induction n using Nat.binaryRec with | zero => exact False.elim (h rfl) | bit b n hn => ?_

Premises used: Nat.bit, False.elim, Nat.zero
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
b : Bool
n : ℕ
hn : ∀ (h : n ≠ 0), ∃ (i : ℕ), n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
pos : ∀ (h' : n = 0), ∃ (i : ℕ), (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false
neg : ∀ (h' : ¬n = 0), ∃ (i : ℕ), (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false
⊢ ∃ (i : ℕ), (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false

Tactic:
by_cases h' : n = 0
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
b : Bool
n : ℕ
hn : ∀ (h : n ≠ 0), ∃ (i : ℕ), n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : n = 0
pos :
  ∀ (hn : ∀ (h : Ne (α := ℕ) 0 0), ∃ (i : ℕ), testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false)
    (h : bit b 0 ≠ 0), ∃ (i : ℕ), (bit b 0).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b 0).testBit j = false
⊢ ∃ (i : ℕ), (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false

Tactic:
subst h'
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
b : Bool
hn : ∀ (h : Ne (α := ℕ) 0 0), ∃ (i : ℕ), testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
revert : ∀ (h : bit b 0 ≠ 0), b = true
⊢ b = true

Tactic:
revert h
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
b : Bool
hn : ∀ (h : Ne (α := ℕ) 0 0), ∃ (i : ℕ), testBit 0 i = Bool.true ∧ ∀ (j : ℕ), i < j → testBit 0 j = Bool.false
false : ∀ (h : bit Bool.false 0 ≠ 0), Bool.false = Bool.true
true : ∀ (h : bit Bool.true 0 ≠ 0), Bool.true = Bool.true
⊢ ∀ (h : bit b 0 ≠ 0), b = Bool.true

Tactic:
cases b
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
hn : ∀ (h : Ne (α := ℕ) 0 0), ∃ (i : ℕ), testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
⊢ ∀ (h : bit false 0 ≠ 0), false = true

Tactic:
simp
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
hn : ∀ (h : Ne (α := ℕ) 0 0), ∃ (i : ℕ), testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
⊢ ∀ (h : bit true 0 ≠ 0), true = true

Tactic:
simp
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
b : Bool
hn : ∀ (h : Ne (α := ℕ) 0 0), ∃ (i : ℕ), testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
pos : ∃ (i : ℕ), (bit true 0).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit true 0).testBit j = false
⊢ ∃ (i : ℕ), (bit b 0).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b 0).testBit j = false

Tactic:
rw [show b = true by
        revert h
        cases b <;> simp]
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
b : Bool
hn : ∀ (h : Ne (α := ℕ) 0 0), ∃ (i : ℕ), testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
rw rw₁ : true = true
⊢ (bit true 0).testBit 0 = true

Tactic:
rw [testBit_bit_zero]

Premises used: Nat.testBit_bit_zero
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
b : Bool
hn : ∀ (h : Ne (α := ℕ) 0 0), ∃ (i : ℕ), testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
pos : ∀ (j : ℕ) (hj : 0 < j), (bit true 0).testBit j = false
⊢ ∃ (i : ℕ), (bit true 0).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit true 0).testBit j = false

Tactic:
refine ⟨0, ⟨by rw [testBit_bit_zero], fun j hj => ?_⟩⟩
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
b : Bool
hn : ∀ (h : Ne (α := ℕ) 0 0), ∃ (i : ℕ), testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
j : ℕ
hj : 0 < j
pos : ∀ (j' : ℕ) (hj : 0 < j'.succ), (bit true 0).testBit j'.succ = false
⊢ (bit true 0).testBit j = false

Tactic:
obtain ⟨j', rfl⟩ := exists_eq_succ_of_ne_zero (ne_of_gt hj)

Premises used: Nat.exists_eq_succ_of_ne_zero, rfl, Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
b : Bool
hn : ∀ (h : Ne (α := ℕ) 0 0), ∃ (i : ℕ), testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
j' : ℕ
hj : 0 < j'.succ
pos : testBit 0 j' = false
pos₁ pos₂ : false = false
⊢ (bit true 0).testBit j'.succ = false

Tactic:
rw [testBit_bit_succ, zero_testBit]

Premises used: Nat.zero_testBit, Nat.testBit_bit_succ
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
b : Bool
n : ℕ
hn : ∀ (h : n ≠ 0), ∃ (i : ℕ), n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
neg :
  ∀ (k : ℕ) (hk : n.testBit k = true) (hk' : ∀ (j : ℕ), k < j → n.testBit j = false),
    ∃ (i : ℕ), (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false
⊢ ∃ (i : ℕ), (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false

Tactic:
obtain ⟨k, ⟨hk, hk'⟩⟩ := hn h'
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
b : Bool
n : ℕ
hn : ∀ (h : n ≠ 0), ∃ (i : ℕ), n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
rw : n.testBit k = true
rw₁ rw₂ : true = true
⊢ (bit b n).testBit (k + 1) = true

Tactic:
rw [testBit_bit_succ, hk]

Premises used: Nat.testBit_bit_succ
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
b : Bool
n : ℕ
hn : ∀ (h : n ≠ 0), ∃ (i : ℕ), n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
neg : ∀ (j : ℕ) (hj : k + 1 < j), (bit b n).testBit j = false
⊢ ∃ (i : ℕ), (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false

Tactic:
refine ⟨k + 1, ⟨by rw [testBit_bit_succ, hk], fun j hj => ?_⟩⟩
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
b : Bool
n : ℕ
hn : ∀ (h : n ≠ 0), ∃ (i : ℕ), n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
j : ℕ
hj : k + 1 < j
x : j = 0
⊢ k + 1 < 0

Tactic:
subst x
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
b : Bool
n : ℕ
hn : ∀ (h : n ≠ 0), ∃ (i : ℕ), n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
hj : k + 1 < 0
⊢ False

Tactic:
simp at hj
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
b : Bool
n : ℕ
hn : ∀ (h : n ≠ 0), ∃ (i : ℕ), n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
j : ℕ
hj : k + 1 < j
neg : ∀ (j' : ℕ) (hj : k + 1 < j'.succ), (bit b n).testBit j'.succ = false
⊢ (bit b n).testBit j = false

Tactic:
obtain ⟨j', rfl⟩ := exists_eq_succ_of_ne_zero (show j ≠ 0 by intro x; subst x; simp at hj)

Premises used: Nat.exists_eq_succ_of_ne_zero, rfl
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
b : Bool
n : ℕ
hn : ∀ (h : n ≠ 0), ∃ (i : ℕ), n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
j' : ℕ
hj : k + 1 < j'.succ
⊢ (bit b n).testBit j'.succ = false

Tactic:
(testBit_bit_succ _ _ _).trans (hk' _ (lt_of_succ_lt_succ hj))

Premises used: Nat.testBit_bit_succ, Eq.trans, Nat.lt_of_succ_lt_succ
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
b : Bool
n : ℕ
hn : ∀ (h : n ≠ 0), ∃ (i : ℕ), n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
j' : ℕ
hj : k + 1 < j'.succ
⊢ (bit b n).testBit j'.succ = false

Tactic:
exact (testBit_bit_succ _ _ _).trans (hk' _ (lt_of_succ_lt_succ hj))

Premises used: Nat.testBit_bit_succ, Eq.trans, Nat.lt_of_succ_lt_succ
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
m i : ℕ
hn : testBit 0 i = false
hm : m.testBit i = true
hnm : ∀ (j : ℕ), i < j → testBit 0 j = m.testBit j
zero : m ≠ 0
⊢ 0 < m

Tactic:
rw [Nat.pos_iff_ne_zero]

Premises used: Nat.pos_iff_ne_zero
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
i : ℕ
hn : testBit 0 i = false
hm : testBit 0 i = true
hnm : ∀ (j : ℕ), i < j → testBit 0 j = testBit 0 j
⊢ False

Tactic:
simp at hm