-- Mathlib/Data/Nat/Bitwise.lean
theorem lt_of_testBit {n m : ℕ} (i : ℕ) (hn : testBit n i = false) (hm : testBit m i = true)
    (hnm : ∀ j, i < j → testBit n j = testBit m j) : n < m

Proof state:
case f.z
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (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))

Result:
no goals

Proof state:
case neg
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (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

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

Result:
case neg.intro
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (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
⊢ bit b n < bit b' m

Proof state:
case pos
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (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

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

Result:
case pos
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (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
⊢ (fun x => 2 * x) m < (fun x => 2 * x + 1) m

Proof state:
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (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

Tactic:
convert hnm (i + 1) (Nat.zero_lt_succ _) using 1
<;> rw [testBit_bit_succ]

Result:
no goals

Proof state:
case neg.intro.false.true
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
m i' : ℕ
hi : ¬i'.succ = 0
hn : n.testBit i' = false
hm : m.testBit i' = true
this : n < m
this' : 2 * n < 2 * m
hm' :
  ∀ (i : ℕ),
    (bit false n).testBit i = false →
      m.testBit i = true → (∀ (j : ℕ), i < j → (bit false n).testBit j = m.testBit j) → bit false n < m
hnm : ∀ (j : ℕ), i'.succ < j → (bit false n).testBit j = (bit true m).testBit j
⊢ 2 * n < 2 * m + 1

Tactic:
exact Nat.lt_add_right 1 this'

Result:
no goals

Proof state:
case z
m i : ℕ
hn : testBit 0 i = false
hm : m.testBit i = true
hnm : ∀ (j : ℕ), i < j → testBit 0 j = m.testBit j
⊢ m ≠ 0

Tactic:
rintro rfl

Result:
case z
i : ℕ
hn : testBit 0 i = false
hm : testBit 0 i = true
hnm : ∀ (j : ℕ), i < j → testBit 0 j = testBit 0 j
⊢ False

Proof state:
case neg.intro.false.false
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
m i' : ℕ
hi : ¬i'.succ = 0
hn : n.testBit i' = false
hm : m.testBit i' = true
this : n < m
this' : 2 * n < 2 * m
hm' :
  ∀ (i : ℕ),
    (bit false n).testBit i = false →
      m.testBit i = true → (∀ (j : ℕ), i < j → (bit false n).testBit j = m.testBit j) → bit false n < m
hnm : ∀ (j : ℕ), i'.succ < j → (bit false n).testBit j = (bit false m).testBit j
⊢ 2 * n < 2 * m

Tactic:
exact this'

Result:
no goals

Proof state:
case pos
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (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
⊢ (fun x => 2 * x) m < (fun x => 2 * x + 1) m

Tactic:
exact Nat.lt_succ_self _

Result:
no goals

Proof state:
case f
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
m 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

Tactic:
induction' m using Nat.binaryRec with b' m hm' generalizing i

Result:
case f.z
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (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

case f.f
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (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

Proof state:
case neg.intro.true.true
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
m i' : ℕ
hi : ¬i'.succ = 0
hn : n.testBit i' = false
hm : m.testBit i' = true
this : n < m
this' : 2 * n < 2 * m
hm' :
  ∀ (i : ℕ),
    (bit true n).testBit i = false →
      m.testBit i = true → (∀ (j : ℕ), i < j → (bit true n).testBit j = m.testBit j) → bit true n < m
hnm : ∀ (j : ℕ), i'.succ < j → (bit true n).testBit j = (bit true m).testBit j
⊢ 2 * n + 1 < 2 * m + 1

Tactic:
exact Nat.succ_lt_succ this'

Result:
no goals

Proof state:
case z
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

Result:
no goals