ι : Type ?u.281379
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
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

case h
ι : Type ?u.281379
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
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
ι : Type ?u.281379
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
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
suffices h :
  ∀ mb : m β, (mb >>= fun b => List.foldlM f b l) = foldl (fun mb a => mb >>= fun b => f b a) mb l
no goals
case h
ι : Type ?u.281379
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
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
induction l with
| nil => intro; simp
| cons _ _ l_ih => intro; simp only [List.foldlM, foldl, ←l_ih, functor_norm]
no goals
ι : Type ?u.281379
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
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
simp [← h (pure b)]
case h.nil
ι : Type ?u.281379
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
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✝ []
case h.nil
ι : Type ?u.281379
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
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 []
intro
no goals
case h.nil
ι : Type ?u.281379
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
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✝ []
simp
case h.cons
ι : Type ?u.281379
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
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✝)
case h.cons
ι : Type ?u.281379
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
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✝)
intro
no goals
case h.cons
ι : Type ?u.281379
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
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✝)
simp only [List.foldlM, foldl, ←l_ih, functor_norm]