exact ih hbs' hb
case cons.intro.intro.intro.intro.inr
α✝ : 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 β
a : α
as : List α
ih : ∀ {bs : List β}, mapM' f as = some bs → b ∈ bs → ∃ a, f a = some b
b' : β
hb' : f a = some b'
bs' : List β
hbs' : mapM' f as = some bs'
hb✝ : b ∈ b' :: bs'
hb : b ∈ bs'
⊢ ∃ a, f a = some b
no goals