awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Bitwise
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
i : ℕ
hn : (bit b n).testBit i = false
hm : testBit 0 i = true
hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = testBit 0 j
⊢ bit b n < 0

Tactic:
False.elim (Bool.false_ne_true ((zero_testBit i).symm.trans hm))

Premises used: False.elim, Nat.zero_testBit, Bool.false_ne_true, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Nat.Bitwise
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
i : ℕ
hn : (bit b n).testBit i = false
hm : testBit 0 i = true
hnm : ∀ (j : ℕ), i < j → (bit b n).testBit j = testBit 0 j
⊢ bit b n < 0

Tactic:
exact False.elim (Bool.false_ne_true ((zero_testBit i).symm.trans hm))

Premises used: False.elim, Nat.zero_testBit, Bool.false_ne_true, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Nat.Bitwise
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
neg : ∀ (hi : ¬i = 0), bit b n < bit b' m
⊢ bit b n < bit b' m

Tactic:
by_cases hi : i = 0
-- Module: Mathlib.Data.Nat.Bitwise
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).testBit 0 = false

Tactic:
subst hi
-- Module: Mathlib.Data.Nat.Bitwise
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' m).testBit 0 = true

Tactic:
subst hi
-- Module: Mathlib.Data.Nat.Bitwise
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
⊢ ∀ (j : ℕ), 0 < j → (bit b n).testBit j = (bit b' m).testBit j

Tactic:
subst hi
-- Module: Mathlib.Data.Nat.Bitwise
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
⊢ b = false

Tactic:
simp only [testBit_bit_zero] at hn hm

Premises used: Nat.testBit_bit_zero
-- Module: Mathlib.Data.Nat.Bitwise
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
⊢ b' = true

Tactic:
simp only [testBit_bit_zero] at hn hm

Premises used: Nat.testBit_bit_zero
-- Module: Mathlib.Data.Nat.Bitwise
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 : ℕ
⊢ (bit b n).testBit (i + 1) = (bit b' m).testBit (i + 1)

Tactic:
hnm (i + 1) (Nat.zero_lt_succ _)

Premises used: Nat.zero_lt_succ, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Bitwise
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)
h₁ : m.testBit i = (bit b' m).testBit (i + 1)
⊢ n.testBit i = m.testBit i

Tactic:
convert! hnm (i + 1) (Nat.zero_lt_succ _) using 1

Premises used: Nat.zero_lt_succ, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Bitwise
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 h₁ : n.testBit i = n.testBit i
⊢ n.testBit i = (bit b n).testBit (i + 1)

Tactic:
rw [testBit_bit_succ]

Premises used: Nat.testBit_bit_succ
-- Module: Mathlib.Data.Nat.Bitwise
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 h₁ : m.testBit i = m.testBit i
⊢ m.testBit i = (bit b' m).testBit (i + 1)

Tactic:
rw [testBit_bit_succ]

Premises used: Nat.testBit_bit_succ
-- Module: Mathlib.Data.Nat.Bitwise
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
⊢ 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]
-- Module: Mathlib.Data.Nat.Bitwise
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
pos : LT.lt (α := ℕ) ((fun (x : ℕ) ↦ 2 * x) m) ((fun (x : ℕ) ↦ 2 * x + 1) m)
⊢ bit b n < bit b' m

Tactic:
rw [hn, hm, this, bit_false, bit_true]

Premises used: Nat.bit_true, Nat.bit_false
-- Module: Mathlib.Data.Nat.Bitwise
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
⊢ LT.lt (α := ℕ) ((fun (x : ℕ) ↦ 2 * x) m) ((fun (x : ℕ) ↦ 2 * x + 1) m)

Tactic:
Nat.lt_succ_self _

Premises used: Nat.lt_succ_self
-- Module: Mathlib.Data.Nat.Bitwise
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
⊢ LT.lt (α := ℕ) ((fun (x : ℕ) ↦ 2 * x) m) ((fun (x : ℕ) ↦ 2 * x + 1) m)

Tactic:
exact Nat.lt_succ_self _

Premises used: Nat.lt_succ_self
-- Module: Mathlib.Data.Nat.Bitwise
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
neg :
  ∀ (i' : ℕ) (hn : (bit b n).testBit i'.succ = false) (hm : (bit b' m).testBit i'.succ = true)
    (hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j) (hi : ¬i'.succ = 0), bit b n < bit b' m
⊢ bit b n < bit b' m

Tactic:
obtain ⟨i', rfl⟩ := exists_eq_succ_of_ne_zero hi

Premises used: Nat.exists_eq_succ_of_ne_zero, rfl
-- Module: Mathlib.Data.Nat.Bitwise
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'.succ = false
hm : (bit b' m).testBit i'.succ = true
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
⊢ n.testBit i' = false

Tactic:
simp only [testBit_bit_succ] at hn hm

Premises used: Nat.testBit_bit_succ
-- Module: Mathlib.Data.Nat.Bitwise
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'.succ = false
hm : (bit b' m).testBit i'.succ = true
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
hn₁ : n.testBit i' = false
⊢ m.testBit i' = true

Tactic:
simp only [testBit_bit_succ] at hn hm

Premises used: Nat.testBit_bit_succ
-- Module: Mathlib.Data.Nat.Bitwise
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' : ℕ
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
hn : n.testBit i' = false
hm : m.testBit i' = true
j : ℕ
hj : i' < j
⊢ (bit b n).testBit j.succ = (bit b' m).testBit j.succ

Tactic:
hnm j.succ (succ_lt_succ hj)

Premises used: Nat.succ_lt_succ, Nat.succ
-- Module: Mathlib.Data.Nat.Bitwise
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' : ℕ
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
hn : n.testBit i' = false
hm : m.testBit i' = true
j : ℕ
hj : i' < j
h : n.testBit j = (bit b n).testBit j.succ
h₁ : m.testBit j = (bit b' m).testBit j.succ
⊢ n.testBit j = m.testBit j

Tactic:
convert! hnm j.succ (succ_lt_succ hj) using 1

Premises used: Nat.succ_lt_succ, Nat.succ
-- Module: Mathlib.Data.Nat.Bitwise
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' : ℕ
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
hn : n.testBit i' = false
hm : m.testBit i' = true
j : ℕ
hj : i' < j
h h₁ : n.testBit j = n.testBit j
⊢ n.testBit j = (bit b n).testBit j.succ

Tactic:
rw [testBit_bit_succ]

Premises used: Nat.testBit_bit_succ
-- Module: Mathlib.Data.Nat.Bitwise
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' : ℕ
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
hn : n.testBit i' = false
hm : m.testBit i' = true
j : ℕ
hj : i' < j
h h₁ : m.testBit j = m.testBit j
⊢ m.testBit j = (bit b' m).testBit j.succ

Tactic:
rw [testBit_bit_succ]

Premises used: Nat.testBit_bit_succ
-- Module: Mathlib.Data.Nat.Bitwise
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' : ℕ
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
hn : n.testBit i' = false
hm : m.testBit i' = true
⊢ n < m

Tactic:
have := hn' _ hn hm fun j hj => by
          convert! hnm j.succ (succ_lt_succ hj) using 1 <;> rw [testBit_bit_succ]
-- Module: Mathlib.Data.Nat.Bitwise
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' : ℕ
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
hn : n.testBit i' = false
hm : m.testBit i' = true
this : n < m
⊢ bit b n < bit b' m

Tactic:
bit_lt_bit b b' this

Premises used: Nat.bit_lt_bit
-- Module: Mathlib.Data.Nat.Bitwise
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' : ℕ
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
hn : n.testBit i' = false
hm : m.testBit i' = true
this : n < m
⊢ bit b n < bit b' m

Tactic:
exact bit_lt_bit b b' this

Premises used: Nat.bit_lt_bit
-- Module: Mathlib.Data.Nat.Bitwise
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
m i : ℕ
hn : (Nat.bit b n).testBit i = false
hm : m.testBit i = true
hnm : ∀ (j : ℕ), i < j → (Nat.bit b n).testBit j = m.testBit j
bit :
  ∀ (i : ℕ) (hn : (Nat.bit b n).testBit i = false) (hm : testBit 0 i = true)
    (hnm : ∀ (j : ℕ), i < j → (Nat.bit b n).testBit j = testBit 0 j), Nat.bit b n < 0
bit₁ :
  ∀ (b' : Bool) (m : ℕ)
    (hm' :
      ∀ (i : ℕ) (hn : (Nat.bit b n).testBit i = false) (hm : m.testBit i = true)
        (hnm : ∀ (j : ℕ), i < j → (Nat.bit b n).testBit j = m.testBit j), Nat.bit b n < m)
    (i : ℕ) (hn : (Nat.bit b n).testBit i = false) (hm : (Nat.bit b' m).testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → (Nat.bit b n).testBit j = (Nat.bit b' m).testBit j), Nat.bit b n < Nat.bit b' m
⊢ Nat.bit b n < m

Tactic:
induction m using Nat.binaryRec generalizing i with
    | zero => exact False.elim (Bool.false_ne_true ((zero_testBit i).symm.trans hm))
    | bit b' m hm' =>
      by_cases hi : i = 0
      · subst hi
        simp only [testBit_bit_zero] at hn hm
        have : n = m :=
          eq_of_testBit_eq fun i => by convert! hnm (i + 1) (Nat.zero_lt_succ _) using 1
          <;> rw [testBit_bit_succ]
        rw [hn, hm, this, bit_false, bit_true]
        exact Nat.lt_succ_self _
      · obtain ⟨i', rfl⟩ := exists_eq_succ_of_ne_zero hi
        simp only [testBit_bit_succ] at hn hm
        have := hn' _ hn hm fun j hj => by
          convert! hnm j.succ (succ_lt_succ hj) using 1 <;> rw [testBit_bit_succ]
        exact bit_lt_bit b b' this

Premises used: Nat.bit, Nat.bit_true, Nat.lt_succ_self, Nat.bit_false, Nat.testBit_bit_zero, Nat.testBit_bit_succ, Nat.zero, rfl
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n m i : ℕ
hn : n.testBit i = false
hm : m.testBit i = true
hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j
zero :
  ∀ {m : ℕ} (i : ℕ) (hn : testBit 0 i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → testBit 0 j = m.testBit j), 0 < m
bit :
  ∀ (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)
    {m : ℕ} (i : ℕ) (hn : (Nat.bit b n).testBit i = false) (hm : m.testBit i = true)
    (hnm : ∀ (j : ℕ), i < j → (Nat.bit b n).testBit j = m.testBit j), Nat.bit b n < m
⊢ n < m

Tactic:
induction n using Nat.binaryRec generalizing i m with
  | zero =>
    rw [Nat.pos_iff_ne_zero]
    rintro rfl
    simp at hm
  | bit b n hn' =>
    induction m using Nat.binaryRec generalizing i with
    | zero => exact False.elim (Bool.false_ne_true ((zero_testBit i).symm.trans hm))
    | bit b' m hm' =>
      by_cases hi : i = 0
      · subst hi
        simp only [testBit_bit_zero] at hn hm
        have : n = m :=
          eq_of_testBit_eq fun i => by convert! hnm (i + 1) (Nat.zero_lt_succ _) using 1
          <;> rw [testBit_bit_succ]
        rw [hn, hm, this, bit_false, bit_true]
        exact Nat.lt_succ_self _
      · obtain ⟨i', rfl⟩ := exists_eq_succ_of_ne_zero hi
        simp only [testBit_bit_succ] at hn hm
        have := hn' _ hn hm fun j hj => by
          convert! hnm j.succ (succ_lt_succ hj) using 1 <;> rw [testBit_bit_succ]
        exact bit_lt_bit b b' this

Premises used: Nat.bit, Nat.bit_true, Nat.pos_iff_ne_zero, Nat.lt_succ_self, Nat.bit_false, Nat.testBit_bit_zero, Nat.testBit_bit_succ, Nat.zero, rfl
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : ∀ (m n : ℕ), bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) m n = swap (φ := fun (x y : ℕ) ↦ ℕ) (bitwise f) m n
⊢ bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) = swap (φ := fun (x y : ℕ) ↦ ℕ) (bitwise f)

Tactic:
funext m n
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
n : ℕ
⊢ bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) 0 n = bitwise f n 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
bm : Bool
m : ℕ
hm : m = 0 → bm = true
ihm : ∀ (n : ℕ), bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) m n = bitwise f n m
⊢ bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) (bit bm m) 0 = bitwise f 0 (bit bm m)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
bm : Bool
m : ℕ
hm : m = 0 → bm = true
ihm : ∀ (n : ℕ), bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) m n = bitwise f n m
bn : Bool
n : ℕ
hn : n = 0 → bn = true
h_1 : bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) (bit bm m) n = bitwise f n (bit bm m)
h :
  bit (swap (φ := fun (a a_1 : Bool) ↦ Bool) f bm bn) (bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) m n) =
    bitwise f (bit bn n) (bit bm m)
h₁ :
  bit (swap (φ := fun (a a_1 : Bool) ↦ Bool) f bm bn) (bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) m n) =
    bit (f bn bm) (bitwise f n m)
h₂ h₃ : bit (swap (φ := fun (a a_1 : Bool) ↦ Bool) f bm bn) (bitwise f n m) = bit (f bn bm) (bitwise f n m)
⊢ bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) (bit bm m) (bit bn n) = bitwise f (bit bn n) (bit bm m)

Tactic:
rw [bitwise_bit' _ _ _ _ hm hn, bitwise_bit' _ _ _ _ hn hm, ihm]

Premises used: Nat.bitwise_bit'
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
bm : Bool
m : ℕ
hm : m = 0 → bm = true
ihm : ∀ (n : ℕ), bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) m n = bitwise f n m
n : ℕ
h : bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) (bit bm m) 0 = bitwise f 0 (bit bm m)
h₁ :
  ∀ (bn : Bool) (n : ℕ) (hn : n = 0 → bn = true),
    bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) (bit bm m) n = bitwise f n (bit bm m) →
      bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) (bit bm m) (bit bn n) = bitwise f (bit bn n) (bit bm m)
⊢ bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) (bit bm m) n = bitwise f n (bit bm m)

Tactic:
induction n using Nat.binaryRec' with
    | zero => simp
    | bit bn n hn => rw [bitwise_bit' _ _ _ _ hm hn, bitwise_bit' _ _ _ _ hn hm, ihm]

Premises used: Nat.bit, Nat.zero
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
m n : ℕ
h : ∀ (n : ℕ), bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) 0 n = bitwise f n 0
h₁ :
  ∀ (bm : Bool) (m : ℕ) (hm : m = 0 → bm = true)
    (ihm : ∀ (n : ℕ), bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) m n = bitwise f n m) (n : ℕ),
    bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) (bit bm m) n = bitwise f n (bit bm m)
⊢ bitwise (swap (φ := fun (a a_1 : Bool) ↦ Bool) f) m n = bitwise f n m

Tactic:
induction m using Nat.binaryRec' generalizing n with
  | zero => simp
  | bit bm m hm ihm =>
    induction n using Nat.binaryRec' with
    | zero => simp
    | bit bn n hn => rw [bitwise_bit' _ _ _ _ hm hn, bitwise_bit' _ _ _ _ hn hm, ihm]

Premises used: Nat.bit, Nat.zero
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
hf : ∀ (b b' : Bool), f b b' = f b' b
n m : ℕ
this : bitwise f = swap (φ := fun (x y : ℕ) ↦ ℕ) (bitwise f)
rw : swap (φ := fun (x y : ℕ) ↦ ℕ) (bitwise f) n m
| bitwise f n m

Tactic:
rw [this]
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
hf : ∀ (b b' : Bool), f b b' = f b' b
n m : ℕ
this : bitwise f = swap (φ := fun (x y : ℕ) ↦ ℕ) (bitwise f)
conv_lhs : bitwise f n m = bitwise f m n
conv_lhs₁ : swap (φ := fun (x y : ℕ) ↦ ℕ) (bitwise f) n m = bitwise f m n
⊢ bitwise f n m = bitwise f m n

Tactic:
conv_lhs => rw [this]
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n m : ℕ
⊢ n ||| m = m ||| n

Tactic:
bitwise_comm Bool.or_comm n m

Premises used: Bool.or_comm, WellFounded.Nat.fix, Nat.bitwise._unary, WellFounded.Nat.fix.go, Nat.bitwise_comm, Nat.lor