α : Type u_1
a : α
m n : Nat
l : List α
h : m < length l
⊢ (if m = n then Option.map (fun x => a) (get? l n) else get? l n) = if m = n then some a else get? l n
α : Type u_1
a : α
m n : Nat
l : List α
h : m < length l
⊢ get? (set l m a) n = if m = n then some a else get? l n
simp [get?_set]
no goals
α : Type u_1
a : α
m n : Nat
l : List α
h : m < length l
⊢ (if m = n then Option.map (fun x => a) (get? l n) else get? l n) = if m = n then some a else get? l n
split <;> subst_vars <;> simp [*, get?_eq_get h]