simp [map, Option.map, attach]
case h
α : Sort u_1
β : Type u_2
f : α ⇀ β
a : α
⊢ map Subtype.val (attach f) a = f a
case h
α : Sort u_1
β : Type u_2
f : α ⇀ β
a : α
⊢ (match
      match h : f a with
      | none => none
      | some b => some { val := b, property := ⋯ } with
    | some x => some ↑x
    | none => none) =
    f a