-- 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.nil
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 β)
w : [] = b✝ :: bs
f : (a' : α) → a' ∈ [] → β → m (ForInStep β)
h : ∀ (a : α) (m_1 : a ∈ b✝ :: bs) (b : β), f a ⋯ b = g a m_1 b
⊢ forIn' [] b f = forIn' (b✝ :: bs) b' g

Tactic:
simp at w

Result:
no goals

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

Tactic:
rfl

Result:
no goals

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

Tactic:
exact h a (mem_cons_of_mem _ m) b

Result:
no goals

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
⊢ forIn' (a :: as) b f = forIn' (a :: as) b' g

Tactic:
simp only [forIn'_cons]

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
⊢ (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

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

Tactic:
subst w

Result:
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

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

Tactic:
obtain b | b := s

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

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

Proof state:
m✝ : Type ?u.51515 → Type ?u.51437
α : Type ?u.51442
β : Type ?u.51515
inst✝ : 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 β)
a : α
m : a ∈ bs
b : β
⊢ a ∈ as

Tactic:
simpa [w] using m

Result:
no goals