apply List.mapM_loop_map
M : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad M
inst✝ : LawfulMonad M
l : List α
f : α → β
fM : α → M β
⊢ (∀ (a : α), fM a = pure (f a)) → mapM fM l = pure (map f l)
no goals