-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Monadic.lean
theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
    (l : Vector α n) (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:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
init : β
l : Array α
f : (a : α) → a ∈ { toArray := l, size_toArray := ⋯ } → β → m (ForInStep β)
⊢ forIn' { toArray := l, size_toArray := ⋯ } init f =
    ForInStep.value <$>
      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) { toArray := l, size_toArray := ⋯ }.attach

Tactic:
simp [Array.forIn'_eq_foldlM]

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
init : β
l : Array α
f : (a : α) → a ∈ { toArray := l, size_toArray := ⋯ } → β → m (ForInStep β)
⊢ ForInStep.value <$>
      Array.foldlM
        (fun x y =>
          match x with
          | ForInStep.yield b => f y.val ⋯ b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l.attach 0 l.size =
    ForInStep.value <$>
      Array.foldlM
        (fun x y =>
          match x with
          | ForInStep.yield b => f y.val ⋯ b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l.attach 0 l.size

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Vector α n
f : (a : α) → a ∈ l → β → m (ForInStep β)
init : β
⊢ forIn' l init f =
    ForInStep.value <$>
      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) l.attach

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
init : β
l : Array α
f : (a : α) → a ∈ { toArray := l, size_toArray := ⋯ } → β → m (ForInStep β)
⊢ forIn' { toArray := l, size_toArray := ⋯ } init f =
    ForInStep.value <$>
      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) { toArray := l, size_toArray := ⋯ }.attach

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
init : β
l : Array α
f : (a : α) → a ∈ { toArray := l, size_toArray := ⋯ } → β → m (ForInStep β)
⊢ ForInStep.value <$>
      Array.foldlM
        (fun x y =>
          match x with
          | ForInStep.yield b => f y.val ⋯ b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l.attach 0 l.size =
    ForInStep.value <$>
      Array.foldlM
        (fun x y =>
          match x with
          | ForInStep.yield b => f y.val ⋯ b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l.attach 0 l.size

Tactic:
rfl

Result:
no goals