-- Mathlib/Data/Vector/MapLemmas.lean
theorem mapAccumr_bisim {f₁ : α → σ₁ → σ₁ × β} {f₂ : α → σ₂ → σ₂ × β} {s₁ : σ₁} {s₂ : σ₂}
    (R : σ₁ → σ₂ → Prop) (h₀ : R s₁ s₂)
    (hR : ∀ {s q} a, R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2) :
    R (mapAccumr f₁ xs s₁).fst (mapAccumr f₂ xs s₂).fst
    ∧ (mapAccumr f₁ xs s₁).snd = (mapAccumr f₂ xs s₂).snd

Proof state:
case snoc
α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ → R (mapAccumr f₁ xs✝ s₁).1 (mapAccumr f₂ xs✝ s₂).1 ∧ (mapAccumr f₁ xs✝ s₁).2 = (mapAccumr f₂ xs✝ s₂).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr f₁ (xs✝.snoc x✝) s₁).1 (mapAccumr f₂ (xs✝.snoc x✝) s₂).1 ∧
    (mapAccumr f₁ (xs✝.snoc x✝) s₁).2 = (mapAccumr f₂ (xs✝.snoc x✝) s₂).2

Tactic:
next xs x ih =>
  rcases (hR x h₀) with ⟨hR, _⟩
  simp only [mapAccumr_snoc, ih hR, true_and]
  congr 1

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
s₁ : σ₁
s₂ : σ₂
R : σ₁ → σ₂ → Prop
h₀ : R s₁ s₂
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2
⊢ R (mapAccumr f₁ xs s₁).1 (mapAccumr f₂ xs s₂).1 ∧ (mapAccumr f₁ xs s₁).2 = (mapAccumr f₂ xs s₂).2

Tactic:
induction xs using Vector.revInductionOn generalizing s₁ s₂

Result:
case nil
α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr f₁ nil s₁).1 (mapAccumr f₂ nil s₂).1 ∧ (mapAccumr f₁ nil s₁).2 = (mapAccumr f₂ nil s₂).2

case snoc
α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ → R (mapAccumr f₁ xs✝ s₁).1 (mapAccumr f₂ xs✝ s₂).1 ∧ (mapAccumr f₁ xs✝ s₁).2 = (mapAccumr f₂ xs✝ s₂).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr f₁ (xs✝.snoc x✝) s₁).1 (mapAccumr f₂ (xs✝.snoc x✝) s₂).1 ∧
    (mapAccumr f₁ (xs✝.snoc x✝) s₁).2 = (mapAccumr f₂ (xs✝.snoc x✝) s₂).2

Proof state:
α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr f₁ nil s₁).1 (mapAccumr f₂ nil s₂).1 ∧ (mapAccumr f₁ nil s₁).2 = (mapAccumr f₂ nil s₂).2

Tactic:
exact ⟨h₀, rfl⟩

Result:
no goals

Proof state:
case intro
α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs✝ : Vector α n
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR✝ : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2
n✝ : ℕ
xs : Vector α n✝
x : α
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ → R (mapAccumr f₁ xs s₁).1 (mapAccumr f₂ xs s₂).1 ∧ (mapAccumr f₁ xs s₁).2 = (mapAccumr f₂ xs s₂).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
hR : R (f₁ x s₁).1 (f₂ x s₂).1
right✝ : (f₁ x s₁).2 = (f₂ x s₂).2
⊢ R (mapAccumr f₁ (xs.snoc x) s₁).1 (mapAccumr f₂ (xs.snoc x) s₂).1 ∧
    (mapAccumr f₁ (xs.snoc x) s₁).2 = (mapAccumr f₂ (xs.snoc x) s₂).2

Tactic:
simp only [mapAccumr_snoc, ih hR, true_and]

Result:
case intro
α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs✝ : Vector α n
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR✝ : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2
n✝ : ℕ
xs : Vector α n✝
x : α
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ → R (mapAccumr f₁ xs s₁).1 (mapAccumr f₂ xs s₂).1 ∧ (mapAccumr f₁ xs s₁).2 = (mapAccumr f₂ xs s₂).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
hR : R (f₁ x s₁).1 (f₂ x s₂).1
right✝ : (f₁ x s₁).2 = (f₂ x s₂).2
⊢ (mapAccumr f₂ xs (f₂ x s₂).1).2.snoc (f₁ x s₁).2 = (mapAccumr f₂ xs (f₂ x s₂).1).2.snoc (f₂ x s₂).2

Proof state:
α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs✝ : Vector α n
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2
n✝ : ℕ
xs : Vector α n✝
x : α
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ → R (mapAccumr f₁ xs s₁).1 (mapAccumr f₂ xs s₂).1 ∧ (mapAccumr f₁ xs s₁).2 = (mapAccumr f₂ xs s₂).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr f₁ (xs.snoc x) s₁).1 (mapAccumr f₂ (xs.snoc x) s₂).1 ∧
    (mapAccumr f₁ (xs.snoc x) s₁).2 = (mapAccumr f₂ (xs.snoc x) s₂).2

Tactic:
rcases (hR x h₀) with ⟨hR, _⟩

Result:
case intro
α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs✝ : Vector α n
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR✝ : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2
n✝ : ℕ
xs : Vector α n✝
x : α
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ → R (mapAccumr f₁ xs s₁).1 (mapAccumr f₂ xs s₂).1 ∧ (mapAccumr f₁ xs s₁).2 = (mapAccumr f₂ xs s₂).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
hR : R (f₁ x s₁).1 (f₂ x s₂).1
right✝ : (f₁ x s₁).2 = (f₂ x s₂).2
⊢ R (mapAccumr f₁ (xs.snoc x) s₁).1 (mapAccumr f₂ (xs.snoc x) s₂).1 ∧
    (mapAccumr f₁ (xs.snoc x) s₁).2 = (mapAccumr f₂ (xs.snoc x) s₂).2

Proof state:
case intro
α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs✝ : Vector α n
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR✝ : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2
n✝ : ℕ
xs : Vector α n✝
x : α
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ → R (mapAccumr f₁ xs s₁).1 (mapAccumr f₂ xs s₂).1 ∧ (mapAccumr f₁ xs s₁).2 = (mapAccumr f₂ xs s₂).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
hR : R (f₁ x s₁).1 (f₂ x s₂).1
right✝ : (f₁ x s₁).2 = (f₂ x s₂).2
⊢ (mapAccumr f₂ xs (f₂ x s₂).1).2.snoc (f₁ x s₁).2 = (mapAccumr f₂ xs (f₂ x s₂).1).2.snoc (f₂ x s₂).2

Tactic:
congr 1

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr f₁ nil s₁).1 (mapAccumr f₂ nil s₂).1 ∧ (mapAccumr f₁ nil s₁).2 = (mapAccumr f₂ nil s₂).2

case snoc
α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ → R (mapAccumr f₁ xs✝ s₁).1 (mapAccumr f₂ xs✝ s₂).1 ∧ (mapAccumr f₁ xs✝ s₁).2 = (mapAccumr f₂ xs✝ s₂).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr f₁ (xs✝.snoc x✝) s₁).1 (mapAccumr f₂ (xs✝.snoc x✝) s₂).1 ∧
    (mapAccumr f₁ (xs✝.snoc x✝) s₁).2 = (mapAccumr f₂ (xs✝.snoc x✝) s₂).2

Tactic:
next => exact ⟨h₀, rfl⟩

Result:
case snoc
α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ → R (mapAccumr f₁ xs✝ s₁).1 (mapAccumr f₂ xs✝ s₂).1 ∧ (mapAccumr f₁ xs✝ s₁).2 = (mapAccumr f₂ xs✝ s₂).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr f₁ (xs✝.snoc x✝) s₁).1 (mapAccumr f₂ (xs✝.snoc x✝) s₂).1 ∧
    (mapAccumr f₁ (xs✝.snoc x✝) s₁).2 = (mapAccumr f₂ (xs✝.snoc x✝) s₂).2