-- Mathlib/.lake/packages/batteries/Batteries/Data/Int.lean
theorem testBit_ofBits_ge {f : Fin n → Bool} (h : i ≥ n) :
    (ofBits f).testBit i = decide (ofBits f < 0)

Proof state:
n i : Nat
f : Fin n → Bool
h : i ≥ n
h✝ : 2 * Nat.ofBits f < 2 ^ n
⊢ 0 ≤ ofNat (Nat.ofBits f)

Tactic:
exact ofNat_nonneg ..

Result:
no goals

Proof state:
case isFalse
n i : Nat
f : Fin n → Bool
h : i ≥ n
h✝ : ¬2 * Nat.ofBits f < 2 ^ n
⊢ (subNatNat (Nat.ofBits f) (2 ^ n)).testBit i = decide (subNatNat (Nat.ofBits f) (2 ^ n) < 0)

Tactic:
have hlt := Nat.ofBits_lt_two_pow f

Result:
case isFalse
n i : Nat
f : Fin n → Bool
h : i ≥ n
h✝ : ¬2 * Nat.ofBits f < 2 ^ n
hlt : Nat.ofBits f < 2 ^ n
⊢ (subNatNat (Nat.ofBits f) (2 ^ n)).testBit i = decide (subNatNat (Nat.ofBits f) (2 ^ n) < 0)

Proof state:
n i : Nat
f : Fin n → Bool
h : i ≥ n
⊢ (if 2 * Nat.ofBits f < 2 ^ n then ofNat (Nat.ofBits f) else subNatNat (Nat.ofBits f) (2 ^ n)).testBit i =
    decide ((if 2 * Nat.ofBits f < 2 ^ n then ofNat (Nat.ofBits f) else subNatNat (Nat.ofBits f) (2 ^ n)) < 0)

Tactic:
split

Result:
case isTrue
n i : Nat
f : Fin n → Bool
h : i ≥ n
h✝ : 2 * Nat.ofBits f < 2 ^ n
⊢ (ofNat (Nat.ofBits f)).testBit i = decide (ofNat (Nat.ofBits f) < 0)

case isFalse
n i : Nat
f : Fin n → Bool
h : i ≥ n
h✝ : ¬2 * Nat.ofBits f < 2 ^ n
⊢ (subNatNat (Nat.ofBits f) (2 ^ n)).testBit i = decide (subNatNat (Nat.ofBits f) (2 ^ n) < 0)

Proof state:
case isFalse
n i : Nat
f : Fin n → Bool
h : i ≥ n
h✝ : ¬2 * Nat.ofBits f < 2 ^ n
hlt : Nat.ofBits f < 2 ^ n
⊢ (subNatNat (Nat.ofBits f) (2 ^ n)).testBit i = decide (subNatNat (Nat.ofBits f) (2 ^ n) < 0)

Tactic:
have h : 2 ^ n - Nat.ofBits f - 1 < 2 ^ i :=
  Nat.lt_of_lt_of_le (by omega) (Nat.pow_le_pow_right Nat.zero_lt_two h)

Result:
case isFalse
n i : Nat
f : Fin n → Bool
h✝¹ : i ≥ n
h✝ : ¬2 * Nat.ofBits f < 2 ^ n
hlt : Nat.ofBits f < 2 ^ n
h : 2 ^ n - Nat.ofBits f - 1 < 2 ^ i
⊢ (subNatNat (Nat.ofBits f) (2 ^ n)).testBit i = decide (subNatNat (Nat.ofBits f) (2 ^ n) < 0)

Proof state:
case isTrue
n i : Nat
f : Fin n → Bool
h : i ≥ n
h✝ : 2 * Nat.ofBits f < 2 ^ n
hge : ¬ofNat (Nat.ofBits f) < 0
⊢ (ofNat (Nat.ofBits f)).testBit i = decide (ofNat (Nat.ofBits f) < 0)

Tactic:
simp only [testBit, Nat.testBit_ofBits_ge _ _ h, hge, decide_false]

Result:
no goals

Proof state:
n i : Nat
f : Fin n → Bool
h : i ≥ n
h✝ : ¬2 * Nat.ofBits f < 2 ^ n
hlt : Nat.ofBits f < 2 ^ n
⊢ 2 ^ n - Nat.ofBits f - 1 < 2 ^ n

Tactic:
omega

Result:
no goals

Proof state:
n i : Nat
f : Fin n → Bool
h : i ≥ n
⊢ (ofBits f).testBit i = decide (ofBits f < 0)

Tactic:
simp only [ofBits]

Result:
n i : Nat
f : Fin n → Bool
h : i ≥ n
⊢ (if 2 * Nat.ofBits f < 2 ^ n then ofNat (Nat.ofBits f) else subNatNat (Nat.ofBits f) (2 ^ n)).testBit i =
    decide ((if 2 * Nat.ofBits f < 2 ^ n then ofNat (Nat.ofBits f) else subNatNat (Nat.ofBits f) (2 ^ n)) < 0)

Proof state:
case isFalse
n i : Nat
f : Fin n → Bool
h✝¹ : i ≥ n
h✝ : ¬2 * Nat.ofBits f < 2 ^ n
hlt : Nat.ofBits f < 2 ^ n
h : 2 ^ n - Nat.ofBits f - 1 < 2 ^ i
⊢ (subNatNat (Nat.ofBits f) (2 ^ n)).testBit i = decide (subNatNat (Nat.ofBits f) (2 ^ n) < 0)

Tactic:
simp [testBit, subNatNat_of_lt hlt, Nat.testBit_lt_two_pow h, negSucc_lt_zero]

Result:
no goals

Proof state:
n i : Nat
f : Fin n → Bool
h : i ≥ n
h✝ : 2 * Nat.ofBits f < 2 ^ n
⊢ ¬ofNat (Nat.ofBits f) < 0

Tactic:
rw [Int.not_lt]

Result:
n i : Nat
f : Fin n → Bool
h : i ≥ n
h✝ : 2 * Nat.ofBits f < 2 ^ n
⊢ 0 ≤ ofNat (Nat.ofBits f)

Proof state:
case isTrue
n i : Nat
f : Fin n → Bool
h : i ≥ n
h✝ : 2 * Nat.ofBits f < 2 ^ n
⊢ (ofNat (Nat.ofBits f)).testBit i = decide (ofNat (Nat.ofBits f) < 0)

Tactic:
have hge : ¬ ofNat (Nat.ofBits f) < 0 := by rw [Int.not_lt]; exact ofNat_nonneg ..

Result:
case isTrue
n i : Nat
f : Fin n → Bool
h : i ≥ n
h✝ : 2 * Nat.ofBits f < 2 ^ n
hge : ¬ofNat (Nat.ofBits f) < 0
⊢ (ofNat (Nat.ofBits f)).testBit i = decide (ofNat (Nat.ofBits f) < 0)