-- Mathlib/Data/Vector/MapLemmas.lean
theorem mapAccumr₂_eq_map₂ {f : α → β → σ → σ × γ} {s₀ : σ} (S : Set σ) (h₀ : s₀ ∈ S)
    (closure : ∀ a b s, s ∈ S → (f a b s).1 ∈ S)
    (out : ∀ a b s s', s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2) :
    (mapAccumr₂ f xs ys s₀).snd = map₂ (f · · s₀ |>.snd) xs ys

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (b : β), ∀ s ∈ S, (f a b s).1 ∈ S
out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2
⊢ (mapAccumr₂ f xs ys s₀).2 = (mapAccumr₂ (fun x y x_1 => ((), (f x y s₀).2)) xs ys ()).2

Tactic:
apply mapAccumr₂_bisim_tail

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (b : β), ∀ s ∈ S, (f a b s).1 ∈ S
out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2
⊢ ∃ R,
    R s₀ () ∧
      ∀ {s : σ} {q : Unit} (a : α) (b : β),
        R s q → R (f a b s).1 ((), (f a b s₀).2).1 ∧ (f a b s).2 = ((), (f a b s₀).2).2

Proof state:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (b : β), ∀ s ∈ S, (f a b s).1 ∈ S
out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2
⊢ ∀ {s : σ} {q : Unit} (a : α) (b : β), s ∈ S → (f a b s).1 ∈ S ∧ (f a b s).2 = ((), (f a b s₀).2).2

Tactic:
exact @fun s _q a b h => ⟨closure a b s h, out a b s s₀ h h₀⟩

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (b : β), ∀ s ∈ S, (f a b s).1 ∈ S
out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2
⊢ ∃ R,
    R s₀ () ∧
      ∀ {s : σ} {q : Unit} (a : α) (b : β),
        R s q → R (f a b s).1 ((), (f a b s₀).2).1 ∧ (f a b s).2 = ((), (f a b s₀).2).2

Tactic:
use fun s _ => s ∈ S, h₀

Result:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (b : β), ∀ s ∈ S, (f a b s).1 ∈ S
out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2
⊢ ∀ {s : σ} {q : Unit} (a : α) (b : β), s ∈ S → (f a b s).1 ∈ S ∧ (f a b s).2 = ((), (f a b s₀).2).2

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (b : β), ∀ s ∈ S, (f a b s).1 ∈ S
out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2
⊢ (mapAccumr₂ f xs ys s₀).2 = map₂ (fun x1 x2 => (f x1 x2 s₀).2) xs ys

Tactic:
rw [Vector.map₂_eq_mapAccumr₂]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (b : β), ∀ s ∈ S, (f a b s).1 ∈ S
out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2
⊢ (mapAccumr₂ f xs ys s₀).2 = (mapAccumr₂ (fun x y x_1 => ((), (f x y s₀).2)) xs ys ()).2