α : Type u_1
a : α
n : Nat
l : List α
h : n < length l
⊢ (fun x => a) <$> some (get l { val := n, isLt := h }) = some a
α : Type u_1
a : α
n : Nat
l : List α
h : n < length l
⊢ get? (set l n a) n = some a
rw [get?_set_eq, get?_eq_get h]
no goals
α : Type u_1
a : α
n : Nat
l : List α
h : n < length l
⊢ (fun x => a) <$> some (get l { val := n, isLt := h }) = some a
rfl