simp only [mapM', Option.pure_eq_some, Option.some.injEq] at h
case nil
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.157952 → Type ?u.157954
α : Type u_2
β : Type u_1
inst✝ : Monad m
b : β
f : α → Option β
bs : List β
h : mapM' f [] = some bs
hb : b ∈ bs
⊢ ∃ a, f a = some b
case nil
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.157952 → Type ?u.157954
α : Type u_2
β : Type u_1
inst✝ : Monad m
b : β
f : α → Option β
bs : List β
hb : b ∈ bs
h : [] = bs
⊢ ∃ a, f a = some b