have ⟨_, h⟩ := h
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
h : ∃ b, f a = some b
⊢ (match f a with
    | some x => some b
    | none => none) =
    some b
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
h✝ : ∃ b, f a = some b
w✝ : β
h : f a = some w✝
⊢ (match f a with
    | some x => some b
    | none => none) =
    some b