α : Type u_1
l : List α
i : Nat
⊢ (if h : (fun as i => i < length as) l i then some l[i] else none) = get? l i
α : Type u_1
l : List α
i : Nat
⊢ l[i]? = get? l i
unfold getElem?
case inl
α : Type u_1
l : List α
i : Nat
h✝ : i < length l
⊢ some l[i] = get? l i

case inr
α : Type u_1
l : List α
i : Nat
h✝ : ¬(fun as i => i < length as) l i
⊢ none = get? l i
α : Type u_1
l : List α
i : Nat
⊢ (if h : (fun as i => i < length as) l i then some l[i] else none) = get? l i
split
no goals
case inl
α : Type u_1
l : List α
i : Nat
h✝ : i < length l
⊢ some l[i] = get? l i
exact (get?_eq_get ‹_›).symm
no goals
case inr
α : Type u_1
l : List α
i : Nat
h✝ : ¬(fun as i => i < length as) l i
⊢ none = get? l i
exact (get?_eq_none.2 <| Nat.not_lt.1 ‹_›).symm