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

case f
n✝ m✝ i✝ : ℕ
hn✝ : testBit n✝ i✝ = false
hm✝ : testBit m✝ i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m i : ℕ
hn : testBit (bit b n) i = false
hm : testBit m i = true
hnm : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j
⊢ bit b n < m
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
induction' n using Nat.binaryRec with b n hn' generalizing i m
case f.z
n✝ m✝ i✝¹ : ℕ
hn✝¹ : testBit n✝ i✝¹ = false
hm✝¹ : testBit m✝ i✝¹ = true
hnm✝¹ : ∀ (j : ℕ), i✝¹ < j → testBit n✝ j = testBit m✝ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m i✝ : ℕ
hn✝ : testBit (bit b n) i✝ = false
hm✝ : testBit m i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit (bit b n) j = testBit m j
i : ℕ
hn : testBit (bit b n) i = false
hm : testBit 0 i = true
hnm : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit 0 j
⊢ bit b n < 0

case f.f
n✝ m✝¹ i✝¹ : ℕ
hn✝¹ : testBit n✝ i✝¹ = false
hm✝¹ : testBit m✝¹ i✝¹ = true
hnm✝¹ : ∀ (j : ℕ), i✝¹ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i✝ : ℕ
hn✝ : testBit (bit b n) i✝ = false
hm✝ : testBit m✝ i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
i : ℕ
hn : testBit (bit b n) i = false
hm : testBit (bit b' m) i = true
hnm : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit (bit b' m) j
⊢ bit b n < bit b' m
case f
n✝ m✝ i✝ : ℕ
hn✝ : testBit n✝ i✝ = false
hm✝ : testBit m✝ i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m i : ℕ
hn : testBit (bit b n) i = false
hm : testBit m i = true
hnm : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j
⊢ bit b n < m
induction' m using Nat.binaryRec with b' m hm' generalizing i
case pos
n✝ m✝¹ i✝¹ : ℕ
hn✝¹ : testBit n✝ i✝¹ = false
hm✝¹ : testBit m✝¹ i✝¹ = true
hnm✝¹ : ∀ (j : ℕ), i✝¹ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i✝ : ℕ
hn✝ : testBit (bit b n) i✝ = false
hm✝ : testBit m✝ i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
i : ℕ
hn : testBit (bit b n) i = false
hm : testBit (bit b' m) i = true
hnm : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit (bit b' m) j
hi : i = 0
⊢ bit b n < bit b' m

case neg
n✝ m✝¹ i✝¹ : ℕ
hn✝¹ : testBit n✝ i✝¹ = false
hm✝¹ : testBit m✝¹ i✝¹ = true
hnm✝¹ : ∀ (j : ℕ), i✝¹ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i✝ : ℕ
hn✝ : testBit (bit b n) i✝ = false
hm✝ : testBit m✝ i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
i : ℕ
hn : testBit (bit b n) i = false
hm : testBit (bit b' m) i = true
hnm : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit (bit b' m) j
hi : ¬i = 0
⊢ bit b n < bit b' m
case f.f
n✝ m✝¹ i✝¹ : ℕ
hn✝¹ : testBit n✝ i✝¹ = false
hm✝¹ : testBit m✝¹ i✝¹ = true
hnm✝¹ : ∀ (j : ℕ), i✝¹ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i✝ : ℕ
hn✝ : testBit (bit b n) i✝ = false
hm✝ : testBit m✝ i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
i : ℕ
hn : testBit (bit b n) i = false
hm : testBit (bit b' m) i = true
hnm : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit (bit b' m) j
⊢ bit b n < bit b' m
by_cases hi : i = 0
case z
n m✝ i✝ : ℕ
hn✝ : testBit n i✝ = false
hm✝ : testBit m✝ i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit n j = testBit m✝ j
m i : ℕ
hn : testBit 0 i = false
hnm : ∀ (j : ℕ), i < j → testBit 0 j = testBit m j
hm : m ≤ 0
⊢ testBit m i ≠ true
case z
n m✝ i✝ : ℕ
hn✝ : testBit n i✝ = false
hm✝ : testBit m✝ i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit n j = testBit m✝ j
m i : ℕ
hn : testBit 0 i = false
hm : testBit m i = true
hnm : ∀ (j : ℕ), i < j → testBit 0 j = testBit m j
⊢ 0 < m
contrapose! hm
case z
n m✝ i✝ : ℕ
hn✝ : testBit n i✝ = false
hm✝ : testBit m✝ i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit n j = testBit m✝ j
m i : ℕ
hn : testBit 0 i = false
hnm : ∀ (j : ℕ), i < j → testBit 0 j = testBit m j
hm : m = 0
⊢ testBit m i ≠ true
case z
n m✝ i✝ : ℕ
hn✝ : testBit n i✝ = false
hm✝ : testBit m✝ i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit n j = testBit m✝ j
m i : ℕ
hn : testBit 0 i = false
hnm : ∀ (j : ℕ), i < j → testBit 0 j = testBit m j
hm : m ≤ 0
⊢ testBit m i ≠ true
rw [le_zero_iff] at hm
no goals
case z
n m✝ i✝ : ℕ
hn✝ : testBit n i✝ = false
hm✝ : testBit m✝ i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit n j = testBit m✝ j
m i : ℕ
hn : testBit 0 i = false
hnm : ∀ (j : ℕ), i < j → testBit 0 j = testBit m j
hm : m = 0
⊢ testBit m i ≠ true
simp [hm]
no goals
case f.z
n✝ m✝ i✝¹ : ℕ
hn✝¹ : testBit n✝ i✝¹ = false
hm✝¹ : testBit m✝ i✝¹ = true
hnm✝¹ : ∀ (j : ℕ), i✝¹ < j → testBit n✝ j = testBit m✝ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m i✝ : ℕ
hn✝ : testBit (bit b n) i✝ = false
hm✝ : testBit m i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit (bit b n) j = testBit m j
i : ℕ
hn : testBit (bit b n) i = false
hm : testBit 0 i = true
hnm : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit 0 j
⊢ bit b n < 0
exact False.elim (Bool.ff_ne_tt ((zero_testBit i).symm.trans hm))
case pos
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hn✝ : testBit (bit b n) i = false
hm✝ : testBit m✝ i = true
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
hn : testBit (bit b n) 0 = false
hm : testBit (bit b' m) 0 = true
hnm : ∀ (j : ℕ), 0 < j → testBit (bit b n) j = testBit (bit b' m) j
⊢ bit b n < bit b' m
case pos
n✝ m✝¹ i✝¹ : ℕ
hn✝¹ : testBit n✝ i✝¹ = false
hm✝¹ : testBit m✝¹ i✝¹ = true
hnm✝¹ : ∀ (j : ℕ), i✝¹ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i✝ : ℕ
hn✝ : testBit (bit b n) i✝ = false
hm✝ : testBit m✝ i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
i : ℕ
hn : testBit (bit b n) i = false
hm : testBit (bit b' m) i = true
hnm : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit (bit b' m) j
hi : i = 0
⊢ bit b n < bit b' m
subst hi
case pos
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hn✝ : testBit (bit b n) i = false
hm✝ : testBit m✝ i = true
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
hnm : ∀ (j : ℕ), 0 < j → testBit (bit b n) j = testBit (bit b' m) j
hn : b = false
hm : b' = true
⊢ bit b n < bit b' m
case pos
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hn✝ : testBit (bit b n) i = false
hm✝ : testBit m✝ i = true
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
hn : testBit (bit b n) 0 = false
hm : testBit (bit b' m) 0 = true
hnm : ∀ (j : ℕ), 0 < j → testBit (bit b n) j = testBit (bit b' m) j
⊢ bit b n < bit b' m
simp only [testBit_zero] at hn hm
case pos
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hn✝ : testBit (bit b n) i = false
hm✝ : testBit m✝ i = true
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
hnm : ∀ (j : ℕ), 0 < j → testBit (bit b n) j = testBit (bit b' m) j
hn : b = false
hm : b' = true
this : n = m
⊢ bit b n < bit b' m
case pos
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hn✝ : testBit (bit b n) i = false
hm✝ : testBit m✝ i = true
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
hnm : ∀ (j : ℕ), 0 < j → testBit (bit b n) j = testBit (bit b' m) j
hn : b = false
hm : b' = true
⊢ bit b n < bit b' m
have : n = m :=
  eq_of_testBit_eq fun i => by convert hnm (i + 1) (Nat.zero_lt_succ _) using 1
  <;> rw [testBit_succ]
case pos
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hn✝ : testBit (bit b n) i = false
hm✝ : testBit m✝ i = true
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
hnm : ∀ (j : ℕ), 0 < j → testBit (bit b n) j = testBit (bit b' m) j
hn : b = false
hm : b' = true
this : n = m
⊢ 2 * m < 2 * m + 1
case pos
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hn✝ : testBit (bit b n) i = false
hm✝ : testBit m✝ i = true
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
hnm : ∀ (j : ℕ), 0 < j → testBit (bit b n) j = testBit (bit b' m) j
hn : b = false
hm : b' = true
this : n = m
⊢ bit b n < bit b' m
rw [hn, hm, this, bit_false, bit_true, bit0_val, bit1_val]
no goals
case pos
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hn✝ : testBit (bit b n) i = false
hm✝ : testBit m✝ i = true
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
hnm : ∀ (j : ℕ), 0 < j → testBit (bit b n) j = testBit (bit b' m) j
hn : b = false
hm : b' = true
this : n = m
⊢ 2 * m < 2 * m + 1
exact lt_add_one _
no goals
n✝ m✝¹ i✝¹ : ℕ
hn✝¹ : testBit n✝ i✝¹ = false
hm✝¹ : testBit m✝¹ i✝¹ = true
hnm✝¹ : ∀ (j : ℕ), i✝¹ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i✝ : ℕ
hn✝ : testBit (bit b n) i✝ = false
hm✝ : testBit m✝ i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
hnm : ∀ (j : ℕ), 0 < j → testBit (bit b n) j = testBit (bit b' m) j
hn : b = false
hm : b' = true
i : ℕ
⊢ testBit n i = testBit m i
convert hnm (i + 1) (Nat.zero_lt_succ _) using 1
<;> rw [testBit_succ]
case neg.intro
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hn✝ : testBit (bit b n) i = false
hm✝ : testBit m✝ i = true
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
i' : ℕ
hn : testBit (bit b n) (succ i') = false
hm : testBit (bit b' m) (succ i') = true
hnm : ∀ (j : ℕ), succ i' < j → testBit (bit b n) j = testBit (bit b' m) j
hi : ¬succ i' = 0
⊢ bit b n < bit b' m
case neg
n✝ m✝¹ i✝¹ : ℕ
hn✝¹ : testBit n✝ i✝¹ = false
hm✝¹ : testBit m✝¹ i✝¹ = true
hnm✝¹ : ∀ (j : ℕ), i✝¹ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i✝ : ℕ
hn✝ : testBit (bit b n) i✝ = false
hm✝ : testBit m✝ i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
i : ℕ
hn : testBit (bit b n) i = false
hm : testBit (bit b' m) i = true
hnm : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit (bit b' m) j
hi : ¬i = 0
⊢ bit b n < bit b' m
obtain ⟨i', rfl⟩ := exists_eq_succ_of_ne_zero hi
case neg.intro
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hn✝ : testBit (bit b n) i = false
hm✝ : testBit m✝ i = true
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
i' : ℕ
hnm : ∀ (j : ℕ), succ i' < j → testBit (bit b n) j = testBit (bit b' m) j
hi : ¬succ i' = 0
hn : testBit n i' = false
hm : testBit m i' = true
⊢ bit b n < bit b' m
case neg.intro
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hn✝ : testBit (bit b n) i = false
hm✝ : testBit m✝ i = true
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
i' : ℕ
hn : testBit (bit b n) (succ i') = false
hm : testBit (bit b' m) (succ i') = true
hnm : ∀ (j : ℕ), succ i' < j → testBit (bit b n) j = testBit (bit b' m) j
hi : ¬succ i' = 0
⊢ bit b n < bit b' m
simp only [testBit_succ] at hn hm
case neg.intro
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hn✝ : testBit (bit b n) i = false
hm✝ : testBit m✝ i = true
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
i' : ℕ
hnm : ∀ (j : ℕ), succ i' < j → testBit (bit b n) j = testBit (bit b' m) j
hi : ¬succ i' = 0
hn : testBit n i' = false
hm : testBit m i' = true
this : n < m
⊢ bit b n < bit b' m
case neg.intro
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hn✝ : testBit (bit b n) i = false
hm✝ : testBit m✝ i = true
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
i' : ℕ
hnm : ∀ (j : ℕ), succ i' < j → testBit (bit b n) j = testBit (bit b' m) j
hi : ¬succ i' = 0
hn : testBit n i' = false
hm : testBit m i' = true
⊢ bit b n < bit b' m
have :=
  hn' _ hn hm fun j hj => by convert hnm j.succ (succ_lt_succ hj) using 1 <;> rw [testBit_succ]
no goals
case neg.intro
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hn✝ : testBit (bit b n) i = false
hm✝ : testBit m✝ i = true
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
i' : ℕ
hnm : ∀ (j : ℕ), succ i' < j → testBit (bit b n) j = testBit (bit b' m) j
hi : ¬succ i' = 0
hn : testBit n i' = false
hm : testBit m i' = true
this : n < m
⊢ bit b n < bit b' m
cases b <;> cases b'
<;> simp only [bit_false, bit_true, bit0_val n, bit1_val n, bit0_val m, bit1_val m]
<;> linarith only [this]
no goals
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hn✝ : testBit (bit b n) i = false
hm✝ : testBit m✝ i = true
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
i' : ℕ
hnm : ∀ (j : ℕ), succ i' < j → testBit (bit b n) j = testBit (bit b' m) j
hi : ¬succ i' = 0
hn : testBit n i' = false
hm : testBit m i' = true
j : ℕ
hj : i' < j
⊢ testBit n j = testBit m j
convert hnm j.succ (succ_lt_succ hj) using 1 <;> rw [testBit_succ]