-- 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 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' : ℕ
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
⊢ bit b n < bit b' m

Tactic:
have := hn' _ hn hm fun j hj => by
  convert hnm j.succ (succ_lt_succ hj) using 1 <;> rw [testBit_bit_succ]

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' : ℕ
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

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

Tactic:
simp only [testBit_bit_succ] at hn hm

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' : ℕ
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
⊢ bit b n < bit b' m

Proof state:
case neg.intro.true.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 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 false m).testBit j
⊢ 2 * n + 1 < 2 * m

Tactic:
calc
  2 * n + 1 < 2 * n + 2 := lt.base _
  _ ≤ 2 * m := mul_le_mul_left 2 this

Result:
no goals

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

Tactic:
by_cases hi : i = 0

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
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

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

Proof state:
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' : ℕ
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
this' : 2 * n < 2 * m
⊢ bit b n < bit b' m

Tactic:
cases b <;> cases b'
<;> simp only [bit_false, bit_true]

Result:
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

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

case neg.intro.true.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 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 false m).testBit j
⊢ 2 * n + 1 < 2 * m

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

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
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
⊢ n.testBit j = m.testBit j

Tactic:
convert hnm j.succ (succ_lt_succ hj) using 1 <;> rw [testBit_bit_succ]

Result:
no goals