-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem forIn'_loop_congr [Monad m] {as bs : List α}
    {f : (a' : α) → a' ∈ as → β → m (ForInStep β)}
    {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)}
    {b : β} (ha : ∃ ys, ys ++ xs = as) (hb : ∃ ys, ys ++ xs = bs)
    (h : ∀ a m m' b, f a m b = g a m' b) : forIn'.loop as f xs b ha = forIn'.loop bs g xs b hb

Proof state:
case cons.e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
as bs : List α
f : (a' : α) → a' ∈ as → β → m (ForInStep β)
g : (a' : α) → a' ∈ bs → β → m (ForInStep β)
h : ∀ (a : α) (m_1 : a ∈ as) (m' : a ∈ bs) (b : β), f a m_1 b = g a m' b
a : α
xs : List α
ih :
  ∀ {b : β} (ha : ∃ ys, ys ++ xs = as) (hb : ∃ ys, ys ++ xs = bs), forIn'.loop as f xs b ha = forIn'.loop bs g xs b hb
b : β
ha : ∃ ys, ys ++ a :: xs = as
hb : ∃ ys, ys ++ a :: xs = bs
⊢ (fun __do_lift =>
      match __do_lift with
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn'.loop as f xs b ⋯) =
    fun __do_lift =>
    match __do_lift with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn'.loop bs g xs b ⋯

Tactic:
funext s

Result:
case cons.e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
as bs : List α
f : (a' : α) → a' ∈ as → β → m (ForInStep β)
g : (a' : α) → a' ∈ bs → β → m (ForInStep β)
h : ∀ (a : α) (m_1 : a ∈ as) (m' : a ∈ bs) (b : β), f a m_1 b = g a m' b
a : α
xs : List α
ih :
  ∀ {b : β} (ha : ∃ ys, ys ++ xs = as) (hb : ∃ ys, ys ++ xs = bs), forIn'.loop as f xs b ha = forIn'.loop bs g xs b hb
b : β
ha : ∃ ys, ys ++ a :: xs = as
hb : ∃ ys, ys ++ a :: xs = bs
s : ForInStep β
⊢ (match s with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn'.loop as f xs b ⋯) =
    match s with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn'.loop bs g xs b ⋯

Proof state:
case cons.e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
as bs : List α
f : (a' : α) → a' ∈ as → β → m (ForInStep β)
g : (a' : α) → a' ∈ bs → β → m (ForInStep β)
h : ∀ (a : α) (m_1 : a ∈ as) (m' : a ∈ bs) (b : β), f a m_1 b = g a m' b
a : α
xs : List α
ih :
  ∀ {b : β} (ha : ∃ ys, ys ++ xs = as) (hb : ∃ ys, ys ++ xs = bs), forIn'.loop as f xs b ha = forIn'.loop bs g xs b hb
b : β
ha : ∃ ys, ys ++ a :: xs = as
hb : ∃ ys, ys ++ a :: xs = bs
s : ForInStep β
⊢ (match s with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn'.loop as f xs b ⋯) =
    match s with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn'.loop bs g xs b ⋯

Tactic:
obtain b | b := s

Result:
case cons.e_a.h.done
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
as bs : List α
f : (a' : α) → a' ∈ as → β → m (ForInStep β)
g : (a' : α) → a' ∈ bs → β → m (ForInStep β)
h : ∀ (a : α) (m_1 : a ∈ as) (m' : a ∈ bs) (b : β), f a m_1 b = g a m' b
a : α
xs : List α
ih :
  ∀ {b : β} (ha : ∃ ys, ys ++ xs = as) (hb : ∃ ys, ys ++ xs = bs), forIn'.loop as f xs b ha = forIn'.loop bs g xs b hb
b✝ : β
ha : ∃ ys, ys ++ a :: xs = as
hb : ∃ ys, ys ++ a :: xs = bs
b : β
⊢ (match ForInStep.done b with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn'.loop as f xs b ⋯) =
    match ForInStep.done b with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn'.loop bs g xs b ⋯

case cons.e_a.h.yield
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
as bs : List α
f : (a' : α) → a' ∈ as → β → m (ForInStep β)
g : (a' : α) → a' ∈ bs → β → m (ForInStep β)
h : ∀ (a : α) (m_1 : a ∈ as) (m' : a ∈ bs) (b : β), f a m_1 b = g a m' b
a : α
xs : List α
ih :
  ∀ {b : β} (ha : ∃ ys, ys ++ xs = as) (hb : ∃ ys, ys ++ xs = bs), forIn'.loop as f xs b ha = forIn'.loop bs g xs b hb
b✝ : β
ha : ∃ ys, ys ++ a :: xs = as
hb : ∃ ys, ys ++ a :: xs = bs
b : β
⊢ (match ForInStep.yield b with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn'.loop as f xs b ⋯) =
    match ForInStep.yield b with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn'.loop bs g xs b ⋯