no goals
α✝ : Type u_1
a : α✝
l : List α✝
n : Nat
e : get? l n = some a
hn : length l ≤ n
⊢ False
cases get?_len_le hn ▸ e
no goals
α✝ : Type u_1
a : α✝
l : List α✝
n : Nat
e : get? l n = some a
this : n < length l
⊢ get l { val := n, isLt := this } = a
rwa [get?_eq_get this, Option.some.injEq] at e