-- 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 nil
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
b : β
ha : ∃ ys, ys ++ [] = as
hb : ∃ ys, ys ++ [] = bs
⊢ forIn'.loop as f [] b ha = forIn'.loop bs g [] b hb

Tactic:
simp [forIn'.loop]

Result:
no goals

Proof state:
case cons
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
⊢ forIn'.loop as f (a :: xs) b ha = forIn'.loop bs g (a :: xs) b hb

Tactic:
simp only [forIn'.loop] at *

Result:
case cons
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
⊢ (do
      let __do_lift ← f a ⋯ b
      match __do_lift with
        | ForInStep.done b => pure b
        | ForInStep.yield b => forIn'.loop as f xs b ⋯) =
    do
    let __do_lift ← g a ⋯ b
    match __do_lift with
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn'.loop bs g xs b ⋯

Proof state:
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 ⋯

Tactic:
rfl

Result:
no goals

Proof state:
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 ⋯

Tactic:
simp

Result:
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 : β
⊢ forIn'.loop as f xs b ⋯ = forIn'.loop bs g xs b ⋯

Proof state:
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 : β
⊢ forIn'.loop as f xs b ⋯ = forIn'.loop bs g xs b ⋯

Tactic:
rw [ih]

Result:
no goals

Proof state:
case cons
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
⊢ (do
      let __do_lift ← f a ⋯ b
      match __do_lift with
        | ForInStep.done b => pure b
        | ForInStep.yield b => forIn'.loop as f xs b ⋯) =
    do
    let __do_lift ← g a ⋯ b
    match __do_lift with
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn'.loop bs g xs b ⋯

Tactic:
congr 1

Result:
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
⊢ f a ⋯ b = g a ⋯ b

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 ⋯

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
⊢ f a ⋯ b = g a ⋯ b

Tactic:
rw [h]

Result:
no goals