awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ 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
have 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
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]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n : ℕ
h : ∀ (i : ℕ), n.testBit i = false
⊢ n = 0
have bit : ∀ (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: induction n using Nat.binaryRec with | zero => rfl | bit b n hn => ?_
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (hypothesis)
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
have this : b = false
Tactic: have : b = false := by simpa using h 0
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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 : ℕ
⊢ n.testBit i = false
have rw : n.testBit i = (bit b n).testBit (i + 1)
Tactic: rw [← h (i + 1), testBit_bit_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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)
⊢ n.testBit i = false
have rw₁ : n.testBit i = n.testBit i
Tactic: rw [← h (i + 1), testBit_bit_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
b : Bool
n : ℕ
hn : ∀ (h : ∀ (i : ℕ), n.testBit i = false), n = 0
h : ∀ (i : ℕ), (bit b n).testBit i = false
this : b = false
⊢ bit b n = 0
have bit : bit false n = 0
Tactic: rw [this, bit_false, hn fun i => by rw [← h (i + 1), testBit_bit_succ]]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ Nat.bit b n = 0
have bit₁ : Eq (α := ℕ) ((fun (x : ℕ) ↦ 2 * x) n) 0
Tactic: rw [this, bit_false, hn fun i => by rw [← h (i + 1), testBit_bit_succ]]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ Nat.bit b n = 0
have bit₂ : Eq (α := ℕ) ((fun (x : ℕ) ↦ 2 * x) 0) 0
Tactic: rw [this, bit_false, hn fun i => by rw [← h (i + 1), testBit_bit_succ]]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n : ℕ
⊢ n.testBit 0 = n.bits.getI 0
have zero : (n.bits.headI.toNat != 0) = n.bits.headI
Tactic: simp only [testBit, shiftRight_zero, one_and_eq_mod_two, mod_two_of_bodd,
      bodd_eq_bits_head, List.getI_zero_eq_headI]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n : ℕ
⊢ (n.bits.headI.toNat != 0) = n.bits.headI
have zero : (false.toNat != 0) = false
Tactic: cases List.headI (bits n)
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n : ℕ
zero : (false.toNat != 0) = false
⊢ (n.bits.headI.toNat != 0) = n.bits.headI
have zero₁ : (true.toNat != 0) = true
Tactic: cases List.headI (bits n)
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
| n.testBit (i + 1)
have rw : (bit n.bodd n.div2).testBit (i + 1)
Tactic: rw [← bit_bodd_div2 n]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
⊢ n.testBit (i + 1) = n.bits.getI (i + 1)
have succ : (bit n.bodd n.div2).testBit (i + 1) = n.bits.getI (i + 1)
Tactic: conv_lhs => rw [← bit_bodd_div2 n]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
⊢ (bit n.bodd n.div2).testBit (i + 1) = n.bits.getI (i + 1)
have succ : n.bits.tail.getI i = n.bits.getI (i + 1)
Tactic: rw [testBit_bit_succ, ih n.div2, div2_bits_eq_tail]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
⊢ n.bits.tail.getI i = n.bits.getI (i + 1)
have succ : Eq (α := Bool) (List.getI (List.tail []) i) (List.getI [] (i + 1))
Tactic: cases n.bits
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
succ : Eq (α := Bool) (List.getI (List.tail []) i) (List.getI [] (i + 1))
⊢ n.bits.tail.getI i = n.bits.getI (i + 1)
have succ₁ : ∀ (head : Bool) (tail : List Bool), (head :: tail).tail.getI i = (head :: tail).getI (i + 1)
Tactic: cases n.bits
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n i : ℕ
⊢ n.testBit i = n.bits.getI i
have zero : ∀ (n : ℕ), n.testBit 0 = n.bits.getI 0
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
Cleared hypotheses: n, i
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n i : ℕ
zero : ∀ (n : ℕ), n.testBit 0 = n.bits.getI 0
⊢ n.testBit i = n.bits.getI i
have succ : ∀ (i : ℕ) (ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i) (n : ℕ), n.testBit (i + 1) = n.bits.getI (i + 1)
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
Cleared hypotheses: n, i
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n : ℕ
h : n ≠ 0
⊢ ∃ (i : ℕ), n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
have bit : ∀ (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: induction n using Nat.binaryRec with | zero => exact False.elim (h rfl) | bit b n hn => ?_
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
have pos : ∀ (h' : n = 0), ∃ (i : ℕ), (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false
Tactic: by_cases h' : n = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ ∃ (i : ℕ), (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false
have neg : ∀ (h' : ¬n = 0), ∃ (i : ℕ), (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false
Tactic: by_cases h' : n = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ ∃ (i : ℕ), (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false
have 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
Tactic: subst h'
Cleared hypotheses: n, hn, h, h'
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ b = true
have revert : ∀ (h : bit b 0 ≠ 0), b = true
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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), b = true
have false : ∀ (h : bit false 0 ≠ 0), false = true
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
b : Bool
hn : ∀ (h : Ne (α := ℕ) 0 0), ∃ (i : ℕ), testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = Bool.false
false : ∀ (h : bit Bool.false 0 ≠ 0), Bool.false = true
⊢ ∀ (h : bit b 0 ≠ 0), b = true
have true : ∀ (h : bit true 0 ≠ 0), true = true
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ ∃ (i : ℕ), (bit b 0).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b 0).testBit j = false
have pos : ∃ (i : ℕ), (bit true 0).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit true 0).testBit j = false
Tactic: rw [show b = true by
        revert h
        cases b <;> simp]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ (bit true 0).testBit 0 = true
have rw : true = true
Tactic: rw [testBit_bit_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ ∃ (i : ℕ), (bit true 0).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit true 0).testBit j = false
have pos : ∀ (j : ℕ) (hj : 0 < j), (bit true 0).testBit j = false
Tactic: refine ⟨0, ⟨by rw [testBit_bit_zero], fun j hj => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ (bit true 0).testBit j = false
have pos : ∀ (j' : ℕ) (hj : 0 < j'.succ), (bit true 0).testBit j'.succ = false
Tactic: obtain ⟨j', rfl⟩ := exists_eq_succ_of_ne_zero (ne_of_gt hj)
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ (bit true 0).testBit j'.succ = false
have pos : testBit 0 j' = false
Tactic: rw [testBit_bit_succ, zero_testBit]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ (bit true 0).testBit j'.succ = false
have pos₁ : false = false
Tactic: rw [testBit_bit_succ, zero_testBit]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ ∃ (i : ℕ), (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false
have 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
Tactic: obtain ⟨k, ⟨hk, hk'⟩⟩ := hn h'
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ (bit b n).testBit (k + 1) = true
have rw₁ : true = true
Tactic: rw [testBit_bit_succ, hk]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ ∃ (i : ℕ), (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false
have neg : ∀ (j : ℕ) (hj : k + 1 < j), (bit b n).testBit j = false
Tactic: refine ⟨k + 1, ⟨by rw [testBit_bit_succ, hk], fun j hj => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (hypothesis)
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
⊢ False
have hj₁ : k + 1 < 0
Tactic: subst x
Cleared hypotheses: j, hj, x
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ (bit b n).testBit j = false
have neg : ∀ (j' : ℕ) (hj : k + 1 < j'.succ), (bit b n).testBit j'.succ = false
Tactic: obtain ⟨j', rfl⟩ := exists_eq_succ_of_ne_zero (show j ≠ 0 by intro x; subst x; simp at hj)
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
m i : ℕ
hn : testBit 0 i = false
hm : m.testBit i = true
hnm : ∀ (j : ℕ), i < j → testBit 0 j = m.testBit j
⊢ 0 < m
have zero : m ≠ 0
Tactic: rw [Nat.pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ) (hn : n.testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j), n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ) (hn : (bit b n).testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j), bit b n < m
i : ℕ
hn : (bit b n).testBit i = false
hm : (bit b' m).testBit i = true
hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = (bit b' m).testBit j
⊢ bit b n < bit b' m
have pos : ∀ (hi : i = 0), bit b n < bit b' m
Tactic: by_cases hi : i = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ) (hn : n.testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j), n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ) (hn : (bit b n).testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j), bit b n < m
i : ℕ
hn : (bit b n).testBit i = false
hm : (bit b' m).testBit i = true
hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = (bit b' m).testBit j
pos : ∀ (hi : i = 0), bit b n < bit b' m
⊢ bit b n < bit b' m
have neg : ∀ (hi : ¬i = 0), bit b n < bit b' m
Tactic: by_cases hi : i = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (hypothesis)
Goal:
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ) (hn : n.testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j), n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ) (hn : (bit b n).testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j), bit b n < m
i : ℕ
hn : (bit b n).testBit i = false
hm : (bit b' m).testBit i = true
hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = (bit b' m).testBit j
hi : i = 0
⊢ bit b n < bit b' m
have hn₁ : (bit b n).testBit 0 = false
Tactic: subst hi
Cleared hypotheses: i, hn, hm, hnm, hi
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (hypothesis)
Goal:
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ) (hn : n.testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j), n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ) (hn : (bit b n).testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j), bit b n < m
i : ℕ
hn : (bit b n).testBit i = false
hm : (bit b' m).testBit i = true
hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = (bit b' m).testBit j
hi : i = 0
hn₁ : (bit b n).testBit 0 = false
⊢ bit b n < bit b' m
have hm₁ : (bit b' m).testBit 0 = true
Tactic: subst hi
Cleared hypotheses: i, hn, hm, hnm, hi
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (hypothesis)
Goal:
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ) (hn : n.testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j), n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ) (hn : (bit b n).testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j), bit b n < m
i : ℕ
hn : (bit b n).testBit i = false
hm : (bit b' m).testBit i = true
hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = (bit b' m).testBit j
hi : i = 0
hn₁ : (bit b n).testBit 0 = false
hm₁ : (bit b' m).testBit 0 = true
⊢ bit b n < bit b' m
have hnm₁ : ∀ (j : ℕ), 0 < j → (bit b n).testBit j = (bit b' m).testBit j
Tactic: subst hi
Cleared hypotheses: i, hn, hm, hnm, hi
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (hypothesis)
Goal:
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ) (hn : n.testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j), n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ) (hn : (bit b n).testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j), bit b n < m
hn : (bit b n).testBit 0 = false
hm : (bit b' m).testBit 0 = true
hnm : ∀ (j : ℕ), 0 < j → (bit b n).testBit j = (bit b' m).testBit j
⊢ bit b n < bit b' m
have hn₁ : b = false
Tactic: simp only [testBit_bit_zero] at hn hm
Cleared hypotheses: hn, hm
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (hypothesis)
Goal:
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ) (hn : n.testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j), n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ) (hn : (bit b n).testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j), bit b n < m
hn : (bit b n).testBit 0 = false
hm : (bit b' m).testBit 0 = true
hnm : ∀ (j : ℕ), 0 < j → (bit b n).testBit j = (bit b' m).testBit j
hn₁ : b = false
⊢ bit b n < bit b' m
have hm₁ : b' = true
Tactic: simp only [testBit_bit_zero] at hn hm
Cleared hypotheses: hn, hm
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ) (hn : n.testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j), n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ) (hn : (bit b n).testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j), bit b n < m
hnm : ∀ (j : ℕ), 0 < j → (bit b n).testBit j = (bit b' m).testBit j
hn : b = false
hm : b' = true
i : ℕ
⊢ n.testBit i = m.testBit i
have h : n.testBit i = (bit b n).testBit (i + 1)
Tactic: convert! hnm (i + 1) (Nat.zero_lt_succ _) using 1
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ) (hn : n.testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j), n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ) (hn : (bit b n).testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j), bit b n < m
hnm : ∀ (j : ℕ), 0 < j → (bit b n).testBit j = (bit b' m).testBit j
hn : b = false
hm : b' = true
i : ℕ
h : n.testBit i = (bit b n).testBit (i + 1)
⊢ n.testBit i = m.testBit i
have h₁ : m.testBit i = (bit b' m).testBit (i + 1)
Tactic: convert! hnm (i + 1) (Nat.zero_lt_succ _) using 1
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ) (hn : n.testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j), n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ) (hn : (bit b n).testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j), bit b n < m
hnm : ∀ (j : ℕ), 0 < j → (bit b n).testBit j = (bit b' m).testBit j
hn : b = false
hm : b' = true
i : ℕ
⊢ n.testBit i = (bit b n).testBit (i + 1)
have h : n.testBit i = n.testBit i
Tactic: rw [testBit_bit_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ) (hn : n.testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j), n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ) (hn : (bit b n).testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j), bit b n < m
hnm : ∀ (j : ℕ), 0 < j → (bit b n).testBit j = (bit b' m).testBit j
hn : b = false
hm : b' = true
i : ℕ
⊢ m.testBit i = (bit b' m).testBit (i + 1)
have h : m.testBit i = m.testBit i
Tactic: rw [testBit_bit_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (hypothesis)
Goal:
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ) (hn : n.testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j), n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ) (hn : (bit b n).testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j), bit b n < m
hnm : ∀ (j : ℕ), 0 < j → (bit b n).testBit j = (bit b' m).testBit j
hn : b = false
hm : b' = true
⊢ bit b n < bit b' m
have this : n = m
Tactic: have : n = m :=
          eq_of_testBit_eq fun i => by convert! hnm (i + 1) (Nat.zero_lt_succ _) using 1
          <;> rw [testBit_bit_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ) (hn : n.testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j), n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ) (hn : (bit b n).testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j), bit b n < m
hnm : ∀ (j : ℕ), 0 < j → (bit b n).testBit j = (bit b' m).testBit j
hn : b = false
hm : b' = true
this : n = m
⊢ bit b n < bit b' m
have pos : LT.lt (α := ℕ) ((fun (x : ℕ) ↦ 2 * x) m) ((fun (x : ℕ) ↦ 2 * x + 1) m)
Tactic: rw [hn, hm, this, bit_false, bit_true]