-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Monadic.lean
theorem forIn'_congr [Monad m] {as bs : Vector α n} (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:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝ : Monad m
as bs : Vector α n
w : as = bs
b b' : β
hb : b = b'
f : (a' : α) → a' ∈ as → β → m (ForInStep β)
g : (a' : α) → a' ∈ bs → β → m (ForInStep β)
h : ∀ (a : α) (m_1 : a ∈ bs) (b : β), f a ⋯ b = g a m_1 b
⊢ forIn' as b f = forIn' bs b' g

Tactic:
cases as <;> cases bs

Result:
case mk.mk
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝ : Monad m
b b' : β
hb : b = b'
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
f : (a' : α) → a' ∈ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } → β → m (ForInStep β)
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
g : (a' : α) → a' ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → β → m (ForInStep β)
w : { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } = { toArray := toArray✝, size_toArray := size_toArray✝ }
h : ∀ (a : α) (m_1 : a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }) (b : β), f a ⋯ b = g a m_1 b
⊢ forIn' { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } b f =
    forIn' { toArray := toArray✝, size_toArray := size_toArray✝ } b' g

Proof state:
case mk.mk
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝ : Monad m
b b' : β
hb : b = b'
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
f : (a' : α) → a' ∈ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } → β → m (ForInStep β)
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
g : (a' : α) → a' ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → β → m (ForInStep β)
w : { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } = { toArray := toArray✝, size_toArray := size_toArray✝ }
h : ∀ (a : α) (m_1 : a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }) (b : β), f a ⋯ b = g a m_1 b
⊢ forIn' { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } b f =
    forIn' { toArray := toArray✝, size_toArray := size_toArray✝ } b' g

Tactic:
simp only [eq_mk, mem_mk, forIn'_mk] at w h ⊢

Result:
case mk.mk
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝ : Monad m
b b' : β
hb : b = b'
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
f : (a' : α) → a' ∈ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } → β → m (ForInStep β)
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
g : (a' : α) → a' ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → β → m (ForInStep β)
w✝ : { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } = { toArray := toArray✝, size_toArray := size_toArray✝ }
w : toArray✝¹ = toArray✝
h : ∀ (a : α) (m_1 : a ∈ toArray✝) (b : β), f a ⋯ b = g a ⋯ b
⊢ (forIn' toArray✝¹ b fun a m b => f a ⋯ b) = forIn' toArray✝ b' fun a m b => g a ⋯ b

Proof state:
m✝ : Type ?u.28351 → Type ?u.28270
α : Type ?u.28275
n : Nat
β : Type ?u.28351
inst✝ : Monad m✝
as bs : Vector α n
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

Proof state:
case mk.mk
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝ : Monad m
b b' : β
hb : b = b'
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
f : (a' : α) → a' ∈ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } → β → m (ForInStep β)
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
g : (a' : α) → a' ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → β → m (ForInStep β)
w✝ : { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } = { toArray := toArray✝, size_toArray := size_toArray✝ }
w : toArray✝¹ = toArray✝
h : ∀ (a : α) (m_1 : a ∈ toArray✝) (b : β), f a ⋯ b = g a ⋯ b
⊢ (forIn' toArray✝¹ b fun a m b => f a ⋯ b) = forIn' toArray✝ b' fun a m b => g a ⋯ b

Tactic:
exact Array.forIn'_congr w hb h

Result:
no goals