-- Mathlib/Data/List/Basic.lean
theorem foldlM_eq_foldl (f : β → α → m β) (b l) :
    List.foldlM f b l = foldl (fun mb a => mb >>= fun b => f b a) (pure b) l

Proof state:
α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
l : List α
⊢ List.foldlM f b l =
    foldl
      (fun mb a => do
        let b ← mb
        f b a)
      (pure b) l

Tactic:
suffices h :
  ∀ mb : m β, (mb >>= fun b => List.foldlM f b l) = foldl (fun mb a => mb >>= fun b => f b a) mb l
  by simp [← h (pure b)]

Result:
α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
l : List α
⊢ ∀ (mb : m β),
    (do
        let b ← mb
        List.foldlM f b l) =
      foldl
        (fun mb a => do
          let b ← mb
          f b a)
        mb l

Proof state:
case nil
α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
⊢ ∀ (mb : m β),
    (do
        let b ← mb
        List.foldlM f b []) =
      foldl
        (fun mb a => do
          let b ← mb
          f b a)
        mb []

Tactic:
intro

Result:
case nil
α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
mb✝ : m β
⊢ (do
      let b ← mb✝
      List.foldlM f b []) =
    foldl
      (fun mb a => do
        let b ← mb
        f b a)
      mb✝ []

Proof state:
case cons
α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
head✝ : α
tail✝ : List α
l_ih :
  ∀ (mb : m β),
    (do
        let b ← mb
        List.foldlM f b tail✝) =
      foldl
        (fun mb a => do
          let b ← mb
          f b a)
        mb tail✝
mb✝ : m β
⊢ (do
      let b ← mb✝
      List.foldlM f b (head✝ :: tail✝)) =
    foldl
      (fun mb a => do
        let b ← mb
        f b a)
      mb✝ (head✝ :: tail✝)

Tactic:
simp only [List.foldlM, foldl, ← l_ih, functor_norm]

Result:
no goals

Proof state:
α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
l : List α
h :
  ∀ (mb : m β),
    (do
        let b ← mb
        List.foldlM f b l) =
      foldl
        (fun mb a => do
          let b ← mb
          f b a)
        mb l
⊢ List.foldlM f b l =
    foldl
      (fun mb a => do
        let b ← mb
        f b a)
      (pure b) l

Tactic:
simp [← h (pure b)]

Result:
no goals

Proof state:
case nil
α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
mb✝ : m β
⊢ (do
      let b ← mb✝
      List.foldlM f b []) =
    foldl
      (fun mb a => do
        let b ← mb
        f b a)
      mb✝ []

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
head✝ : α
tail✝ : List α
l_ih :
  ∀ (mb : m β),
    (do
        let b ← mb
        List.foldlM f b tail✝) =
      foldl
        (fun mb a => do
          let b ← mb
          f b a)
        mb tail✝
⊢ ∀ (mb : m β),
    (do
        let b ← mb
        List.foldlM f b (head✝ :: tail✝)) =
      foldl
        (fun mb a => do
          let b ← mb
          f b a)
        mb (head✝ :: tail✝)

Tactic:
intro

Result:
case cons
α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
head✝ : α
tail✝ : List α
l_ih :
  ∀ (mb : m β),
    (do
        let b ← mb
        List.foldlM f b tail✝) =
      foldl
        (fun mb a => do
          let b ← mb
          f b a)
        mb tail✝
mb✝ : m β
⊢ (do
      let b ← mb✝
      List.foldlM f b (head✝ :: tail✝)) =
    foldl
      (fun mb a => do
        let b ← mb
        f b a)
      mb✝ (head✝ :: tail✝)

Proof state:
α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
l : List α
⊢ ∀ (mb : m β),
    (do
        let b ← mb
        List.foldlM f b l) =
      foldl
        (fun mb a => do
          let b ← mb
          f b a)
        mb l

Tactic:
induction l with
| nil => intro; simp
| cons _ _ l_ih => intro; simp only [List.foldlM, foldl, ← l_ih, functor_norm]

Result:
no goals