simp[List.mapM, List.mapM.loop]
m : Type u_1 → Type u_2
a : Type u_3
b : Type u_1
M : Monad m
LM : LawfulMonad m
x : a
xs : List a
f : a → m b
⊢ mapM f (x :: xs) = do
    let b_1 ← f x
    let bs ← mapM f xs
    pure (b_1 :: bs)
m : Type u_1 → Type u_2
a : Type u_3
b : Type u_1
M : Monad m
LM : LawfulMonad m
x : a
xs : List a
f : a → m b
⊢ (do
      let __do_lift ← f x
      List.mapM.loop f xs [__do_lift]) =
    do
    let b_1 ← f x
    let bs ← List.mapM.loop f xs []
    pure (b_1 :: bs)