Theorem: LeanColls.BitVec.get_empty (LeanColls/Data/BitVec.lean)

State before:
n : ℕ
i : Fin n
⊢ (empty n).get i = false
Tactic:
match i with
| ⟨i,h_i⟩ =>
simp [empty,get]
State after:
no goals

State before:
n : ℕ
i✝ : Fin n
i : ℕ
h_i : i < n
⊢ (empty n).get ⟨i, h_i⟩ = false
Tactic:
simp [empty,get]
State after:
n : ℕ
i✝ : Fin n
i : ℕ
h_i : i < n
⊢ (Seq.get (sorryAx ByteArray true) ⟨i / 8, ⋯⟩).land (UInt8.shiftLeft 1 (i % 8).toUInt8) = 0