Theorem: List.mapM_map (MLIR/Util/KDTensor.lean)

State before:
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)
Tactic:
apply List.mapM_loop_map
State after:
no goals