awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : γ → ζ
f₂ : α → β → γ
nil : map f₁ (map₂ f₂ Vector.nil Vector.nil) = map₂ (fun (x : α) (y : β) ↦ f₁ (f₂ x y)) Vector.nil Vector.nil
snoc :
  ∀ {n : ℕ} (xs : Vector α n) (ys : Vector β n) (x : α) (y : β),
    map f₁ (map₂ f₂ xs ys) = map₂ (fun (x : α) (y : β) ↦ f₁ (f₂ x y)) xs ys →
      map f₁ (map₂ f₂ (xs.snoc x) (ys.snoc y)) = map₂ (fun (x : α) (y : β) ↦ f₁ (f₂ x y)) (xs.snoc x) (ys.snoc y)
⊢ map f₁ (map₂ f₂ xs ys) = map₂ (fun (x : α) (y : β) ↦ f₁ (f₂ x y)) xs ys

Tactic:
induction xs, ys using Vector.revInductionOn₂
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : γ → ζ
f₂ : α → β → γ
⊢ map f₁ (map₂ f₂ nil nil) = map₂ (fun (x : α) (y : β) ↦ f₁ (f₂ x y)) nil nil

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : γ → ζ
f₂ : α → β → γ
n_1 : ℕ
xs_1 : Vector α n_1
ys_1 : Vector β n_1
x : α
y : β
h : map f₁ (map₂ f₂ xs_1 ys_1) = map₂ (fun (x : α) (y : β) ↦ f₁ (f₂ x y)) xs_1 ys_1
⊢ map f₁ (map₂ f₂ (xs_1.snoc x) (ys_1.snoc y)) = map₂ (fun (x : α) (y : β) ↦ f₁ (f₂ x y)) (xs_1.snoc x) (ys_1.snoc y)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : γ → α → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
nil :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr₂ f₁ (mapAccumr₂ f₂ Vector.nil Vector.nil s₂).2 Vector.nil s₁ =
      let m : (σ₁ × σ₂) × Vector φ 0 :=
        mapAccumr₂
          (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
            match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
            | (s₁, s₂) =>
              let r₂ := f₂ x y s₂;
              let r₁ := f₁ r₂.2 x s₁;
              ((r₁.1, r₂.1), r₁.2))
          Vector.nil Vector.nil (s₁, s₂);
      (m.1.1, m.2)
snoc :
  ∀ {n : ℕ} (xs : Vector α n) (ys : Vector β n) (x : α) (y : β),
    (∀ {s₁ : σ₁} {s₂ : σ₂},
        mapAccumr₂ f₁ (mapAccumr₂ f₂ xs ys s₂).2 xs s₁ =
          let m : (σ₁ × σ₂) × Vector φ n :=
            mapAccumr₂
              (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
                match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
                | (s₁, s₂) =>
                  let r₂ := f₂ x y s₂;
                  let r₁ := f₁ r₂.2 x s₁;
                  ((r₁.1, r₂.1), r₁.2))
              xs ys (s₁, s₂);
          (m.1.1, m.2)) →
      ∀ {s₁ : σ₁} {s₂ : σ₂},
        mapAccumr₂ f₁ (mapAccumr₂ f₂ (xs.snoc x) (ys.snoc y) s₂).2 (xs.snoc x) s₁ =
          let m : (σ₁ × σ₂) × Vector φ (n + 1) :=
            mapAccumr₂
              (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
                match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
                | (s₁, s₂) =>
                  let r₂ := f₂ x y s₂;
                  let r₁ := f₁ r₂.2 x s₁;
                  ((r₁.1, r₂.1), r₁.2))
              (xs.snoc x) (ys.snoc y) (s₁, s₂);
          (m.1.1, m.2)
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ xs ys s₂).2 xs s₁ =
    let m : (σ₁ × σ₂) × Vector φ n :=
      mapAccumr₂
        (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
          match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ r₂.2 x s₁;
            ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
f₁ : γ → α → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ nil nil s₂).2 nil s₁ =
    let m : (σ₁ × σ₂) × Vector φ 0 :=
      mapAccumr₂
        (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
          match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ r₂.2 x s₁;
            ((r₁.1, r₂.1), r₁.2))
        nil nil (s₁, s₂);
    (m.1.1, m.2)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
f₁ : γ → α → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
n_1 : ℕ
xs : Vector α n_1
ys : Vector β n_1
x : α
y : β
h :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr₂ f₁ (mapAccumr₂ f₂ xs ys s₂).2 xs s₁ =
      let m : (σ₁ × σ₂) × Vector φ n_1 :=
        mapAccumr₂
          (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
            match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
            | (s₁, s₂) =>
              let r₂ := f₂ x y s₂;
              let r₁ := f₁ r₂.2 x s₁;
              ((r₁.1, r₂.1), r₁.2))
          xs ys (s₁, s₂);
      (m.1.1, m.2)
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ (xs.snoc x) (ys.snoc y) s₂).2 (xs.snoc x) s₁ =
    let m : (σ₁ × σ₂) × Vector φ (n_1 + 1) :=
      mapAccumr₂
        (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
          match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ r₂.2 x s₁;
            ((r₁.1, r₂.1), r₁.2))
        (xs.snoc x) (ys.snoc y) (s₁, s₂);
    (m.1.1, m.2)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : γ → β → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
nil :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr₂ f₁ (mapAccumr₂ f₂ Vector.nil Vector.nil s₂).2 Vector.nil s₁ =
      let m : (σ₁ × σ₂) × Vector φ 0 :=
        mapAccumr₂
          (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
            match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
            | (s₁, s₂) =>
              let r₂ := f₂ x y s₂;
              let r₁ := f₁ r₂.2 y s₁;
              ((r₁.1, r₂.1), r₁.2))
          Vector.nil Vector.nil (s₁, s₂);
      (m.1.1, m.2)
snoc :
  ∀ {n : ℕ} (xs : Vector α n) (ys : Vector β n) (x : α) (y : β),
    (∀ {s₁ : σ₁} {s₂ : σ₂},
        mapAccumr₂ f₁ (mapAccumr₂ f₂ xs ys s₂).2 ys s₁ =
          let m : (σ₁ × σ₂) × Vector φ n :=
            mapAccumr₂
              (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
                match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
                | (s₁, s₂) =>
                  let r₂ := f₂ x y s₂;
                  let r₁ := f₁ r₂.2 y s₁;
                  ((r₁.1, r₂.1), r₁.2))
              xs ys (s₁, s₂);
          (m.1.1, m.2)) →
      ∀ {s₁ : σ₁} {s₂ : σ₂},
        mapAccumr₂ f₁ (mapAccumr₂ f₂ (xs.snoc x) (ys.snoc y) s₂).2 (ys.snoc y) s₁ =
          let m : (σ₁ × σ₂) × Vector φ (n + 1) :=
            mapAccumr₂
              (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
                match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
                | (s₁, s₂) =>
                  let r₂ := f₂ x y s₂;
                  let r₁ := f₁ r₂.2 y s₁;
                  ((r₁.1, r₂.1), r₁.2))
              (xs.snoc x) (ys.snoc y) (s₁, s₂);
          (m.1.1, m.2)
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ xs ys s₂).2 ys s₁ =
    let m : (σ₁ × σ₂) × Vector φ n :=
      mapAccumr₂
        (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
          match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ r₂.2 y s₁;
            ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
f₁ : γ → β → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ nil nil s₂).2 nil s₁ =
    let m : (σ₁ × σ₂) × Vector φ 0 :=
      mapAccumr₂
        (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
          match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ r₂.2 y s₁;
            ((r₁.1, r₂.1), r₁.2))
        nil nil (s₁, s₂);
    (m.1.1, m.2)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
f₁ : γ → β → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
n_1 : ℕ
xs : Vector α n_1
ys : Vector β n_1
x : α
y : β
h :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr₂ f₁ (mapAccumr₂ f₂ xs ys s₂).2 ys s₁ =
      let m : (σ₁ × σ₂) × Vector φ n_1 :=
        mapAccumr₂
          (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
            match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
            | (s₁, s₂) =>
              let r₂ := f₂ x y s₂;
              let r₁ := f₁ r₂.2 y s₁;
              ((r₁.1, r₂.1), r₁.2))
          xs ys (s₁, s₂);
      (m.1.1, m.2)
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ (xs.snoc x) (ys.snoc y) s₂).2 (ys.snoc y) s₁ =
    let m : (σ₁ × σ₂) × Vector φ (n_1 + 1) :=
      mapAccumr₂
        (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
          match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ r₂.2 y s₁;
            ((r₁.1, r₂.1), r₁.2))
        (xs.snoc x) (ys.snoc y) (s₁, s₂);
    (m.1.1, m.2)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : α → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
nil :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr₂ f₁ Vector.nil (mapAccumr₂ f₂ Vector.nil Vector.nil s₂).2 s₁ =
      let m : (σ₁ × σ₂) × Vector φ 0 :=
        mapAccumr₂
          (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
            match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
            | (s₁, s₂) =>
              let r₂ := f₂ x y s₂;
              let r₁ := f₁ x r₂.2 s₁;
              ((r₁.1, r₂.1), r₁.2))
          Vector.nil Vector.nil (s₁, s₂);
      (m.1.1, m.2)
snoc :
  ∀ {n : ℕ} (xs : Vector α n) (ys : Vector β n) (x : α) (y : β),
    (∀ {s₁ : σ₁} {s₂ : σ₂},
        mapAccumr₂ f₁ xs (mapAccumr₂ f₂ xs ys s₂).2 s₁ =
          let m : (σ₁ × σ₂) × Vector φ n :=
            mapAccumr₂
              (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
                match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
                | (s₁, s₂) =>
                  let r₂ := f₂ x y s₂;
                  let r₁ := f₁ x r₂.2 s₁;
                  ((r₁.1, r₂.1), r₁.2))
              xs ys (s₁, s₂);
          (m.1.1, m.2)) →
      ∀ {s₁ : σ₁} {s₂ : σ₂},
        mapAccumr₂ f₁ (xs.snoc x) (mapAccumr₂ f₂ (xs.snoc x) (ys.snoc y) s₂).2 s₁ =
          let m : (σ₁ × σ₂) × Vector φ (n + 1) :=
            mapAccumr₂
              (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
                match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
                | (s₁, s₂) =>
                  let r₂ := f₂ x y s₂;
                  let r₁ := f₁ x r₂.2 s₁;
                  ((r₁.1, r₂.1), r₁.2))
              (xs.snoc x) (ys.snoc y) (s₁, s₂);
          (m.1.1, m.2)
⊢ mapAccumr₂ f₁ xs (mapAccumr₂ f₂ xs ys s₂).2 s₁ =
    let m : (σ₁ × σ₂) × Vector φ n :=
      mapAccumr₂
        (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
          match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ x r₂.2 s₁;
            ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
f₁ : α → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr₂ f₁ nil (mapAccumr₂ f₂ nil nil s₂).2 s₁ =
    let m : (σ₁ × σ₂) × Vector φ 0 :=
      mapAccumr₂
        (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
          match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ x r₂.2 s₁;
            ((r₁.1, r₂.1), r₁.2))
        nil nil (s₁, s₂);
    (m.1.1, m.2)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
f₁ : α → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
n_1 : ℕ
xs : Vector α n_1
ys : Vector β n_1
x : α
y : β
h :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr₂ f₁ xs (mapAccumr₂ f₂ xs ys s₂).2 s₁ =
      let m : (σ₁ × σ₂) × Vector φ n_1 :=
        mapAccumr₂
          (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
            match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
            | (s₁, s₂) =>
              let r₂ := f₂ x y s₂;
              let r₁ := f₁ x r₂.2 s₁;
              ((r₁.1, r₂.1), r₁.2))
          xs ys (s₁, s₂);
      (m.1.1, m.2)
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr₂ f₁ (xs.snoc x) (mapAccumr₂ f₂ (xs.snoc x) (ys.snoc y) s₂).2 s₁ =
    let m : (σ₁ × σ₂) × Vector φ (n_1 + 1) :=
      mapAccumr₂
        (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
          match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ x r₂.2 s₁;
            ((r₁.1, r₂.1), r₁.2))
        (xs.snoc x) (ys.snoc y) (s₁, s₂);
    (m.1.1, m.2)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : β → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
nil :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr₂ f₁ Vector.nil (mapAccumr₂ f₂ Vector.nil Vector.nil s₂).2 s₁ =
      let m : (σ₁ × σ₂) × Vector φ 0 :=
        mapAccumr₂
          (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
            match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
            | (s₁, s₂) =>
              let r₂ := f₂ x y s₂;
              let r₁ := f₁ y r₂.2 s₁;
              ((r₁.1, r₂.1), r₁.2))
          Vector.nil Vector.nil (s₁, s₂);
      (m.1.1, m.2)
snoc :
  ∀ {n : ℕ} (xs : Vector α n) (ys : Vector β n) (x : α) (y : β),
    (∀ {s₁ : σ₁} {s₂ : σ₂},
        mapAccumr₂ f₁ ys (mapAccumr₂ f₂ xs ys s₂).2 s₁ =
          let m : (σ₁ × σ₂) × Vector φ n :=
            mapAccumr₂
              (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
                match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
                | (s₁, s₂) =>
                  let r₂ := f₂ x y s₂;
                  let r₁ := f₁ y r₂.2 s₁;
                  ((r₁.1, r₂.1), r₁.2))
              xs ys (s₁, s₂);
          (m.1.1, m.2)) →
      ∀ {s₁ : σ₁} {s₂ : σ₂},
        mapAccumr₂ f₁ (ys.snoc y) (mapAccumr₂ f₂ (xs.snoc x) (ys.snoc y) s₂).2 s₁ =
          let m : (σ₁ × σ₂) × Vector φ (n + 1) :=
            mapAccumr₂
              (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
                match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
                | (s₁, s₂) =>
                  let r₂ := f₂ x y s₂;
                  let r₁ := f₁ y r₂.2 s₁;
                  ((r₁.1, r₂.1), r₁.2))
              (xs.snoc x) (ys.snoc y) (s₁, s₂);
          (m.1.1, m.2)
⊢ mapAccumr₂ f₁ ys (mapAccumr₂ f₂ xs ys s₂).2 s₁ =
    let m : (σ₁ × σ₂) × Vector φ n :=
      mapAccumr₂
        (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
          match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ y r₂.2 s₁;
            ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
f₁ : β → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr₂ f₁ nil (mapAccumr₂ f₂ nil nil s₂).2 s₁ =
    let m : (σ₁ × σ₂) × Vector φ 0 :=
      mapAccumr₂
        (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
          match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ y r₂.2 s₁;
            ((r₁.1, r₂.1), r₁.2))
        nil nil (s₁, s₂);
    (m.1.1, m.2)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
f₁ : β → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
n_1 : ℕ
xs : Vector α n_1
ys : Vector β n_1
x : α
y : β
h :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr₂ f₁ ys (mapAccumr₂ f₂ xs ys s₂).2 s₁ =
      let m : (σ₁ × σ₂) × Vector φ n_1 :=
        mapAccumr₂
          (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
            match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
            | (s₁, s₂) =>
              let r₂ := f₂ x y s₂;
              let r₁ := f₁ y r₂.2 s₁;
              ((r₁.1, r₂.1), r₁.2))
          xs ys (s₁, s₂);
      (m.1.1, m.2)
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr₂ f₁ (ys.snoc y) (mapAccumr₂ f₂ (xs.snoc x) (ys.snoc y) s₂).2 s₁ =
    let m : (σ₁ × σ₂) × Vector φ (n_1 + 1) :=
      mapAccumr₂
        (fun (x : α) (y : β) (x_1 : σ₁ × σ₂) ↦
          match (motive := σ₁ × σ₂ → (σ₁ × σ₂) × φ) x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ y r₂.2 s₁;
            ((r₁.1, r₂.1), r₁.2))
        (xs.snoc x) (ys.snoc y) (s₁, s₂);
    (m.1.1, m.2)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : 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
induction :
  ∀ {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
snoc :
  ∀ {n : ℕ} (xs : Vector α n) (x : α),
    (∀ {s₁ : σ₁} {s₂ : σ₂} (h₀ : 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
⊢ 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₂
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : 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:
⟨h₀, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : 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⟩
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : 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:
next => exact ⟨h₀, rfl⟩
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs_1 : 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_1 : ℕ
xs : Vector α n_1
x : α
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂} (h₀ : 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 (f₁ x s₁).1 (f₂ x s₂).1

Tactic:
rcases (hR x h₀) with ⟨hR, _⟩
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs_1 : 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_1 : ℕ
xs : Vector α n_1
x : α
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂} (h₀ : 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
⊢ (f₁ x s₁).2 = (f₂ x s₂).2

Tactic:
rcases (hR x h₀) with ⟨hR, _⟩
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs_1 : Vector α n
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR_1 : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2
n_1 : ℕ
xs : Vector α n_1
x : α
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂} (h₀ : 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
simp : (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
⊢ 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]

Premises used: List.Vector.mapAccumr_snoc, true_and
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs_1 : Vector α n
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR_1 : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2
n_1 : ℕ
xs : Vector α n_1
x : α
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂} (h₀ : 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
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
s₁ : σ₁
s₂ : σ₂
h :
  ∃ (R : σ₁ → σ₂ → Prop),
    R s₁ s₂ ∧ ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2
rcases :
  ∀ (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),
    (mapAccumr f₁ xs s₁).2 = (mapAccumr f₂ xs s₂).2
⊢ (mapAccumr f₁ xs s₁).2 = (mapAccumr f₂ xs s₂).2

Tactic:
rcases h with ⟨R, h₀, hR⟩
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : 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
⊢ (mapAccumr f₁ xs s₁).2 = (mapAccumr f₂ xs s₂).2

Tactic:
(mapAccumr_bisim R h₀ hR).2

Premises used: And.right, List.Vector.mapAccumr_bisim
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : 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
⊢ (mapAccumr f₁ xs s₁).2 = (mapAccumr f₂ xs s₂).2

Tactic:
exact (mapAccumr_bisim R h₀ hR).2

Premises used: And.right, List.Vector.mapAccumr_bisim