-- Mathlib/Data/Nat/Bitwise.lean
theorem exists_most_significant_bit {n : ℕ} (h : n ≠ 0) :
    ∃ i, testBit n i = true ∧ ∀ j, i < j → testBit n j = false

Proof state:
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
j : ℕ
hj : k + 1 < j
x : j = 0
⊢ False

Tactic:
subst x

Result:
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
hj : k + 1 < 0
⊢ False

Proof state:
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
⊢ (bit b n).testBit (k + 1) = true

Tactic:
rw [testBit_bit_succ, hk]

Result:
no goals

Proof state:
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
⊢ bit b 0 ≠ 0 → b = true

Tactic:
cases b <;> simp

Result:
no goals

Proof state:
case neg.intro.intro
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
⊢ ∃ i, (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false

Tactic:
refine ⟨k + 1, ⟨by rw [testBit_bit_succ, hk], fun j hj => ?_⟩⟩

Result:
case neg.intro.intro
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
j : ℕ
hj : k + 1 < j
⊢ (bit b n).testBit j = false

Proof state:
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
j : ℕ
hj : k + 1 < j
⊢ j ≠ 0

Tactic:
intro x

Result:
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
j : ℕ
hj : k + 1 < j
x : j = 0
⊢ False

Proof state:
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
hj : k + 1 < 0
⊢ False

Tactic:
simp at hj

Result:
no goals

Proof state:
n : ℕ
h : n ≠ 0
⊢ ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false

Tactic:
induction' n using Nat.binaryRec with b n hn

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

case f
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
⊢ ∃ i, (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false

Proof state:
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
⊢ (bit true 0).testBit 0 = true

Tactic:
rw [testBit_bit_zero]

Result:
no goals

Proof state:
case pos
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
⊢ (bit true 0).testBit j = false

Tactic:
obtain ⟨j', rfl⟩ := exists_eq_succ_of_ne_zero (ne_of_gt hj)

Result:
case pos.intro
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'.succ
⊢ (bit true 0).testBit j'.succ = false

Proof state:
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
⊢ b = true

Tactic:
revert h

Result:
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
⊢ bit b 0 ≠ 0 → b = true

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

Tactic:
exact False.elim (h rfl)

Result:
no goals

Proof state:
case f
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
⊢ ∃ i, (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false

Tactic:
by_cases h' : n = 0

Result:
case pos
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : n = 0
⊢ ∃ i, (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false

case neg
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
⊢ ∃ i, (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false

Proof state:
case pos.intro
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'.succ
⊢ (bit true 0).testBit j'.succ = false

Tactic:
rw [testBit_bit_succ, zero_testBit]

Result:
no goals

Proof state:
case pos
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
⊢ ∃ i, (bit true 0).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit true 0).testBit j = false

Tactic:
refine ⟨0, ⟨by rw [testBit_bit_zero], fun j hj => ?_⟩⟩

Result:
case pos
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
⊢ (bit true 0).testBit j = false

Proof state:
case neg.intro.intro.intro
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
j' : ℕ
hj : k + 1 < j'.succ
⊢ (bit b n).testBit j'.succ = false

Tactic:
exact (testBit_bit_succ _ _ _).trans (hk' _ (lt_of_succ_lt_succ hj))

Result:
no goals

Proof state:
case neg
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
⊢ ∃ i, (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false

Tactic:
obtain ⟨k, ⟨hk, hk'⟩⟩ := hn h'

Result:
case neg.intro.intro
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
⊢ ∃ i, (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false

Proof state:
case pos
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
⊢ ∃ i, (bit b 0).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b 0).testBit j = false

Tactic:
rw [show b = true by
    revert h
    cases b <;> simp]

Result:
case pos
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
⊢ ∃ i, (bit true 0).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit true 0).testBit j = false

Proof state:
case neg.intro.intro
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
j : ℕ
hj : k + 1 < j
⊢ (bit b n).testBit j = false

Tactic:
obtain ⟨j', rfl⟩ := exists_eq_succ_of_ne_zero (show j ≠ 0 by intro x; subst x; simp at hj)

Result:
case neg.intro.intro.intro
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : n.testBit k = true
hk' : ∀ (j : ℕ), k < j → n.testBit j = false
j' : ℕ
hj : k + 1 < j'.succ
⊢ (bit b n).testBit j'.succ = false