simp[allSome', mapM_map]
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.170951 → Type ?u.170953
α : Type u_1
β : Type u_2
inst✝ : Monad m
l : List α
f : α → β
⊢ (map (fun x => some (f x)) l).allSome' = some (map f l)
no goals