-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem foldlM_cons_eq_append [Monad m] [LawfulMonad m] (f : α → m β) (as : List α) (b : β) (bs : List β) :
    (as.foldlM (init := b :: bs) fun acc a => return ((← f a) :: acc)) =
      (· ++ b :: bs) <$> as.foldlM (init := []) fun acc a => return ((← f a) :: acc)

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 α
b : β
bs : List β
ih :
  ∀ (b : β) (bs : List β),
    List.foldlM (fun acc a => (fun a => a :: acc) <$> f a) (b :: bs) as =
      (fun x => x ++ b :: bs) <$> List.foldlM (fun acc a => (fun a => a :: acc) <$> f a) [] as
⊢ List.foldlM
      (fun acc a => do
        let __do_lift ← f a
        pure (__do_lift :: acc))
      (b :: bs) (a :: as) =
    (fun x => x ++ b :: bs) <$>
      List.foldlM
        (fun acc a => do
          let __do_lift ← f a
          pure (__do_lift :: acc))
        [] (a :: as)

Tactic:
simp [ih, _root_.map_bind, Functor.map_map, Function.comp_def]

Result:
no goals

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

Tactic:
induction as generalizing b bs with
| nil => simp
| cons a as ih =>
  simp only [bind_pure_comp] at ih
  simp [ih, _root_.map_bind, Functor.map_map, Function.comp_def]

Result:
no goals

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 β
b : β
bs : List β
⊢ List.foldlM
      (fun acc a => do
        let __do_lift ← f a
        pure (__do_lift :: acc))
      (b :: bs) [] =
    (fun x => x ++ b :: bs) <$>
      List.foldlM
        (fun acc a => do
          let __do_lift ← f a
          pure (__do_lift :: acc))
        [] []

Tactic:
simp

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 :
  ∀ (b : β) (bs : List β),
    List.foldlM
        (fun acc a => do
          let __do_lift ← f a
          pure (__do_lift :: acc))
        (b :: bs) as =
      (fun x => x ++ b :: bs) <$>
        List.foldlM
          (fun acc a => do
            let __do_lift ← f a
            pure (__do_lift :: acc))
          [] as
b : β
bs : List β
⊢ List.foldlM
      (fun acc a => do
        let __do_lift ← f a
        pure (__do_lift :: acc))
      (b :: bs) (a :: as) =
    (fun x => x ++ b :: bs) <$>
      List.foldlM
        (fun acc a => do
          let __do_lift ← f a
          pure (__do_lift :: acc))
        [] (a :: as)

Tactic:
simp only [bind_pure_comp] at ih

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 α
b : β
bs : List β
ih :
  ∀ (b : β) (bs : List β),
    List.foldlM (fun acc a => (fun a => a :: acc) <$> f a) (b :: bs) as =
      (fun x => x ++ b :: bs) <$> List.foldlM (fun acc a => (fun a => a :: acc) <$> f a) [] as
⊢ List.foldlM
      (fun acc a => do
        let __do_lift ← f a
        pure (__do_lift :: acc))
      (b :: bs) (a :: as) =
    (fun x => x ++ b :: bs) <$>
      List.foldlM
        (fun acc a => do
          let __do_lift ← f a
          pure (__do_lift :: acc))
        [] (a :: as)