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

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

Tactic:
congr 1

Result:
no goals

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

Tactic:
exact ⟨h₀, rfl⟩

Result:
no goals

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

Tactic:
simp only [mapAccumr₂_snoc, ih hR, true_and]

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

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

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

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

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

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

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

Result:
no goals

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

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

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

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