awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
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₂ : α → β → σ₂ → σ₂ × γ
⊢ 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)
have nil : ∀ {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: induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
Cleared hypotheses: s₁, s₂, xs, ys
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
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)
⊢ 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)
have 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)
Tactic: induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
Cleared hypotheses: s₁, s₂, xs, ys
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
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₂ : α → β → σ₂ → σ₂ × γ
⊢ 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)
have nil : ∀ {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: induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
Cleared hypotheses: s₁, s₂, xs, ys
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
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)
⊢ 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)
have 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)
Tactic: induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
Cleared hypotheses: s₁, s₂, xs, ys
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
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₂ : α → β → σ₂ → σ₂ × γ
⊢ 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)
have nil : ∀ {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: induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
Cleared hypotheses: s₁, s₂, xs, ys
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
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)
⊢ 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)
have 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)
Tactic: induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
Cleared hypotheses: s₁, s₂, xs, ys
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
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
⊢ R (mapAccumr f₁ xs s₁).1 (mapAccumr f₂ xs s₂).1 ∧ (mapAccumr f₁ xs s₁).2 = (mapAccumr f₂ xs s₂).2
have 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
Tactic: induction xs using Vector.revInductionOn generalizing s₁ s₂
Cleared hypotheses: s₁, s₂, h₀
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
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
⊢ R (mapAccumr f₁ xs s₁).1 (mapAccumr f₂ xs s₂).1 ∧ (mapAccumr f₁ xs s₁).2 = (mapAccumr f₂ xs s₂).2
have 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
Tactic: induction xs using Vector.revInductionOn generalizing s₁ s₂
Cleared hypotheses: s₁, s₂, h₀
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (hypothesis)
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 (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
have hR₁ : R (f₁ x s₁).1 (f₂ x s₂).1
Tactic: rcases (hR x h₀) with ⟨hR, _⟩
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (hypothesis)
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
⊢ 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
have right : (f₁ x s₁).2 = (f₂ x s₂).2
Tactic: rcases (hR x h₀) with ⟨hR, _⟩
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
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
⊢ 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
have 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
Tactic: simp only [mapAccumr_snoc, ih hR, true_and]
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
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
⊢ (mapAccumr f₁ xs s₁).2 = (mapAccumr f₂ xs s₂).2
have 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
Tactic: rcases h with ⟨R, h₀, hR⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : 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
have induction : ∀ {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: induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
Cleared hypotheses: ys, s₁, s₂, h₀
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : 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
induction :
  ∀ {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
⊢ 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
have snoc : ∀ {n : ℕ} (xs : Vector α n) (ys : Vector β n) (x : α) (y : β),
  (∀ {s₁ : σ₁} {s₂ : σ₂} (h₀ : 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: induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
Cleared hypotheses: ys, s₁, s₂, h₀
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs_1 : 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_1 : ℕ
xs : Vector α n_1
ys : Vector β n_1
x : α
y : β
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂} (h₀ : 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
have hR₁ : R (f₁ x y s₁).1 (f₂ x y s₂).1
Tactic: rcases (hR x y h₀) with ⟨hR, _⟩
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs_1 : 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_1 : ℕ
xs : Vector α n_1
ys : Vector β n_1
x : α
y : β
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂} (h₀ : 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
⊢ 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
have right : (f₁ x y s₁).2 = (f₂ x y s₂).2
Tactic: rcases (hR x y h₀) with ⟨hR, _⟩
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs_1 : Vector α n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR_1 : ∀ {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_1 : ℕ
xs : Vector α n_1
ys : Vector β n_1
x : α
y : β
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂} (h₀ : 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
have simp : (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: simp only [mapAccumr₂_snoc, ih hR, true_and]
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : 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₂ : σ₂
h :
  ∃ (R : σ₁ → σ₂ → Prop),
    R s₁ s₂ ∧ ∀ {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
⊢ (mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2
have rcases : ∀ (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),
  (mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2
Tactic: rcases h with ⟨R, h₀, hR⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
n : ℕ
xs : Vector α n
f : α → β
⊢ map f xs = (mapAccumr (fun (x : α) (x_1 : Unit) ↦ ((), f x)) xs ()).2
have nil : map f nil = (mapAccumr (fun (x : α) (x_1 : Unit) ↦ ((), f x)) nil ()).2
Tactic: induction xs using Vector.revInductionOn
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
n : ℕ
xs : Vector α n
f : α → β
nil : map f Vector.nil = (mapAccumr (fun (x : α) (x_1 : Unit) ↦ ((), f x)) Vector.nil ()).2
⊢ map f xs = (mapAccumr (fun (x : α) (x_1 : Unit) ↦ ((), f x)) xs ()).2
have snoc : ∀ {n : ℕ} (xs : Vector α n) (x : α),
  map f xs = (mapAccumr (fun (x : α) (x_1 : Unit) ↦ ((), f x)) xs ()).2 →
    map f (xs.snoc x) = (mapAccumr (fun (x : α) (x_1 : Unit) ↦ ((), f x)) (xs.snoc x) ()).2
Tactic: induction xs using Vector.revInductionOn
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (s : σ), s ∈ S → (f a s).1 ∈ S
out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).2 = (f a s').2
⊢ (mapAccumr f xs s₀).2 = map (fun (x : α) ↦ (f x s₀).2) xs
have rw : (mapAccumr f xs s₀).2 = (mapAccumr (fun (x : α) (x_1 : Unit) ↦ ((), (f x s₀).2)) xs ()).2
Tactic: rw [Vector.map_eq_mapAccumr]
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (s : σ), s ∈ S → (f a s).1 ∈ S
out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).2 = (f a s').2
⊢ (mapAccumr f xs s₀).2 = (mapAccumr (fun (x : α) (x_1 : Unit) ↦ ((), (f x s₀).2)) xs ()).2
have h : ∃ (R : σ → Unit → Prop),
  R s₀ () ∧ ∀ {s : σ} {q : Unit} (a : α), R s q → R (f a s).1 ((), (f a s₀).2).1 ∧ (f a s).2 = ((), (f a s₀).2).2
Tactic: apply mapAccumr_bisim_tail
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (s : σ), s ∈ S → (f a s).1 ∈ S
out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).2 = (f a s').2
⊢ ∃ (R : σ → Unit → Prop),
    R s₀ () ∧ ∀ {s : σ} {q : Unit} (a : α), R s q → R (f a s).1 ((), (f a s₀).2).1 ∧ (f a s).2 = ((), (f a s₀).2).2
have right : ∀ {s : σ} {q : Unit} (a : α), s ∈ S → (f a s).1 ∈ S ∧ (f a s).2 = ((), (f a s₀).2).2
Tactic: use fun s _ => s ∈ S, h₀
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → γ
⊢ map₂ f xs ys = (mapAccumr₂ (fun (x : α) (y : β) (x_1 : Unit) ↦ ((), f x y)) xs ys ()).2
have nil : map₂ f nil nil = (mapAccumr₂ (fun (x : α) (y : β) (x_1 : Unit) ↦ ((), f x y)) nil nil ()).2
Tactic: induction xs, ys using Vector.revInductionOn₂
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → γ
nil :
  map₂ f Vector.nil Vector.nil =
    (mapAccumr₂ (fun (x : α) (y : β) (x_1 : Unit) ↦ ((), f x y)) Vector.nil Vector.nil ()).2
⊢ map₂ f xs ys = (mapAccumr₂ (fun (x : α) (y : β) (x_1 : Unit) ↦ ((), f x y)) xs ys ()).2
have snoc : ∀ {n : ℕ} (xs : Vector α n) (ys : Vector β n) (x : α) (y : β),
  map₂ f xs ys = (mapAccumr₂ (fun (x : α) (y : β) (x_1 : Unit) ↦ ((), f x y)) xs ys ()).2 →
    map₂ f (xs.snoc x) (ys.snoc y) =
      (mapAccumr₂ (fun (x : α) (y : β) (x_1 : Unit) ↦ ((), f x y)) (xs.snoc x) (ys.snoc y) ()).2
Tactic: induction xs, ys using Vector.revInductionOn₂