case z
n : ℕ
h✝ : n ≠ 0
h : 0 ≠ 0
⊢ ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false

case f
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
⊢ ∃ i, testBit (bit b n) i = true ∧ ∀ (j : ℕ), i < j → testBit (bit b n) j = false
n : ℕ
h : n ≠ 0
⊢ ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
induction' n using Nat.binaryRec with b n hn
case pos
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
h' : n = 0
⊢ ∃ i, testBit (bit b n) i = true ∧ ∀ (j : ℕ), i < j → testBit (bit b n) j = false

case neg
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
h' : ¬n = 0
⊢ ∃ i, testBit (bit b n) i = true ∧ ∀ (j : ℕ), i < j → testBit (bit b n) j = false
case f
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
⊢ ∃ i, testBit (bit b n) i = true ∧ ∀ (j : ℕ), i < j → testBit (bit b n) j = false
by_cases h' : n = 0
no goals
case z
n : ℕ
h✝ : n ≠ 0
h : 0 ≠ 0
⊢ ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
exact False.elim (h rfl)
case pos
n : ℕ
h✝ : n ≠ 0
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
⊢ ∃ i, testBit (bit b 0) i = true ∧ ∀ (j : ℕ), i < j → testBit (bit b 0) j = false
case pos
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
h' : n = 0
⊢ ∃ i, testBit (bit b n) i = true ∧ ∀ (j : ℕ), i < j → testBit (bit b n) j = false
subst h'
case pos
n : ℕ
h✝ : n ≠ 0
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
⊢ ∃ i, testBit (bit true 0) i = true ∧ ∀ (j : ℕ), i < j → testBit (bit true 0) j = false
case pos
n : ℕ
h✝ : n ≠ 0
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
⊢ ∃ i, testBit (bit b 0) i = true ∧ ∀ (j : ℕ), i < j → testBit (bit b 0) j = false
rw [show b = true by
    revert h
    cases b <;> simp]
case pos
n : ℕ
h✝ : n ≠ 0
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
j : ℕ
hj : 0 < j
⊢ testBit (bit true 0) j = false
case pos
n : ℕ
h✝ : n ≠ 0
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
⊢ ∃ i, testBit (bit true 0) i = true ∧ ∀ (j : ℕ), i < j → testBit (bit true 0) j = false
refine' ⟨0, ⟨by rw [testBit_zero], fun j hj => _⟩⟩
case pos.intro
n : ℕ
h✝ : n ≠ 0
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
j' : ℕ
hj : 0 < succ j'
⊢ testBit (bit true 0) (succ j') = false
case pos
n : ℕ
h✝ : n ≠ 0
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
j : ℕ
hj : 0 < j
⊢ testBit (bit true 0) j = false
obtain ⟨j', rfl⟩ := exists_eq_succ_of_ne_zero (ne_of_gt hj)
no goals
case pos.intro
n : ℕ
h✝ : n ≠ 0
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
j' : ℕ
hj : 0 < succ j'
⊢ testBit (bit true 0) (succ j') = false
rw [testBit_succ, zero_testBit]
n : ℕ
h : n ≠ 0
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
⊢ bit b 0 ≠ 0 → b = true
n : ℕ
h✝ : n ≠ 0
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
⊢ b = true
revert h
no goals
n : ℕ
h : n ≠ 0
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
⊢ bit b 0 ≠ 0 → b = true
cases b <;> simp
no goals
n : ℕ
h✝ : n ≠ 0
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
⊢ testBit (bit true 0) 0 = true
rw [testBit_zero]
case neg.intro.intro
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : testBit n k = true
hk' : ∀ (j : ℕ), k < j → testBit n j = false
⊢ ∃ i, testBit (bit b n) i = true ∧ ∀ (j : ℕ), i < j → testBit (bit b n) j = false
case neg
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
h' : ¬n = 0
⊢ ∃ i, testBit (bit b n) i = true ∧ ∀ (j : ℕ), i < j → testBit (bit b n) j = false
obtain ⟨k, ⟨hk, hk'⟩⟩ := hn h'
case neg.intro.intro
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : testBit n k = true
hk' : ∀ (j : ℕ), k < j → testBit n j = false
j : ℕ
hj : k + 1 < j
⊢ testBit (bit b n) j = false
case neg.intro.intro
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : testBit n k = true
hk' : ∀ (j : ℕ), k < j → testBit n j = false
⊢ ∃ i, testBit (bit b n) i = true ∧ ∀ (j : ℕ), i < j → testBit (bit b n) j = false
refine' ⟨k + 1, ⟨by rw [testBit_succ, hk], fun j hj => _⟩⟩
case neg.intro.intro.intro
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : testBit n k = true
hk' : ∀ (j : ℕ), k < j → testBit n j = false
j' : ℕ
hj : k + 1 < succ j'
⊢ testBit (bit b n) (succ j') = false
case neg.intro.intro
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : testBit n k = true
hk' : ∀ (j : ℕ), k < j → testBit n j = false
j : ℕ
hj : k + 1 < j
⊢ testBit (bit b n) j = false
obtain ⟨j', rfl⟩ := exists_eq_succ_of_ne_zero (show j ≠ 0 by intro x; subst x; simp at hj)
no goals
case neg.intro.intro.intro
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : testBit n k = true
hk' : ∀ (j : ℕ), k < j → testBit n j = false
j' : ℕ
hj : k + 1 < succ j'
⊢ testBit (bit b n) (succ j') = false
exact (testBit_succ _ _ _).trans (hk' _ (lt_of_succ_lt_succ hj))
no goals
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : testBit n k = true
hk' : ∀ (j : ℕ), k < j → testBit n j = false
⊢ testBit (bit b n) (k + 1) = true
rw [testBit_succ, hk]
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : testBit n k = true
hk' : ∀ (j : ℕ), k < j → testBit n j = false
j : ℕ
hj : k + 1 < j
x : j = 0
⊢ False
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : testBit n k = true
hk' : ∀ (j : ℕ), k < j → testBit n j = false
j : ℕ
hj : k + 1 < j
⊢ j ≠ 0
intro x
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : testBit n k = true
hk' : ∀ (j : ℕ), k < j → testBit n j = false
hj : k + 1 < 0
⊢ False
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : testBit n k = true
hk' : ∀ (j : ℕ), k < j → testBit n j = false
j : ℕ
hj : k + 1 < j
x : j = 0
⊢ False
subst x
no goals
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : testBit n k = true
hk' : ∀ (j : ℕ), k < j → testBit n j = false
hj : k + 1 < 0
⊢ False
simp at hj