-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem mapM_eq_reverse_foldlM_cons [Monad m] [LawfulMonad m] (f : α → m β) (l : List α) :
    mapM f l = reverse <$> (l.foldlM (fun acc a => return ((← f a) :: acc)) [])

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l : List α
⊢ mapM' f l =
    reverse <$>
      List.foldlM
        (fun acc a => do
          let __do_lift ← f a
          pure (__do_lift :: acc))
        [] l

Tactic:
induction l with
| nil => simp
| cons a as ih =>
  simp only [mapM'_cons, ih, bind_map_left, foldlM_cons, LawfulMonad.bind_assoc, pure_bind,
    foldlM_cons_eq_append, _root_.map_bind, Functor.map_map, Function.comp_def, reverse_append,
    reverse_cons, reverse_nil, nil_append, singleton_append]
  simp [bind_pure_comp]

Result:
no goals

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
as : List α
ih :
  mapM' f as =
    reverse <$>
      List.foldlM
        (fun acc a => do
          let __do_lift ← f a
          pure (__do_lift :: acc))
        [] as
⊢ (do
      let __do_lift ← f a
      let a ←
        List.foldlM
            (fun acc a => do
              let __do_lift ← f a
              pure (__do_lift :: acc))
            [] as
      pure (__do_lift :: a.reverse)) =
    do
    let a ← f a
    (fun a_1 => a :: a_1.reverse) <$>
        List.foldlM
          (fun acc a => do
            let __do_lift ← f a
            pure (__do_lift :: acc))
          [] as

Tactic:
simp [bind_pure_comp]

Result:
no goals

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
as : List α
ih :
  mapM' f as =
    reverse <$>
      List.foldlM
        (fun acc a => do
          let __do_lift ← f a
          pure (__do_lift :: acc))
        [] as
⊢ mapM' f (a :: as) =
    reverse <$>
      List.foldlM
        (fun acc a => do
          let __do_lift ← f a
          pure (__do_lift :: acc))
        [] (a :: as)

Tactic:
simp only [mapM'_cons, ih, bind_map_left, foldlM_cons, LawfulMonad.bind_assoc, pure_bind,
  foldlM_cons_eq_append, _root_.map_bind, Functor.map_map, Function.comp_def, reverse_append,
  reverse_cons, reverse_nil, nil_append, singleton_append]

Result:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
as : List α
ih :
  mapM' f as =
    reverse <$>
      List.foldlM
        (fun acc a => do
          let __do_lift ← f a
          pure (__do_lift :: acc))
        [] as
⊢ (do
      let __do_lift ← f a
      let a ←
        List.foldlM
            (fun acc a => do
              let __do_lift ← f a
              pure (__do_lift :: acc))
            [] as
      pure (__do_lift :: a.reverse)) =
    do
    let a ← f a
    (fun a_1 => a :: a_1.reverse) <$>
        List.foldlM
          (fun acc a => do
            let __do_lift ← f a
            pure (__do_lift :: acc))
          [] as

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l : List α
⊢ mapM f l =
    reverse <$>
      List.foldlM
        (fun acc a => do
          let __do_lift ← f a
          pure (__do_lift :: acc))
        [] l

Tactic:
rw [← mapM'_eq_mapM]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l : List α
⊢ mapM' f l =
    reverse <$>
      List.foldlM
        (fun acc a => do
          let __do_lift ← f a
          pure (__do_lift :: acc))
        [] l

Proof state:
case nil
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
⊢ mapM' f [] =
    reverse <$>
      List.foldlM
        (fun acc a => do
          let __do_lift ← f a
          pure (__do_lift :: acc))
        [] []

Tactic:
simp

Result:
no goals