-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
    (l : List α) (f : (a : α) → a ∈ l → β → m (ForInStep β)) (init : β) :
    forIn' l init f = ForInStep.value <$>
      l.attach.foldlM (fun b ⟨a, m⟩ => match b with
        | .yield b => f a m b
        | .done b => pure (.done b)) (ForInStep.yield init)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
as : List α
ih :
  ∀ (f : (a : α) → a ∈ as → β → m (ForInStep β)) (init : β),
    forIn' as init f =
      ForInStep.value <$>
        List.foldlM
          (fun b x =>
            match x with
            | ⟨a, m_1⟩ =>
              match b with
              | ForInStep.yield b => f a m_1 b
              | ForInStep.done b => pure (ForInStep.done b))
          (ForInStep.yield init) as.attach
f : (a_1 : α) → a_1 ∈ a :: as → β → m (ForInStep β)
init : β
x : ForInStep β
b : β
⊢ (match ForInStep.yield b with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn' as b fun a' m b => f a' ⋯ b) =
    ForInStep.value <$>
      List.foldlM
        (fun b x =>
          match b with
          | ForInStep.yield b => f x.val ⋯ b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield b) (map (fun x => ⟨x.val, ⋯⟩) as.attach)

Tactic:
simp [ih, List.foldlM_map]

Result:
no goals

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
as : List α
ih :
  ∀ (f : (a : α) → a ∈ as → β → m (ForInStep β)) (init : β),
    forIn' as init f =
      ForInStep.value <$>
        List.foldlM
          (fun b x =>
            match x with
            | ⟨a, m_1⟩ =>
              match b with
              | ForInStep.yield b => f a m_1 b
              | ForInStep.done b => pure (ForInStep.done b))
          (ForInStep.yield init) as.attach
f : (a_1 : α) → a_1 ∈ a :: as → β → m (ForInStep β)
init : β
⊢ forIn' (a :: as) init f =
    ForInStep.value <$>
      List.foldlM
        (fun b x =>
          match x with
          | ⟨a_1, m_1⟩ =>
            match b with
            | ForInStep.yield b => f a_1 m_1 b
            | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) (a :: as).attach

Tactic:
simp only [forIn'_cons, attach_cons, foldlM_cons, _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
a : α
as : List α
ih :
  ∀ (f : (a : α) → a ∈ as → β → m (ForInStep β)) (init : β),
    forIn' as init f =
      ForInStep.value <$>
        List.foldlM
          (fun b x =>
            match x with
            | ⟨a, m_1⟩ =>
              match b with
              | ForInStep.yield b => f a m_1 b
              | ForInStep.done b => pure (ForInStep.done b))
          (ForInStep.yield init) as.attach
f : (a_1 : α) → a_1 ∈ a :: as → β → m (ForInStep β)
init : β
⊢ (do
      let x ← f a ⋯ init
      match x with
        | ForInStep.done b => pure b
        | ForInStep.yield b => forIn' as b fun a' m b => f a' ⋯ b) =
    do
    let a_1 ← f a ⋯ init
    ForInStep.value <$>
        List.foldlM
          (fun b x =>
            match b with
            | ForInStep.yield b => f x.val ⋯ b
            | ForInStep.done b => pure (ForInStep.done b))
          a_1 (map (fun x => ⟨x.val, ⋯⟩) as.attach)

Proof state:
case nil
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
init : β
x : ForInStep β
b : β
f : (a_1 : α) → a_1 ∈ [a] → β → m (ForInStep β)
⊢ pure b =
    ForInStep.value <$>
      List.foldlM
        (fun b x =>
          match b with
          | ForInStep.yield b => f x.val ⋯ b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.done b) (map (fun x => ⟨x.val, ⋯⟩) [].attach)

Tactic:
simp

Result:
no goals

Proof state:
m✝ : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m✝
inst✝ : LawfulMonad m✝
a✝¹ : α
init : β
x : ForInStep β
b✝ : β
a✝ : α
as : List α
ih :
  ∀ (f : (a : α) → a ∈ a✝¹ :: as → β → m✝ (ForInStep β)),
    pure b✝ =
      ForInStep.value <$>
        List.foldlM
          (fun b x =>
            match b with
            | ForInStep.yield b => f x.val ⋯ b
            | ForInStep.done b => pure (ForInStep.done b))
          (ForInStep.done b✝) (map (fun x => ⟨x.val, ⋯⟩) as.attach)
f : (a : α) → a ∈ a✝¹ :: a✝ :: as → β → m✝ (ForInStep β)
a : α
m : a ∈ a✝¹ :: as
b : β
⊢ a ∈ a✝¹ :: a✝ :: as

Tactic:
simp only [mem_cons] at m

Result:
m✝ : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m✝
inst✝ : LawfulMonad m✝
a✝¹ : α
init : β
x : ForInStep β
b✝ : β
a✝ : α
as : List α
ih :
  ∀ (f : (a : α) → a ∈ a✝¹ :: as → β → m✝ (ForInStep β)),
    pure b✝ =
      ForInStep.value <$>
        List.foldlM
          (fun b x =>
            match b with
            | ForInStep.yield b => f x.val ⋯ b
            | ForInStep.done b => pure (ForInStep.done b))
          (ForInStep.done b✝) (map (fun x => ⟨x.val, ⋯⟩) as.attach)
f : (a : α) → a ∈ a✝¹ :: a✝ :: as → β → m✝ (ForInStep β)
a : α
b : β
m : a = a✝¹ ∨ a ∈ as
⊢ a ∈ a✝¹ :: a✝ :: as

Proof state:
case inr
m✝ : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m✝
inst✝ : LawfulMonad m✝
a✝¹ : α
init : β
x : ForInStep β
b✝ : β
a✝ : α
as : List α
ih :
  ∀ (f : (a : α) → a ∈ a✝¹ :: as → β → m✝ (ForInStep β)),
    pure b✝ =
      ForInStep.value <$>
        List.foldlM
          (fun b x =>
            match b with
            | ForInStep.yield b => f x.val ⋯ b
            | ForInStep.done b => pure (ForInStep.done b))
          (ForInStep.done b✝) (map (fun x => ⟨x.val, ⋯⟩) as.attach)
f : (a : α) → a ∈ a✝¹ :: a✝ :: as → β → m✝ (ForInStep β)
a : α
b : β
m : a ∈ as
⊢ a ∈ a✝¹ :: a✝ :: as

Tactic:
exact mem_cons_of_mem _ (mem_cons_of_mem _ m)

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
as : List α
f : (a_1 : α) → a_1 ∈ a :: as → β → m (ForInStep β)
init : β
x : ForInStep β
b : β
⊢ (match ForInStep.done b with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn' as b fun a' m b => f a' ⋯ b) =
    ForInStep.value <$>
      List.foldlM
        (fun b x =>
          match b with
          | ForInStep.yield b => f x.val ⋯ b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.done b) (map (fun x => ⟨x.val, ⋯⟩) as.attach)

Tactic:
dsimp

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
as : List α
f : (a_1 : α) → a_1 ∈ a :: as → β → m (ForInStep β)
init : β
x : ForInStep β
b : β
⊢ pure b =
    ForInStep.value <$>
      List.foldlM
        (fun b x =>
          match b with
          | ForInStep.yield b => f x.val ⋯ b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.done b) (map (fun x => ⟨x.val, ⋯⟩) as.attach)