Theorem: Array.getElem?_nil (Runtime/Utilities/Extensions.lean)

State before:
α : Type u_1
i : Nat
⊢ #[][i]? = none
Tactic:
simp [getElem?]
State after:
α : Type u_1
i : Nat
⊢ (if h : i < size #[] then some #[][i] else none) = none

State before:
α : Type u_1
i : Nat
⊢ (if h : i < size #[] then some #[][i] else none) = none
Tactic:
split <;> simp
State after:
case inl
α : Type u_1
i : Nat
h✝ : i < size #[]
⊢ False

State before:
case inl
α : Type u_1
i : Nat
h✝ : i < size #[]
⊢ False
Tactic:
contradiction
State after:
no goals