no goals
α : Type u_1
β : Type ?u.2053
l : List α
d : α
⊢ (fun o => Option.getD o d) '' range (get? l) = insert d {x | x ∈ l}
simp only [range_list_get?, image_insert_eq, Option.getD, image_image, image_id']