-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem filterMapM_cons [Monad m] [LawfulMonad m] (f : α → m (Option β)) :
    (a :: l).filterMapM f = do
      match (← f a) with
      | none => filterMapM f l
      | some b => return (b :: (← filterMapM f l))

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
⊢ (do
      let __do_lift ← f a
      match __do_lift with
        | none => filterMapM.loop f l []
        | some b => filterMapM.loop f l [b]) =
    do
    let __do_lift ← f a
    match __do_lift with
      | none => filterMapM f l
      | some b => do
        let __do_lift ← filterMapM f l
        pure (b :: __do_lift)

Tactic:
congr

Result:
case e_a
m : Type u_1 → Type u_2
α β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
⊢ (fun __do_lift =>
      match __do_lift with
      | none => filterMapM.loop f l []
      | some b => filterMapM.loop f l [b]) =
    fun __do_lift =>
    match __do_lift with
    | none => filterMapM f l
    | some b => do
      let __do_lift ← filterMapM f l
      pure (b :: __do_lift)

Proof state:
case e_a.h.h_1
m : Type u_1 → Type u_2
α β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
b : Option β
⊢ filterMapM.loop f l [] =
    match none with
    | none => filterMapM f l
    | some b => do
      let __do_lift ← filterMapM f l
      pure (b :: __do_lift)

Tactic:
simp [filterMapM]

Result:
no goals

Proof state:
case e_a.h.h_2
m : Type u_1 → Type u_2
α β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
__do_lift✝ : Option β
b : β
⊢ filterMapM.loop f l [b] = cons b <$> filterMapM f l

Tactic:
rw [filterMapM_loop_eq, filterMapM]

Result:
case e_a.h.h_2
m : Type u_1 → Type u_2
α β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
__do_lift✝ : Option β
b : β
⊢ (fun x => [b].reverse ++ x) <$> filterMapM.loop f l [] = cons b <$> filterMapM.loop f l []

Proof state:
case e_a.h.h_2
m : Type u_1 → Type u_2
α β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
__do_lift✝ : Option β
b : β
⊢ (fun x => [b].reverse ++ x) <$> filterMapM.loop f l [] = cons b <$> filterMapM.loop f l []

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
⊢ filterMapM f (a :: l) = do
    let __do_lift ← f a
    match __do_lift with
      | none => filterMapM f l
      | some b => do
        let __do_lift ← filterMapM f l
        pure (b :: __do_lift)

Tactic:
conv => lhs; unfold filterMapM; unfold filterMapM.loop

Result:
m : Type u_1 → Type u_2
α β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
⊢ (do
      let __do_lift ← f a
      match __do_lift with
        | none => filterMapM.loop f l []
        | some b => filterMapM.loop f l [b]) =
    do
    let __do_lift ← f a
    match __do_lift with
      | none => filterMapM f l
      | some b => do
        let __do_lift ← filterMapM f l
        pure (b :: __do_lift)

Proof state:
case e_a
m : Type u_1 → Type u_2
α β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
⊢ (fun __do_lift =>
      match __do_lift with
      | none => filterMapM.loop f l []
      | some b => filterMapM.loop f l [b]) =
    fun __do_lift =>
    match __do_lift with
    | none => filterMapM f l
    | some b => do
      let __do_lift ← filterMapM f l
      pure (b :: __do_lift)

Tactic:
funext b?

Result:
case e_a.h
m : Type u_1 → Type u_2
α β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
b? : Option β
⊢ (match b? with
    | none => filterMapM.loop f l []
    | some b => filterMapM.loop f l [b]) =
    match b? with
    | none => filterMapM f l
    | some b => do
      let __do_lift ← filterMapM f l
      pure (b :: __do_lift)

Proof state:
case e_a.h.h_2
m : Type u_1 → Type u_2
α β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
__do_lift✝ : Option β
b : β
⊢ filterMapM.loop f l [b] =
    match some b with
    | none => filterMapM f l
    | some b => do
      let __do_lift ← filterMapM f l
      pure (b :: __do_lift)

Tactic:
simp only [bind_pure_comp]

Result:
case e_a.h.h_2
m : Type u_1 → Type u_2
α β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
__do_lift✝ : Option β
b : β
⊢ filterMapM.loop f l [b] = cons b <$> filterMapM f l

Proof state:
case e_a.h
m : Type u_1 → Type u_2
α β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
b? : Option β
⊢ (match b? with
    | none => filterMapM.loop f l []
    | some b => filterMapM.loop f l [b]) =
    match b? with
    | none => filterMapM f l
    | some b => do
      let __do_lift ← filterMapM f l
      pure (b :: __do_lift)

Tactic:
split <;> rename_i b

Result:
case e_a.h.h_1
m : Type u_1 → Type u_2
α β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
b : Option β
⊢ filterMapM.loop f l [] =
    match none with
    | none => filterMapM f l
    | some b => do
      let __do_lift ← filterMapM f l
      pure (b :: __do_lift)

case e_a.h.h_2
m : Type u_1 → Type u_2
α β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
__do_lift✝ : Option β
b : β
⊢ filterMapM.loop f l [b] =
    match some b with
    | none => filterMapM f l
    | some b => do
      let __do_lift ← filterMapM f l
      pure (b :: __do_lift)