-- 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.intro.e_a.h.yield
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
b : β
⊢ ∀ (a_1 : α) (m_1 : a_1 ∈ as) (b : β), f a_1 ⋯ b = g a_1 ⋯ b

Tactic:
intro a m b

Result:
case cons.cons.intro.e_a.h.yield
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 : a ∈ as) (b : β), f a ⋯ b = g a m b) → forIn' as_1 b f = forIn' as b' g
g : (a' : α) → a' ∈ a✝ :: as → β → m✝ (ForInStep β)
w : a✝ :: as = a✝ :: as
h : ∀ (a : α) (m : a ∈ a✝ :: as) (b : β), f a ⋯ b = g a m b
b✝ : β
a : α
m : a ∈ as
b : β
⊢ f a ⋯ b = g a ⋯ b

Proof state:
case cons.cons.intro.e_a.h.yield
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
b : β
⊢ (forIn' as b fun a' m b => f a' ⋯ b) = forIn' as b fun a' m b => g a' ⋯ b

Tactic:
rw [ih rfl rfl]

Result:
case cons.cons.intro.e_a.h.yield
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
b : β
⊢ ∀ (a_1 : α) (m_1 : a_1 ∈ as) (b : β), f a_1 ⋯ b = g a_1 ⋯ b

Proof state:
case nil
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
b b' : β
hb : b = b'
g f : (a' : α) → a' ∈ [] → β → m (ForInStep β)
h : ∀ (a : α) (m_1 : a ∈ []) (b : β), f a ⋯ b = g a m_1 b
⊢ forIn' [] b f = forIn' [] b' g

Tactic:
simp [hb, forIn'_nil]

Result:
no goals

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

Tactic:
funext s

Result:
case cons.cons.intro.e_a.h
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
s : ForInStep β
⊢ (match s with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn' as b fun a' m b => f a' ⋯ b) =
    match s with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn' as b fun a' m b => g a' ⋯ b

Proof state:
case cons.cons.intro.e_a.h.yield
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
b : β
⊢ (match ForInStep.yield b with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn' as b fun a' m b => f a' ⋯ b) =
    match ForInStep.yield b with
    | ForInStep.done b => pure b
    | ForInStep.yield b => forIn' as b fun a' m b => g a' ⋯ b

Tactic:
simp

Result:
case cons.cons.intro.e_a.h.yield
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
b : β
⊢ (forIn' as b fun a' m b => f a' ⋯ b) = forIn' as b fun a' m b => g a' ⋯ b

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

Tactic:
simp [h, hb]

Result:
no goals