-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem foldlM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : γ → β → m γ) (l : List α) (init : γ) :
    (l.filterMap f).foldlM g init =
      l.foldlM (fun x y => match f y with | some b => g x b | none => pure x) init

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : γ → β → m γ
a : α
l : List α
ih :
  ∀ (init : γ),
    List.foldlM g init (filterMap f l) =
      List.foldlM
        (fun x y =>
          match f y with
          | some b => g x b
          | none => pure x)
        init l
init : γ
⊢ List.foldlM g init (filterMap f (a :: l)) =
    List.foldlM
      (fun x y =>
        match f y with
        | some b => g x b
        | none => pure x)
      init (a :: l)

Tactic:
simp only [filterMap_cons, foldlM_cons]

Result:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : γ → β → m γ
a : α
l : List α
ih :
  ∀ (init : γ),
    List.foldlM g init (filterMap f l) =
      List.foldlM
        (fun x y =>
          match f y with
          | some b => g x b
          | none => pure x)
        init l
init : γ
⊢ List.foldlM g init
      (match f a with
      | none => filterMap f l
      | some b => b :: filterMap f l) =
    do
    let init ←
      match f a with
        | some b => g init b
        | none => pure init
    List.foldlM
        (fun x y =>
          match f y with
          | some b => g x b
          | none => pure x)
        init l

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : γ → β → m γ
a : α
l : List α
ih :
  ∀ (init : γ),
    List.foldlM g init (filterMap f l) =
      List.foldlM
        (fun x y =>
          match f y with
          | some b => g x b
          | none => pure x)
        init l
init : γ
⊢ List.foldlM g init
      (match f a with
      | none => filterMap f l
      | some b => b :: filterMap f l) =
    do
    let init ←
      match f a with
        | some b => g init b
        | none => pure init
    List.foldlM
        (fun x y =>
          match f y with
          | some b => g x b
          | none => pure x)
        init l

Tactic:
cases f a <;> simp [ih]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : γ → β → m γ
l : List α
init : γ
⊢ List.foldlM g init (filterMap f l) =
    List.foldlM
      (fun x y =>
        match f y with
        | some b => g x b
        | none => pure x)
      init l

Tactic:
induction l generalizing init with
| nil => rfl
| cons a l ih =>
  simp only [filterMap_cons, foldlM_cons]
  cases f a <;> simp [ih]

Result:
no goals

Proof state:
case nil
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : γ → β → m γ
init : γ
⊢ List.foldlM g init (filterMap f []) =
    List.foldlM
      (fun x y =>
        match f y with
        | some b => g x b
        | none => pure x)
      init []

Tactic:
rfl

Result:
no goals