-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem ne_zero_implies_bit_true {x : Nat} (xnz : x ≠ 0) : ∃ i, testBit x i

Proof state:
x : Nat
hyp : x > 0 → x / 2 ≠ 0 → ∃ i, (x / 2).testBit i = true
xnz : x ≠ 0
x_pos : x > 0
mod2_eq : x % 2 = 0
⊢ ∃ i, x.testBit i = true

Tactic:
rw [←div_add_mod x 2] at xnz

Result:
x : Nat
hyp : x > 0 → x / 2 ≠ 0 → ∃ i, (x / 2).testBit i = true
xnz : 2 * (x / 2) + x % 2 ≠ 0
x_pos : x > 0
mod2_eq : x % 2 = 0
⊢ ∃ i, x.testBit i = true

Proof state:
x : Nat
xnz : x ≠ 0
⊢ ∃ i, x.testBit i = true

Tactic:
induction x using div2Induction with
| ind x hyp =>
  have x_pos : x > 0 := Nat.pos_of_ne_zero xnz
  match mod_two_eq_zero_or_one x with
  | Or.inl mod2_eq =>
    rw [←div_add_mod x 2] at xnz
    simp only [mod2_eq, ne_eq, Nat.mul_eq_zero, Nat.add_zero, false_or, reduceCtorEq] at xnz
    have ⟨d, dif⟩   := hyp x_pos xnz
    apply Exists.intro (d+1)
    simp_all
  | Or.inr mod2_eq =>
    apply Exists.intro 0
    simp_all

Result:
no goals

Proof state:
x : Nat
hyp : x > 0 → x / 2 ≠ 0 → ∃ i, (x / 2).testBit i = true
x_pos : x > 0
mod2_eq : x % 2 = 0
xnz : ¬x / 2 = 0
⊢ ∃ i, x.testBit i = true

Tactic:
have ⟨d, dif⟩   := hyp x_pos xnz

Result:
x : Nat
hyp : x > 0 → x / 2 ≠ 0 → ∃ i, (x / 2).testBit i = true
x_pos : x > 0
mod2_eq : x % 2 = 0
xnz : ¬x / 2 = 0
d : Nat
dif : (x / 2).testBit d = true
⊢ ∃ i, x.testBit i = true

Proof state:
x : Nat
hyp : x > 0 → x / 2 ≠ 0 → ∃ i, (x / 2).testBit i = true
x_pos : x > 0
mod2_eq : x % 2 = 0
xnz : ¬x / 2 = 0
d : Nat
dif : (x / 2).testBit d = true
⊢ x.testBit (d + 1) = true

Tactic:
simp_all

Result:
no goals

Proof state:
case ind
x : Nat
hyp : x > 0 → x / 2 ≠ 0 → ∃ i, (x / 2).testBit i = true
xnz : x ≠ 0
⊢ ∃ i, x.testBit i = true

Tactic:
have x_pos : x > 0 := Nat.pos_of_ne_zero xnz

Result:
case ind
x : Nat
hyp : x > 0 → x / 2 ≠ 0 → ∃ i, (x / 2).testBit i = true
xnz : x ≠ 0
x_pos : x > 0
⊢ ∃ i, x.testBit i = true

Proof state:
x : Nat
hyp : x > 0 → x / 2 ≠ 0 → ∃ i, (x / 2).testBit i = true
x_pos : x > 0
mod2_eq : x % 2 = 0
xnz : ¬x / 2 = 0
d : Nat
dif : (x / 2).testBit d = true
⊢ ∃ i, x.testBit i = true

Tactic:
apply Exists.intro (d+1)

Result:
x : Nat
hyp : x > 0 → x / 2 ≠ 0 → ∃ i, (x / 2).testBit i = true
x_pos : x > 0
mod2_eq : x % 2 = 0
xnz : ¬x / 2 = 0
d : Nat
dif : (x / 2).testBit d = true
⊢ x.testBit (d + 1) = true

Proof state:
x : Nat
hyp : x > 0 → x / 2 ≠ 0 → ∃ i, (x / 2).testBit i = true
xnz : 2 * (x / 2) + x % 2 ≠ 0
x_pos : x > 0
mod2_eq : x % 2 = 0
⊢ ∃ i, x.testBit i = true

Tactic:
simp only [mod2_eq, ne_eq, Nat.mul_eq_zero, Nat.add_zero, false_or, reduceCtorEq] at xnz

Result:
x : Nat
hyp : x > 0 → x / 2 ≠ 0 → ∃ i, (x / 2).testBit i = true
x_pos : x > 0
mod2_eq : x % 2 = 0
xnz : ¬x / 2 = 0
⊢ ∃ i, x.testBit i = true

Proof state:
x : Nat
hyp : x > 0 → x / 2 ≠ 0 → ∃ i, (x / 2).testBit i = true
xnz : x ≠ 0
x_pos : x > 0
mod2_eq : x % 2 = 1
⊢ x.testBit 0 = true

Tactic:
simp_all

Result:
no goals

Proof state:
x : Nat
hyp : x > 0 → x / 2 ≠ 0 → ∃ i, (x / 2).testBit i = true
xnz : x ≠ 0
x_pos : x > 0
mod2_eq : x % 2 = 1
⊢ ∃ i, x.testBit i = true

Tactic:
apply Exists.intro 0

Result:
x : Nat
hyp : x > 0 → x / 2 ≠ 0 → ∃ i, (x / 2).testBit i = true
xnz : x ≠ 0
x_pos : x > 0
mod2_eq : x % 2 = 1
⊢ x.testBit 0 = true

Proof state:
case ind
x : Nat
hyp : x > 0 → x / 2 ≠ 0 → ∃ i, (x / 2).testBit i = true
xnz : x ≠ 0
x_pos : x > 0
⊢ ∃ i, x.testBit i = true

Tactic:
match mod_two_eq_zero_or_one x with
| Or.inl mod2_eq =>
  rw [←div_add_mod x 2] at xnz
  simp only [mod2_eq, ne_eq, Nat.mul_eq_zero, Nat.add_zero, false_or, reduceCtorEq] at xnz
  have ⟨d, dif⟩   := hyp x_pos xnz
  apply Exists.intro (d+1)
  simp_all
| Or.inr mod2_eq =>
  apply Exists.intro 0
  simp_all

Result:
no goals