-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem forIn'_cons [Monad m] {a : α} {as : List α}
    (f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)) (b : β) :
    forIn' (a::as) b f = f a (mem_cons_self a as) b >>=
      fun | ForInStep.done b => pure b | ForInStep.yield b => forIn' as b fun a' m b => f a' (mem_cons_of_mem a m) b

Proof state:
case e_a.h.yield
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
a : α
as : List α
f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
b✝ b : β
⊢ (match ForInStep.yield b with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn'.loop (a :: as) f as b ⋯) =
    match ForInStep.yield b with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn'.loop as (fun a' m b => f a' ⋯ b) as b ⋯

Tactic:
apply forIn'_loop_congr

Result:
case e_a.h.yield.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
a : α
as : List α
f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
b✝ b : β
⊢ ∀ (a_1 : α) (m_1 : a_1 ∈ a :: as) (m' : a_1 ∈ as) (b : β), f a_1 m_1 b = f a_1 ⋯ b

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
a : α
as : List α
f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
b : β
⊢ (do
      let __do_lift ← f a ⋯ b
      match __do_lift with
        | ForInStep.done b => pure b
        | ForInStep.yield b => forIn'.loop (a :: as) f as b ⋯) =
    do
    let x ← f a ⋯ b
    match x with
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn'.loop as (fun a' m b => f a' ⋯ b) as b ⋯

Tactic:
congr 1

Result:
case e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
a : α
as : List α
f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
b : β
⊢ (fun __do_lift =>
      match __do_lift with
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn'.loop (a :: as) f as b ⋯) =
    fun x =>
    match x with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn'.loop as (fun a' m b => f a' ⋯ b) as b ⋯

Proof state:
case e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
a : α
as : List α
f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
b : β
s : ForInStep β
⊢ (match s with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn'.loop (a :: as) f as b ⋯) =
    match s with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn'.loop as (fun a' m b => f a' ⋯ b) as b ⋯

Tactic:
obtain b | b := s

Result:
case e_a.h.done
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
a : α
as : List α
f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
b✝ b : β
⊢ (match ForInStep.done b with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn'.loop (a :: as) f as b ⋯) =
    match ForInStep.done b with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn'.loop as (fun a' m b => f a' ⋯ b) as b ⋯

case e_a.h.yield
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
a : α
as : List α
f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
b✝ b : β
⊢ (match ForInStep.yield b with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn'.loop (a :: as) f as b ⋯) =
    match ForInStep.yield b with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn'.loop as (fun a' m b => f a' ⋯ b) as b ⋯

Proof state:
case e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
a : α
as : List α
f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
b : β
⊢ (fun __do_lift =>
      match __do_lift with
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn'.loop (a :: as) f as b ⋯) =
    fun x =>
    match x with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn'.loop as (fun a' m b => f a' ⋯ b) as b ⋯

Tactic:
funext s

Result:
case e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
a : α
as : List α
f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
b : β
s : ForInStep β
⊢ (match s with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn'.loop (a :: as) f as b ⋯) =
    match s with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn'.loop as (fun a' m b => f a' ⋯ b) as b ⋯

Proof state:
case e_a.h.yield.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
a : α
as : List α
f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
b✝¹ b : β
a✝ : α
m✝ : a✝ ∈ a :: as
m'✝ : a✝ ∈ as
b✝ : β
⊢ f a✝ m✝ b✝ = f a✝ ⋯ b✝

Tactic:
rfl

Result:
no goals

Proof state:
case e_a.h.done
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
a : α
as : List α
f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
b✝ b : β
⊢ (match ForInStep.done b with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn'.loop (a :: as) f as b ⋯) =
    match ForInStep.done b with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn'.loop as (fun a' m b => f a' ⋯ b) as b ⋯

Tactic:
rfl

Result:
no goals

Proof state:
case e_a.h.yield.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
a : α
as : List α
f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
b✝ b : β
⊢ ∀ (a_1 : α) (m_1 : a_1 ∈ a :: as) (m' : a_1 ∈ as) (b : β), f a_1 m_1 b = f a_1 ⋯ b

Tactic:
intros

Result:
case e_a.h.yield.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
a : α
as : List α
f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
b✝¹ b : β
a✝ : α
m✝ : a✝ ∈ a :: as
m'✝ : a✝ ∈ as
b✝ : β
⊢ f a✝ m✝ b✝ = f a✝ ⋯ b✝

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
a : α
as : List α
f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
b : β
⊢ forIn' (a :: as) b f = do
    let x ← f a ⋯ b
    match x with
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn' as b fun a' m b => f a' ⋯ b

Tactic:
simp only [forIn', List.forIn', forIn'.loop]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
a : α
as : List α
f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
b : β
⊢ (do
      let __do_lift ← f a ⋯ b
      match __do_lift with
        | ForInStep.done b => pure b
        | ForInStep.yield b => forIn'.loop (a :: as) f as b ⋯) =
    do
    let x ← f a ⋯ b
    match x with
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn'.loop as (fun a' m b => f a' ⋯ b) as b ⋯