-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
    (f : α → β → m (ForInStep β)) (init : β) (l : List α) :
    forIn l init f = ForInStep.value <$>
      l.foldlM (fun b a => match b with
        | .yield b => f a 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
f : α → β → m (ForInStep β)
a : α
as : List α
init : β
x : ForInStep β
b : β
⊢ pure b =
    ForInStep.value <$>
      List.foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => f a b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.done b) as

Tactic:
induction as with
| nil => simp
| cons a as ih => simp [ih]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m (ForInStep β)
init : β
l : List α
⊢ forIn l init f =
    ForInStep.value <$>
      List.foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => f a b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l

Tactic:
induction l generalizing init with
| nil => simp
| cons a as ih =>
  simp only [foldlM_cons, bind_pure_comp, forIn_cons, _root_.map_bind]
  congr 1
  funext x
  match x with
  | .done b =>
    clear ih
    dsimp
    induction as with
    | nil => simp
    | cons a as ih => simp [ih]
  | .yield b =>
    simp [ih]

Result:
no goals

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

Tactic:
dsimp

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

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 (ForInStep β)
a : α
as : List α
ih :
  ∀ (init : β),
    forIn as init f =
      ForInStep.value <$>
        List.foldlM
          (fun b a =>
            match b with
            | ForInStep.yield b => f a b
            | ForInStep.done b => pure (ForInStep.done b))
          (ForInStep.yield init) as
init : β
⊢ (fun x =>
      match x with
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn as b f) =
    fun a =>
    ForInStep.value <$>
      List.foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => f a b
          | ForInStep.done b => pure (ForInStep.done b))
        a as

Tactic:
funext x

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 (ForInStep β)
a : α
as : List α
ih :
  ∀ (init : β),
    forIn as init f =
      ForInStep.value <$>
        List.foldlM
          (fun b a =>
            match b with
            | ForInStep.yield b => f a b
            | ForInStep.done b => pure (ForInStep.done b))
          (ForInStep.yield init) as
init : β
x : ForInStep β
⊢ (match x with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn as b f) =
    ForInStep.value <$>
      List.foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => f a b
          | ForInStep.done b => pure (ForInStep.done b))
        x as

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 (ForInStep β)
a : α
as : List α
ih :
  ∀ (init : β),
    forIn as init f =
      ForInStep.value <$>
        List.foldlM
          (fun b a =>
            match b with
            | ForInStep.yield b => f a b
            | ForInStep.done b => pure (ForInStep.done b))
          (ForInStep.yield init) as
init : β
⊢ (do
      let x ← f a init
      match x with
        | ForInStep.done b => pure b
        | ForInStep.yield b => forIn as b f) =
    do
    let a ← f a init
    ForInStep.value <$>
        List.foldlM
          (fun b a =>
            match b with
            | ForInStep.yield b => f a b
            | ForInStep.done b => pure (ForInStep.done b))
          a as

Tactic:
congr 1

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 (ForInStep β)
a : α
as : List α
ih :
  ∀ (init : β),
    forIn as init f =
      ForInStep.value <$>
        List.foldlM
          (fun b a =>
            match b with
            | ForInStep.yield b => f a b
            | ForInStep.done b => pure (ForInStep.done b))
          (ForInStep.yield init) as
init : β
⊢ (fun x =>
      match x with
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn as b f) =
    fun a =>
    ForInStep.value <$>
      List.foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => f a b
          | ForInStep.done b => pure (ForInStep.done b))
        a as

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 (ForInStep β)
a✝ : α
init : β
x : ForInStep β
b : β
a : α
as : List α
ih :
  pure b =
    ForInStep.value <$>
      List.foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => f a b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.done b) as
⊢ pure b =
    ForInStep.value <$>
      List.foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => f a b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.done b) (a :: as)

Tactic:
simp [ih]

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 (ForInStep β)
init : β
⊢ forIn [] init f =
    ForInStep.value <$>
      List.foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => f a b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) []

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
f : α → β → m (ForInStep β)
a : α
as : List α
ih :
  ∀ (init : β),
    forIn as init f =
      ForInStep.value <$>
        List.foldlM
          (fun b a =>
            match b with
            | ForInStep.yield b => f a b
            | ForInStep.done b => pure (ForInStep.done b))
          (ForInStep.yield init) as
init : β
x : ForInStep β
b : β
⊢ (match ForInStep.done b with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn as b f) =
    ForInStep.value <$>
      List.foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => f a b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.done b) as

Tactic:
clear ih

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