simp [const, map_val, ids]
case h
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
⊢ map (fun x => b) f a = const (ids f) b a
case h
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
⊢ Option.map (fun x => b) (f a) = if ∃ b, f a = some b then some b else none