∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → m β) (x : List α),
  List.mapM' f x =
    match x with
    | [] => pure []
    | a :: l => do
      let __do_lift ← f a
      let __do_lift_1 ← List.mapM' f l
      pure (__do_lift :: __do_lift_1)