α : Type u_1
l₁ : List α
a : α
l₂ : List α
n : Nat
l : List α
eq : l = l₁ ++ a :: l₂
h : length l₁ = n
⊢ get? (a :: l₂) 0 = some a
α : Type u_1
l₁ : List α
a : α
l₂ : List α
n : Nat
l : List α
eq : l = l₁ ++ a :: l₂
h : length l₁ = n
⊢ some (get l { val := n, isLt := (_ : n < length l) }) = some a
rw [← get?_eq_get, eq, get?_append_right (h ▸ Nat.le_refl _), h, Nat.sub_self]
no goals
α : Type u_1
l₁ : List α
a : α
l₂ : List α
n : Nat
l : List α
eq : l = l₁ ++ a :: l₂
h : length l₁ = n
⊢ get? (a :: l₂) 0 = some a
rfl