-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem filterMapM_loop_eq [Monad m] [LawfulMonad m]
    (f : α → m (Option β)) (l : List α) (acc : List β) :
    filterMapM.loop f l acc = (acc.reverse ++ ·) <$> filterMapM.loop f l []

Proof state:
case cons
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
a : α
l : List α
ih : ∀ (acc : List β), filterMapM.loop f l acc = (fun x => acc.reverse ++ x) <$> filterMapM.loop f l []
acc : List β
⊢ (do
      let __do_lift ← f a
      match __do_lift with
        | none => filterMapM.loop f l acc
        | some b => filterMapM.loop f l (b :: acc)) =
    do
    let a ← f a
    (fun x => acc.reverse ++ x) <$>
        match a with
        | none => filterMapM.loop f l []
        | some b => filterMapM.loop f l [b]

Tactic:
congr

Result:
case cons.e_a
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
a : α
l : List α
ih : ∀ (acc : List β), filterMapM.loop f l acc = (fun x => acc.reverse ++ x) <$> filterMapM.loop f l []
acc : List β
⊢ (fun __do_lift =>
      match __do_lift with
      | none => filterMapM.loop f l acc
      | some b => filterMapM.loop f l (b :: acc)) =
    fun a =>
    (fun x => acc.reverse ++ x) <$>
      match a with
      | none => filterMapM.loop f l []
      | some b => filterMapM.loop f l [b]

Proof state:
case cons.e_a.h
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
a : α
l : List α
ih : ∀ (acc : List β), filterMapM.loop f l acc = (fun x => acc.reverse ++ x) <$> filterMapM.loop f l []
acc : List β
b? : Option β
⊢ (match b? with
    | none => filterMapM.loop f l acc
    | some b => filterMapM.loop f l (b :: acc)) =
    (fun x => acc.reverse ++ x) <$>
      match b? with
      | none => filterMapM.loop f l []
      | some b => filterMapM.loop f l [b]

Tactic:
split <;> rename_i b

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

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

Proof state:
case nil
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
acc : List β
⊢ filterMapM.loop f [] acc = (fun x => acc.reverse ++ x) <$> filterMapM.loop f [] []

Tactic:
simp [filterMapM.loop]

Result:
no goals

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

Tactic:
simp

Result:
no goals

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

Tactic:
simp only [filterMapM.loop, _root_.map_bind]

Result:
case cons
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
a : α
l : List α
ih : ∀ (acc : List β), filterMapM.loop f l acc = (fun x => acc.reverse ++ x) <$> filterMapM.loop f l []
acc : List β
⊢ (do
      let __do_lift ← f a
      match __do_lift with
        | none => filterMapM.loop f l acc
        | some b => filterMapM.loop f l (b :: acc)) =
    do
    let a ← f a
    (fun x => acc.reverse ++ x) <$>
        match a with
        | none => filterMapM.loop f l []
        | some b => filterMapM.loop f l [b]

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

Tactic:
apply ih

Result:
no goals

Proof state:
case cons.e_a
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
a : α
l : List α
ih : ∀ (acc : List β), filterMapM.loop f l acc = (fun x => acc.reverse ++ x) <$> filterMapM.loop f l []
acc : List β
⊢ (fun __do_lift =>
      match __do_lift with
      | none => filterMapM.loop f l acc
      | some b => filterMapM.loop f l (b :: acc)) =
    fun a =>
    (fun x => acc.reverse ++ x) <$>
      match a with
      | none => filterMapM.loop f l []
      | some b => filterMapM.loop f l [b]

Tactic:
funext b?

Result:
case cons.e_a.h
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
a : α
l : List α
ih : ∀ (acc : List β), filterMapM.loop f l acc = (fun x => acc.reverse ++ x) <$> filterMapM.loop f l []
acc : List β
b? : Option β
⊢ (match b? with
    | none => filterMapM.loop f l acc
    | some b => filterMapM.loop f l (b :: acc)) =
    (fun x => acc.reverse ++ x) <$>
      match b? with
      | none => filterMapM.loop f l []
      | some b => filterMapM.loop f l [b]

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

Tactic:
rw [ih, ih [b]]

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