-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem testBit_limit {x i : Nat} (x_lt_succ : x < 2^(i+1)) :
    testBit x i = decide (x ≥ 2^i)

Proof state:
case false.inr.inl.a
x i : Nat
x_lt_succ : x < 2 ^ (i + 1)
xi : x.testBit i = false
x_ge : x ≥ 2 ^ i
j : Nat
j_ge : j ≥ i
jp : x.testBit j = true
x_lt : i < j
⊢ ?false.inr.inl.n < ?false.inr.inl.n

case false.inr.inl.n
x i : Nat
x_lt_succ : x < 2 ^ (i + 1)
xi : x.testBit i = false
x_ge : x ≥ 2 ^ i
j : Nat
j_ge : j ≥ i
jp : x.testBit j = true
x_lt : i < j
⊢ Nat

Tactic:
calc x < 2^(i+1) := x_lt_succ
     _ ≤ 2 ^ j := Nat.pow_le_pow_of_le_right Nat.zero_lt_two x_lt
     _ ≤ x := testBit_implies_ge jp

Result:
no goals

Proof state:
case false
x i : Nat
x_lt_succ : x < 2 ^ (i + 1)
xi : x.testBit i = false
⊢ x < 2 ^ i

Tactic:
cases Nat.lt_or_ge x (2^i) with
| inl x_lt =>
  exact x_lt
| inr x_ge =>
  have ⟨j, ⟨j_ge, jp⟩⟩  := ge_two_pow_implies_high_bit_true x_ge
  cases Nat.lt_or_eq_of_le j_ge with
  | inr x_eq =>
    simp [x_eq, jp] at xi
  | inl x_lt =>
    exfalso
    apply Nat.lt_irrefl
    calc x < 2^(i+1) := x_lt_succ
         _ ≤ 2 ^ j := Nat.pow_le_pow_of_le_right Nat.zero_lt_two x_lt
         _ ≤ x := testBit_implies_ge jp

Result:
no goals

Proof state:
case false.inr.inl
x i : Nat
x_lt_succ : x < 2 ^ (i + 1)
xi : x.testBit i = false
x_ge : x ≥ 2 ^ i
j : Nat
j_ge : j ≥ i
jp : x.testBit j = true
x_lt : i < j
⊢ x < 2 ^ i

Tactic:
exfalso

Result:
case false.inr.inl
x i : Nat
x_lt_succ : x < 2 ^ (i + 1)
xi : x.testBit i = false
x_ge : x ≥ 2 ^ i
j : Nat
j_ge : j ≥ i
jp : x.testBit j = true
x_lt : i < j
⊢ False

Proof state:
case false.inr.inl
x i : Nat
x_lt_succ : x < 2 ^ (i + 1)
xi : x.testBit i = false
x_ge : x ≥ 2 ^ i
j : Nat
j_ge : j ≥ i
jp : x.testBit j = true
x_lt : i < j
⊢ False

Tactic:
apply Nat.lt_irrefl

Result:
case false.inr.inl.a
x i : Nat
x_lt_succ : x < 2 ^ (i + 1)
xi : x.testBit i = false
x_ge : x ≥ 2 ^ i
j : Nat
j_ge : j ≥ i
jp : x.testBit j = true
x_lt : i < j
⊢ ?false.inr.inl.n < ?false.inr.inl.n

case false.inr.inl.n
x i : Nat
x_lt_succ : x < 2 ^ (i + 1)
xi : x.testBit i = false
x_ge : x ≥ 2 ^ i
j : Nat
j_ge : j ≥ i
jp : x.testBit j = true
x_lt : i < j
⊢ Nat

Proof state:
case false.inl
x i : Nat
x_lt_succ : x < 2 ^ (i + 1)
xi : x.testBit i = false
x_lt : x < 2 ^ i
⊢ x < 2 ^ i

Tactic:
exact x_lt

Result:
no goals

Proof state:
case false.inr.inr
x i : Nat
x_lt_succ : x < 2 ^ (i + 1)
xi : x.testBit i = false
x_ge : x ≥ 2 ^ i
j : Nat
j_ge : j ≥ i
jp : x.testBit j = true
x_eq : i = j
⊢ x < 2 ^ i

Tactic:
simp [x_eq, jp] at xi

Result:
no goals

Proof state:
case false
x i : Nat
x_lt_succ : x < 2 ^ (i + 1)
xi : x.testBit i = false
⊢ false = decide (x ≥ 2 ^ i)

Tactic:
simp

Result:
case false
x i : Nat
x_lt_succ : x < 2 ^ (i + 1)
xi : x.testBit i = false
⊢ x < 2 ^ i

Proof state:
case true
x i : Nat
x_lt_succ : x < 2 ^ (i + 1)
xi : x.testBit i = true
⊢ true = decide (x ≥ 2 ^ i)

Tactic:
simp [testBit_implies_ge xi]

Result:
no goals

Proof state:
case false.inr
x i : Nat
x_lt_succ : x < 2 ^ (i + 1)
xi : x.testBit i = false
x_ge : x ≥ 2 ^ i
⊢ x < 2 ^ i

Tactic:
have ⟨j, ⟨j_ge, jp⟩⟩  := ge_two_pow_implies_high_bit_true x_ge

Result:
case false.inr
x i : Nat
x_lt_succ : x < 2 ^ (i + 1)
xi : x.testBit i = false
x_ge : x ≥ 2 ^ i
j : Nat
j_ge : j ≥ i
jp : x.testBit j = true
⊢ x < 2 ^ i

Proof state:
case false.inr
x i : Nat
x_lt_succ : x < 2 ^ (i + 1)
xi : x.testBit i = false
x_ge : x ≥ 2 ^ i
j : Nat
j_ge : j ≥ i
jp : x.testBit j = true
⊢ x < 2 ^ i

Tactic:
cases Nat.lt_or_eq_of_le j_ge with
| inr x_eq =>
  simp [x_eq, jp] at xi
| inl x_lt =>
  exfalso
  apply Nat.lt_irrefl
  calc x < 2^(i+1) := x_lt_succ
       _ ≤ 2 ^ j := Nat.pow_le_pow_of_le_right Nat.zero_lt_two x_lt
       _ ≤ x := testBit_implies_ge jp

Result:
no goals

Proof state:
x i : Nat
x_lt_succ : x < 2 ^ (i + 1)
⊢ x.testBit i = decide (x ≥ 2 ^ i)

Tactic:
cases xi : testBit x i with
| true =>
  simp [testBit_implies_ge xi]
| false =>
  simp
  cases Nat.lt_or_ge x (2^i) with
  | inl x_lt =>
    exact x_lt
  | inr x_ge =>
    have ⟨j, ⟨j_ge, jp⟩⟩  := ge_two_pow_implies_high_bit_true x_ge
    cases Nat.lt_or_eq_of_le j_ge with
    | inr x_eq =>
      simp [x_eq, jp] at xi
    | inl x_lt =>
      exfalso
      apply Nat.lt_irrefl
      calc x < 2^(i+1) := x_lt_succ
           _ ≤ 2 ^ j := Nat.pow_le_pow_of_le_right Nat.zero_lt_two x_lt
           _ ≤ x := testBit_implies_ge jp

Result:
no goals