-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem forIn'_congr [Monad m] {as bs : List α} (w : as = bs)
    {b b' : β} (hb : b = b')
    {f : (a' : α) → a' ∈ as → β → m (ForInStep β)}
    {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)}
    (h : ∀ a m b, f a (by simpa [w] using m) b = g a m b) :
    forIn' as b f = forIn' bs b' g

Proof state:
case cons.cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
b✝ : α
bs : List α
ih :
  ∀ {as : List α} (w : as = bs) {b b' : β},
    b = b' →
      ∀ {f : (a' : α) → a' ∈ as → β → m (ForInStep β)} {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)},
        (∀ (a : α) (m_1 : a ∈ bs) (b : β), f a ⋯ b = g a m_1 b) → forIn' as b f = forIn' bs b' g
b b' : β
hb : b = b'
g : (a' : α) → a' ∈ b✝ :: bs → β → m (ForInStep β)
a : α
as : List α
w : a :: as = b✝ :: bs
f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
h : ∀ (a_1 : α) (m_1 : a_1 ∈ b✝ :: bs) (b : β), f a_1 ⋯ b = g a_1 m_1 b
⊢ forIn' (a :: as) b f = forIn' (b✝ :: bs) b' g

Tactic:
simp only [cons.injEq] at w

Result:
case cons.cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
b✝ : α
bs : List α
ih :
  ∀ {as : List α} (w : as = bs) {b b' : β},
    b = b' →
      ∀ {f : (a' : α) → a' ∈ as → β → m (ForInStep β)} {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)},
        (∀ (a : α) (m_1 : a ∈ bs) (b : β), f a ⋯ b = g a m_1 b) → forIn' as b f = forIn' bs b' g
b b' : β
hb : b = b'
g : (a' : α) → a' ∈ b✝ :: bs → β → m (ForInStep β)
a : α
as : List α
w✝ : a :: as = b✝ :: bs
f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
h : ∀ (a_1 : α) (m_1 : a_1 ∈ b✝ :: bs) (b : β), f a_1 ⋯ b = g a_1 m_1 b
w : a = b✝ ∧ as = bs
⊢ forIn' (a :: as) b f = forIn' (b✝ :: bs) b' g

Proof state:
case cons.cons.intro
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
b b' : β
hb : b = b'
a : α
as : List α
f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
ih :
  ∀ {as_1 : List α} (w : as_1 = as) {b b' : β},
    b = b' →
      ∀ {f : (a' : α) → a' ∈ as_1 → β → m (ForInStep β)} {g : (a' : α) → a' ∈ as → β → m (ForInStep β)},
        (∀ (a : α) (m_1 : a ∈ as) (b : β), f a ⋯ b = g a m_1 b) → forIn' as_1 b f = forIn' as b' g
g : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
w : a :: as = a :: as
h : ∀ (a_1 : α) (m_1 : a_1 ∈ a :: as) (b : β), f a_1 ⋯ b = g a_1 m_1 b
⊢ (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) =
    do
    let x ← g a ⋯ b'
    match x with
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn' as b fun a' m b => g a' ⋯ b

Tactic:
congr 1

Result:
case cons.cons.intro.e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
b b' : β
hb : b = b'
a : α
as : List α
f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
ih :
  ∀ {as_1 : List α} (w : as_1 = as) {b b' : β},
    b = b' →
      ∀ {f : (a' : α) → a' ∈ as_1 → β → m (ForInStep β)} {g : (a' : α) → a' ∈ as → β → m (ForInStep β)},
        (∀ (a : α) (m_1 : a ∈ as) (b : β), f a ⋯ b = g a m_1 b) → forIn' as_1 b f = forIn' as b' g
g : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
w : a :: as = a :: as
h : ∀ (a_1 : α) (m_1 : a_1 ∈ a :: as) (b : β), f a_1 ⋯ b = g a_1 m_1 b
⊢ f a ⋯ b = g a ⋯ b'

case cons.cons.intro.e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
b b' : β
hb : b = b'
a : α
as : List α
f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
ih :
  ∀ {as_1 : List α} (w : as_1 = as) {b b' : β},
    b = b' →
      ∀ {f : (a' : α) → a' ∈ as_1 → β → m (ForInStep β)} {g : (a' : α) → a' ∈ as → β → m (ForInStep β)},
        (∀ (a : α) (m_1 : a ∈ as) (b : β), f a ⋯ b = g a m_1 b) → forIn' as_1 b f = forIn' as b' g
g : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
w : a :: as = a :: as
h : ∀ (a_1 : α) (m_1 : a_1 ∈ a :: as) (b : β), f a_1 ⋯ b = g a_1 m_1 b
⊢ (fun x =>
      match x with
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn' as b fun a' m b => f a' ⋯ b) =
    fun x =>
    match x with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn' as b fun a' m b => g a' ⋯ b

Proof state:
case cons.cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
b✝ : α
bs : List α
ih :
  ∀ {as : List α} (w : as = bs) {b b' : β},
    b = b' →
      ∀ {f : (a' : α) → a' ∈ as → β → m (ForInStep β)} {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)},
        (∀ (a : α) (m_1 : a ∈ bs) (b : β), f a ⋯ b = g a m_1 b) → forIn' as b f = forIn' bs b' g
b b' : β
hb : b = b'
g : (a' : α) → a' ∈ b✝ :: bs → β → m (ForInStep β)
a : α
as : List α
w✝ : a :: as = b✝ :: bs
f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
h : ∀ (a_1 : α) (m_1 : a_1 ∈ b✝ :: bs) (b : β), f a_1 ⋯ b = g a_1 m_1 b
w : a = b✝ ∧ as = bs
⊢ forIn' (a :: as) b f = forIn' (b✝ :: bs) b' g

Tactic:
obtain ⟨rfl, rfl⟩ := w

Result:
case cons.cons.intro
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
b b' : β
hb : b = b'
a : α
as : List α
f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
ih :
  ∀ {as_1 : List α} (w : as_1 = as) {b b' : β},
    b = b' →
      ∀ {f : (a' : α) → a' ∈ as_1 → β → m (ForInStep β)} {g : (a' : α) → a' ∈ as → β → m (ForInStep β)},
        (∀ (a : α) (m_1 : a ∈ as) (b : β), f a ⋯ b = g a m_1 b) → forIn' as_1 b f = forIn' as b' g
g : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)
w : a :: as = a :: as
h : ∀ (a_1 : α) (m_1 : a_1 ∈ a :: as) (b : β), f a_1 ⋯ b = g a_1 m_1 b
⊢ forIn' (a :: as) b f = forIn' (a :: as) b' g