-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem ge_two_pow_implies_high_bit_true {x : Nat} (p : x ≥ 2^n) : ∃ i, i ≥ n ∧ testBit x i

Proof state:
case right
x : Nat
hyp : x > 0 → ∀ {n : Nat}, x / 2 ≥ 2 ^ n → ∃ i, i ≥ n ∧ (x / 2).testBit i = true
n✝ : Nat
x_pos : x > 0
x_ne_zero : x ≠ 0
n : Nat
p : x ≥ 2 ^ n.succ
x_ge_n : x / 2 ≥ 2 ^ n
j : Nat
jp : j ≥ n ∧ (x / 2).testBit j = true
⊢ x.testBit (j + 1) = true

Tactic:
case right =>
  simpa using jp.right

Result:
no goals

Proof state:
x : Nat
hyp : x > 0 → ∀ {n : Nat}, x / 2 ≥ 2 ^ n → ∃ i, i ≥ n ∧ (x / 2).testBit i = true
n✝ : Nat
x_pos : x > 0
x_ne_zero : x ≠ 0
n : Nat
p : x ≥ 2 ^ n.succ
x_ge_n : x / 2 ≥ 2 ^ n
j : Nat
jp : j ≥ n ∧ (x / 2).testBit j = true
⊢ x.testBit (j + 1) = true

Tactic:
simpa using jp.right

Result:
no goals

Proof state:
x : Nat
hyp : x > 0 → ∀ {n : Nat}, x / 2 ≥ 2 ^ n → ∃ i, i ≥ n ∧ (x / 2).testBit i = true
n✝ : Nat
x_pos : x > 0
x_ne_zero : x ≠ 0
n : Nat
p : x ≥ 2 ^ n.succ
x_ge_n : x / 2 ≥ 2 ^ n
j : Nat
jp : j ≥ n ∧ (x / 2).testBit j = true
⊢ ∃ i, i ≥ n.succ ∧ x.testBit i = true

Tactic:
apply Exists.intro (j+1)

Result:
x : Nat
hyp : x > 0 → ∀ {n : Nat}, x / 2 ≥ 2 ^ n → ∃ i, i ≥ n ∧ (x / 2).testBit i = true
n✝ : Nat
x_pos : x > 0
x_ne_zero : x ≠ 0
n : Nat
p : x ≥ 2 ^ n.succ
x_ge_n : x / 2 ≥ 2 ^ n
j : Nat
jp : j ≥ n ∧ (x / 2).testBit j = true
⊢ j + 1 ≥ n.succ ∧ x.testBit (j + 1) = true

Proof state:
x : Nat
hyp : x > 0 → ∀ {n : Nat}, x / 2 ≥ 2 ^ n → ∃ i, i ≥ n ∧ (x / 2).testBit i = true
n : Nat
x_pos : x > 0
x_ne_zero : x ≠ 0
p : x ≥ 2 ^ zero
⊢ ∃ i, i ≥ zero ∧ x.testBit i = true

Tactic:
let ⟨j, jp⟩ := ne_zero_implies_bit_true x_ne_zero

Result:
x : Nat
hyp : x > 0 → ∀ {n : Nat}, x / 2 ≥ 2 ^ n → ∃ i, i ≥ n ∧ (x / 2).testBit i = true
n : Nat
x_pos : x > 0
x_ne_zero : x ≠ 0
p : x ≥ 2 ^ zero
j : Nat
jp : x.testBit j = true
⊢ ∃ i, i ≥ zero ∧ x.testBit i = true

Proof state:
case left
x : Nat
hyp : x > 0 → ∀ {n : Nat}, x / 2 ≥ 2 ^ n → ∃ i, i ≥ n ∧ (x / 2).testBit i = true
n✝ : Nat
x_pos : x > 0
x_ne_zero : x ≠ 0
n : Nat
p : x ≥ 2 ^ n.succ
x_ge_n : x / 2 ≥ 2 ^ n
j : Nat
jp : j ≥ n ∧ (x / 2).testBit j = true
⊢ j + 1 ≥ n.succ

case right
x : Nat
hyp : x > 0 → ∀ {n : Nat}, x / 2 ≥ 2 ^ n → ∃ i, i ≥ n ∧ (x / 2).testBit i = true
n✝ : Nat
x_pos : x > 0
x_ne_zero : x ≠ 0
n : Nat
p : x ≥ 2 ^ n.succ
x_ge_n : x / 2 ≥ 2 ^ n
j : Nat
jp : j ≥ n ∧ (x / 2).testBit j = true
⊢ x.testBit (j + 1) = true

Tactic:
case left =>
  exact (Nat.succ_le_succ jp.left)

Result:
case right
x : Nat
hyp : x > 0 → ∀ {n : Nat}, x / 2 ≥ 2 ^ n → ∃ i, i ≥ n ∧ (x / 2).testBit i = true
n✝ : Nat
x_pos : x > 0
x_ne_zero : x ≠ 0
n : Nat
p : x ≥ 2 ^ n.succ
x_ge_n : x / 2 ≥ 2 ^ n
j : Nat
jp : j ≥ n ∧ (x / 2).testBit j = true
⊢ x.testBit (j + 1) = true

Proof state:
x : Nat
hyp : x > 0 → ∀ {n : Nat}, x / 2 ≥ 2 ^ n → ∃ i, i ≥ n ∧ (x / 2).testBit i = true
n✝ : Nat
x_pos : x > 0
x_ne_zero : x ≠ 0
n : Nat
p : x ≥ 2 ^ n.succ
⊢ x / 2 ≥ 2 ^ n

Tactic:
simpa [le_div_iff_mul_le, ← Nat.pow_succ'] using p

Result:
no goals

Proof state:
x : Nat
hyp : x > 0 → ∀ {n : Nat}, x / 2 ≥ 2 ^ n → ∃ i, i ≥ n ∧ (x / 2).testBit i = true
n✝ : Nat
x_pos : x > 0
x_ne_zero : x ≠ 0
n : Nat
p : x ≥ 2 ^ n.succ
x_ge_n : x / 2 ≥ 2 ^ n
j : Nat
jp : j ≥ n ∧ (x / 2).testBit j = true
⊢ j + 1 ≥ n.succ ∧ x.testBit (j + 1) = true

Tactic:
apply And.intro

Result:
case left
x : Nat
hyp : x > 0 → ∀ {n : Nat}, x / 2 ≥ 2 ^ n → ∃ i, i ≥ n ∧ (x / 2).testBit i = true
n✝ : Nat
x_pos : x > 0
x_ne_zero : x ≠ 0
n : Nat
p : x ≥ 2 ^ n.succ
x_ge_n : x / 2 ≥ 2 ^ n
j : Nat
jp : j ≥ n ∧ (x / 2).testBit j = true
⊢ j + 1 ≥ n.succ

case right
x : Nat
hyp : x > 0 → ∀ {n : Nat}, x / 2 ≥ 2 ^ n → ∃ i, i ≥ n ∧ (x / 2).testBit i = true
n✝ : Nat
x_pos : x > 0
x_ne_zero : x ≠ 0
n : Nat
p : x ≥ 2 ^ n.succ
x_ge_n : x / 2 ≥ 2 ^ n
j : Nat
jp : j ≥ n ∧ (x / 2).testBit j = true
⊢ x.testBit (j + 1) = true

Proof state:
x : Nat
hyp : x > 0 → ∀ {n : Nat}, x / 2 ≥ 2 ^ n → ∃ i, i ≥ n ∧ (x / 2).testBit i = true
n : Nat
x_pos : x > 0
x_ne_zero : x ≠ 0
p : x ≥ 2 ^ zero
j : Nat
jp : x.testBit j = true
⊢ ∃ i, i ≥ zero ∧ x.testBit i = true

Tactic:
exact Exists.intro j (And.intro (Nat.zero_le _) jp)

Result:
no goals

Proof state:
case ind
x : Nat
hyp : x > 0 → ∀ {n : Nat}, x / 2 ≥ 2 ^ n → ∃ i, i ≥ n ∧ (x / 2).testBit i = true
n : Nat
p : x ≥ 2 ^ n
x_pos : x > 0
⊢ ∃ i, i ≥ n ∧ x.testBit i = true

Tactic:
have x_ne_zero : x ≠ 0 := Nat.ne_of_gt x_pos

Result:
case ind
x : Nat
hyp : x > 0 → ∀ {n : Nat}, x / 2 ≥ 2 ^ n → ∃ i, i ≥ n ∧ (x / 2).testBit i = true
n : Nat
p : x ≥ 2 ^ n
x_pos : x > 0
x_ne_zero : x ≠ 0
⊢ ∃ i, i ≥ n ∧ x.testBit i = true

Proof state:
x : Nat
hyp : x > 0 → ∀ {n : Nat}, x / 2 ≥ 2 ^ n → ∃ i, i ≥ n ∧ (x / 2).testBit i = true
n✝ : Nat
x_pos : x > 0
x_ne_zero : x ≠ 0
n : Nat
p : x ≥ 2 ^ n.succ
x_ge_n : x / 2 ≥ 2 ^ n
j : Nat
jp : j ≥ n ∧ (x / 2).testBit j = true
⊢ j + 1 ≥ n.succ

Tactic:
exact (Nat.succ_le_succ jp.left)

Result:
no goals

Proof state:
n x : Nat
p : x ≥ 2 ^ n
⊢ ∃ i, i ≥ n ∧ x.testBit i = true

Tactic:
induction x using div2Induction generalizing n with
| ind x hyp =>
  have x_pos : x > 0 := Nat.lt_of_lt_of_le (Nat.two_pow_pos n) p
  have x_ne_zero : x ≠ 0 := Nat.ne_of_gt x_pos
  match n with
  | zero =>
    let ⟨j, jp⟩ := ne_zero_implies_bit_true x_ne_zero
    exact Exists.intro j (And.intro (Nat.zero_le _) jp)
  | succ n =>
    have x_ge_n : x / 2 ≥ 2 ^ n := by
        simpa [le_div_iff_mul_le, ← Nat.pow_succ'] using p
    have ⟨j, jp⟩ := @hyp x_pos n x_ge_n
    apply Exists.intro (j+1)
    apply And.intro
    case left =>
      exact (Nat.succ_le_succ jp.left)
    case right =>
      simpa using jp.right

Result:
no goals

Proof state:
x : Nat
hyp : x > 0 → ∀ {n : Nat}, x / 2 ≥ 2 ^ n → ∃ i, i ≥ n ∧ (x / 2).testBit i = true
n✝ : Nat
x_pos : x > 0
x_ne_zero : x ≠ 0
n : Nat
p : x ≥ 2 ^ n.succ
⊢ ∃ i, i ≥ n.succ ∧ x.testBit i = true

Tactic:
have x_ge_n : x / 2 ≥ 2 ^ n := by
    simpa [le_div_iff_mul_le, ← Nat.pow_succ'] using p

Result:
x : Nat
hyp : x > 0 → ∀ {n : Nat}, x / 2 ≥ 2 ^ n → ∃ i, i ≥ n ∧ (x / 2).testBit i = true
n✝ : Nat
x_pos : x > 0
x_ne_zero : x ≠ 0
n : Nat
p : x ≥ 2 ^ n.succ
x_ge_n : x / 2 ≥ 2 ^ n
⊢ ∃ i, i ≥ n.succ ∧ x.testBit i = true

Proof state:
case ind
x : Nat
hyp : x > 0 → ∀ {n : Nat}, x / 2 ≥ 2 ^ n → ∃ i, i ≥ n ∧ (x / 2).testBit i = true
n : Nat
p : x ≥ 2 ^ n
x_pos : x > 0
x_ne_zero : x ≠ 0
⊢ ∃ i, i ≥ n ∧ x.testBit i = true

Tactic:
match n with
| zero =>
  let ⟨j, jp⟩ := ne_zero_implies_bit_true x_ne_zero
  exact Exists.intro j (And.intro (Nat.zero_le _) jp)
| succ n =>
  have x_ge_n : x / 2 ≥ 2 ^ n := by
      simpa [le_div_iff_mul_le, ← Nat.pow_succ'] using p
  have ⟨j, jp⟩ := @hyp x_pos n x_ge_n
  apply Exists.intro (j+1)
  apply And.intro
  case left =>
    exact (Nat.succ_le_succ jp.left)
  case right =>
    simpa using jp.right

Result:
no goals

Proof state:
case ind
x : Nat
hyp : x > 0 → ∀ {n : Nat}, x / 2 ≥ 2 ^ n → ∃ i, i ≥ n ∧ (x / 2).testBit i = true
n : Nat
p : x ≥ 2 ^ n
⊢ ∃ i, i ≥ n ∧ x.testBit i = true

Tactic:
have x_pos : x > 0 := Nat.lt_of_lt_of_le (Nat.two_pow_pos n) p

Result:
case ind
x : Nat
hyp : x > 0 → ∀ {n : Nat}, x / 2 ≥ 2 ^ n → ∃ i, i ≥ n ∧ (x / 2).testBit i = true
n : Nat
p : x ≥ 2 ^ n
x_pos : x > 0
⊢ ∃ i, i ≥ n ∧ x.testBit i = true

Proof state:
x : Nat
hyp : x > 0 → ∀ {n : Nat}, x / 2 ≥ 2 ^ n → ∃ i, i ≥ n ∧ (x / 2).testBit i = true
n✝ : Nat
x_pos : x > 0
x_ne_zero : x ≠ 0
n : Nat
p : x ≥ 2 ^ n.succ
x_ge_n : x / 2 ≥ 2 ^ n
⊢ ∃ i, i ≥ n.succ ∧ x.testBit i = true

Tactic:
have ⟨j, jp⟩ := @hyp x_pos n x_ge_n

Result:
x : Nat
hyp : x > 0 → ∀ {n : Nat}, x / 2 ≥ 2 ^ n → ∃ i, i ≥ n ∧ (x / 2).testBit i = true
n✝ : Nat
x_pos : x > 0
x_ne_zero : x ≠ 0
n : Nat
p : x ≥ 2 ^ n.succ
x_ge_n : x / 2 ≥ 2 ^ n
j : Nat
jp : j ≥ n ∧ (x / 2).testBit j = true
⊢ ∃ i, i ≥ n.succ ∧ x.testBit i = true