-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/List.lean
theorem forIn'_some [Monad m] [LawfulMonad m] (a : α) (b : β) (f : (a' : α) → a' ∈ some a → β → m (ForInStep β)) :
    forIn' (some a) b f = bind (f a rfl b) (fun r => pure (ForInStep.value r))

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
b : β
f : (a' : α) → a' ∈ some a → β → m (ForInStep β)
⊢ forIn' (some a) b f = do
    let r ← f a ⋯ b
    pure r.value

Tactic:
simp only [forIn', bind_pure_comp]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
b : β
f : (a' : α) → a' ∈ some a → β → m (ForInStep β)
⊢ (do
      let __do_lift ← f a ⋯ b
      match __do_lift with
        | ForInStep.done r => pure r
        | ForInStep.yield r => pure r) =
    ForInStep.value <$> f a ⋯ b

Proof state:
case e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
b : β
f : (a' : α) → a' ∈ some a → β → m (ForInStep β)
⊢ (fun __do_lift =>
      match __do_lift with
      | ForInStep.done r => pure r
      | ForInStep.yield r => pure r) =
    fun a => pure a.value

Tactic:
funext x

Result:
case e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
b : β
f : (a' : α) → a' ∈ some a → β → m (ForInStep β)
x : ForInStep β
⊢ (match x with
    | ForInStep.done r => pure r
    | ForInStep.yield r => pure r) =
    pure x.value

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
b : β
f : (a' : α) → a' ∈ some a → β → m (ForInStep β)
⊢ (do
      let __do_lift ← f a ⋯ b
      match __do_lift with
        | ForInStep.done r => pure r
        | ForInStep.yield r => pure r) =
    do
    let a ← f a ⋯ b
    pure a.value

Tactic:
congr

Result:
case e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
b : β
f : (a' : α) → a' ∈ some a → β → m (ForInStep β)
⊢ (fun __do_lift =>
      match __do_lift with
      | ForInStep.done r => pure r
      | ForInStep.yield r => pure r) =
    fun a => pure a.value

Proof state:
case e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
b : β
f : (a' : α) → a' ∈ some a → β → m (ForInStep β)
x : ForInStep β
⊢ (match x with
    | ForInStep.done r => pure r
    | ForInStep.yield r => pure r) =
    pure x.value

Tactic:
split <;> rfl

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 : α
b : β
f : (a' : α) → a' ∈ some a → β → m (ForInStep β)
⊢ (do
      let __do_lift ← f a ⋯ b
      match __do_lift with
        | ForInStep.done r => pure r
        | ForInStep.yield r => pure r) =
    ForInStep.value <$> f a ⋯ b

Tactic:
rw [map_eq_pure_bind]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
b : β
f : (a' : α) → a' ∈ some a → β → m (ForInStep β)
⊢ (do
      let __do_lift ← f a ⋯ b
      match __do_lift with
        | ForInStep.done r => pure r
        | ForInStep.yield r => pure r) =
    do
    let a ← f a ⋯ b
    pure a.value