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

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

Tactic:
induction l generalizing acc with
| nil => simp [flatMapM.loop]
| cons a l ih =>
  simp only [flatMapM.loop, append_nil, _root_.map_bind]
  congr
  funext bs
  rw [ih, ih [bs]]
  simp

Result:
no goals

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

Tactic:
rw [ih, ih [bs]]

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

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

Tactic:
funext bs

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

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

Tactic:
congr

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

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

Tactic:
simp only [flatMapM.loop, append_nil, _root_.map_bind]

Result:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (List β)
a : α
l : List α
ih : ∀ (acc : List (List β)), flatMapM.loop f l acc = (fun x => acc.reverse.flatten ++ x) <$> flatMapM.loop f l []
acc : List (List β)
⊢ (do
      let bs' ← f a
      flatMapM.loop f l (bs' :: acc)) =
    do
    let a ← f a
    (fun x => acc.reverse.flatten ++ x) <$> flatMapM.loop f l [a]

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

Tactic:
simp

Result:
no goals

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

Tactic:
simp [flatMapM.loop]

Result:
no goals