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
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
f₁ : β → σ₁ → σ₁ × γ
f₂ : α → σ₂ → σ₂ × β
nil :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr f₁ (mapAccumr f₂ Vector.nil s₂).2 s₁ =
      let m : (σ₁ × σ₂) × Vector γ 0 :=
        mapAccumr
          (fun (x : α) (s : σ₁ × σ₂) ↦
            let r₂ := f₂ x s.2;
            let r₁ := f₁ r₂.2 s.1;
            ((r₁.1, r₂.1), r₁.2))
          Vector.nil (s₁, s₂);
      (m.1.1, m.2)
⊢ mapAccumr f₁ (mapAccumr f₂ xs s₂).2 s₁ =
    let m : (σ₁ × σ₂) × Vector γ n :=
      mapAccumr
        (fun (x : α) (s : σ₁ × σ₂) ↦
          let r₂ := f₂ x s.2;
          let r₁ := f₁ r₂.2 s.1;
          ((r₁.1, r₂.1), r₁.2))
        xs (s₁, s₂);
    (m.1.1, m.2)
have snoc : ∀ {n : ℕ} (xs : Vector α n) (x : α),
  (∀ {s₁ : σ₁} {s₂ : σ₂},
      mapAccumr f₁ (mapAccumr f₂ xs s₂).2 s₁ =
        let m : (σ₁ × σ₂) × Vector γ n :=
          mapAccumr
            (fun (x : α) (s : σ₁ × σ₂) ↦
              let r₂ := f₂ x s.2;
              let r₁ := f₁ r₂.2 s.1;
              ((r₁.1, r₂.1), r₁.2))
            xs (s₁, s₂);
        (m.1.1, m.2)) →
    ∀ {s₁ : σ₁} {s₂ : σ₂},
      mapAccumr f₁ (mapAccumr f₂ (xs.snoc x) s₂).2 s₁ =
        let m : (σ₁ × σ₂) × Vector γ (n + 1) :=
          mapAccumr
            (fun (x : α) (s : σ₁ × σ₂) ↦
              let r₂ := f₂ x s.2;
              let r₁ := f₁ r₂.2 s.1;
              ((r₁.1, r₂.1), r₁.2))
            (xs.snoc x) (s₁, s₂);
        (m.1.1, m.2)
Tactic: induction xs using Vector.revInductionOn generalizing s₁ s₂
Cleared hypotheses: s₁, s₂, xs
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
n : ℕ
xs : Vector α n
f₁ : β → σ₁ → σ₁ × γ
s : σ₁
f₂ : α → β
⊢ mapAccumr f₁ (map f₂ xs) s = mapAccumr (fun (x : α) (s : σ₁) ↦ f₁ (f₂ x) s) xs s
have nil : ∀ {s : σ₁}, mapAccumr f₁ (map f₂ nil) s = mapAccumr (fun (x : α) (s : σ₁) ↦ f₁ (f₂ x) s) nil s
Tactic: induction xs using Vector.revInductionOn generalizing s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
n : ℕ
xs : Vector α n
f₁ : β → σ₁ → σ₁ × γ
s : σ₁
f₂ : α → β
nil : ∀ {s : σ₁}, mapAccumr f₁ (map f₂ Vector.nil) s = mapAccumr (fun (x : α) (s : σ₁) ↦ f₁ (f₂ x) s) Vector.nil s
⊢ mapAccumr f₁ (map f₂ xs) s = mapAccumr (fun (x : α) (s : σ₁) ↦ f₁ (f₂ x) s) xs s
have snoc : ∀ {n : ℕ} (xs : Vector α n) (x : α),
  (∀ {s : σ₁}, mapAccumr f₁ (map f₂ xs) s = mapAccumr (fun (x : α) (s : σ₁) ↦ f₁ (f₂ x) s) xs s) →
    ∀ {s : σ₁}, mapAccumr f₁ (map f₂ (xs.snoc x)) s = mapAccumr (fun (x : α) (s : σ₁) ↦ f₁ (f₂ x) s) (xs.snoc x) s
Tactic: induction xs using Vector.revInductionOn generalizing s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₂ : α → σ₂ → σ₂ × β
s : σ₂
f₁ : β → γ
⊢ map f₁ (mapAccumr f₂ xs s).2 =
    (mapAccumr
        (fun (x : α) (s : σ₂) ↦
          let r := f₂ x s;
          (r.1, f₁ r.2))
        xs s).2
have nil : ∀ {s : σ₂},
  map f₁ (mapAccumr f₂ nil s).2 =
    (mapAccumr
        (fun (x : α) (s : σ₂) ↦
          let r := f₂ x s;
          (r.1, f₁ r.2))
        nil s).2
Tactic: induction xs using Vector.revInductionOn generalizing s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₂ : α → σ₂ → σ₂ × β
s : σ₂
f₁ : β → γ
nil :
  ∀ {s : σ₂},
    map f₁ (mapAccumr f₂ Vector.nil s).2 =
      (mapAccumr
          (fun (x : α) (s : σ₂) ↦
            let r := f₂ x s;
            (r.1, f₁ r.2))
          Vector.nil s).2
⊢ map f₁ (mapAccumr f₂ xs s).2 =
    (mapAccumr
        (fun (x : α) (s : σ₂) ↦
          let r := f₂ x s;
          (r.1, f₁ r.2))
        xs s).2
have snoc : ∀ {n : ℕ} (xs : Vector α n) (x : α),
  (∀ {s : σ₂},
      map f₁ (mapAccumr f₂ xs s).2 =
        (mapAccumr
            (fun (x : α) (s : σ₂) ↦
              let r := f₂ x s;
              (r.1, f₁ r.2))
            xs s).2) →
    ∀ {s : σ₂},
      map f₁ (mapAccumr f₂ (xs.snoc x) s).2 =
        (mapAccumr
            (fun (x : α) (s : σ₂) ↦
              let r := f₂ x s;
              (r.1, f₁ r.2))
            (xs.snoc x) s).2
Tactic: induction xs using Vector.revInductionOn generalizing s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
f₁ : β → γ
f₂ : α → β
⊢ map f₁ (map f₂ xs) = map (fun (x : α) ↦ f₁ (f₂ x)) xs
have nil : map f₁ (map f₂ nil) = map (fun (x : α) ↦ f₁ (f₂ x)) nil
Tactic: induction xs
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
f₁ : β → γ
f₂ : α → β
nil : map f₁ (map f₂ Vector.nil) = map (fun (x : α) ↦ f₁ (f₂ x)) Vector.nil
⊢ map f₁ (map f₂ xs) = map (fun (x : α) ↦ f₁ (f₂ x)) xs
have cons : ∀ {n : ℕ} {x : α} {w : Vector α n},
  map f₁ (map f₂ w) = map (fun (x : α) ↦ f₁ (f₂ x)) w →
    map f₁ (map f₂ (x ::ᵥ w)) = map (fun (x : α) ↦ f₁ (f₂ x)) (x ::ᵥ w)
Tactic: induction xs
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
p : α → Prop
f₁ : β → γ
f₂ : (a : α) → p a → β
H : ∀ (x : α), x ∈ xs.toList → p x
⊢ map f₁ (pmap (p := p) f₂ xs H) = pmap (p := p) (fun (x : α) (hx : p x) ↦ f₁ (f₂ x hx)) xs H
have nil : ∀ (H : ∀ (x : α), Membership.mem (γ := List α) (toList nil) x → p x),
  map f₁ (pmap (p := p) f₂ nil H) = pmap (p := p) (fun (x : α) (hx : p x) ↦ f₁ (f₂ x hx)) nil H
Tactic: induction xs
Cleared hypotheses: 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
p : α → Prop
f₁ : β → γ
f₂ : (a : α) → p a → β
H : ∀ (x : α), x ∈ xs.toList → p x
nil :
  ∀ (H : ∀ (x : α), Membership.mem (γ := List α) (toList Vector.nil) x → p x),
    map f₁ (pmap (p := p) f₂ Vector.nil H) = pmap (p := p) (fun (x : α) (hx : p x) ↦ f₁ (f₂ x hx)) Vector.nil H
⊢ map f₁ (pmap (p := p) f₂ xs H) = pmap (p := p) (fun (x : α) (hx : p x) ↦ f₁ (f₂ x hx)) xs H
have cons : ∀ {n : ℕ} {x : α} {w : Vector α n},
  (∀ (H : ∀ (x : α), x ∈ w.toList → p x),
      map f₁ (pmap (p := p) f₂ w H) = pmap (p := p) (fun (x : α) (hx : p x) ↦ f₁ (f₂ x hx)) w H) →
    ∀ (H : ∀ (x_1 : α), x_1 ∈ (x ::ᵥ w).toList → p x_1),
      map f₁ (pmap (p := p) f₂ (x ::ᵥ w) H) = pmap (p := p) (fun (x : α) (hx : p x) ↦ f₁ (f₂ x hx)) (x ::ᵥ w) H
Tactic: induction xs
Cleared hypotheses: 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
p : β → Prop
f₁ : (b : β) → p b → γ
f₂ : α → β
H : ∀ (x : β), x ∈ (map f₂ xs).toList → p x
⊢ pmap (p := p) f₁ (map f₂ xs) H = pmap (p := fun (x : α) ↦ p (f₂ x)) (fun (x : α) (hx : p (f₂ x)) ↦ f₁ (f₂ x) hx) xs ⋯
have nil : ∀ (H : ∀ (x : β), x ∈ (map f₂ nil).toList → p x),
  pmap (p := p) f₁ (map f₂ nil) H =
    pmap (p := fun (x : α) ↦ p (f₂ x)) (fun (x : α) (hx : p (f₂ x)) ↦ f₁ (f₂ x) hx) nil sorry
Tactic: induction xs
Cleared hypotheses: 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
p : β → Prop
f₁ : (b : β) → p b → γ
f₂ : α → β
H : ∀ (x : β), x ∈ (map f₂ xs).toList → p x
nil :
  ∀ (H : ∀ (x : β), x ∈ (map f₂ Vector.nil).toList → p x),
    pmap (p := p) f₁ (map f₂ Vector.nil) H =
      pmap (p := fun (x : α) ↦ p (f₂ x)) (fun (x : α) (hx : p (f₂ x)) ↦ f₁ (f₂ x) hx) Vector.nil ⋯
⊢ pmap (p := p) f₁ (map f₂ xs) H = pmap (p := fun (x : α) ↦ p (f₂ x)) (fun (x : α) (hx : p (f₂ x)) ↦ f₁ (f₂ x) hx) xs ⋯
have cons : ∀ {n : ℕ} {x : α} {w : Vector α n},
  (∀ (H : ∀ (x : β), x ∈ (map f₂ w).toList → p x),
      pmap (p := p) f₁ (map f₂ w) H =
        pmap (p := fun (x : α) ↦ p (f₂ x)) (fun (x : α) (hx : p (f₂ x)) ↦ f₁ (f₂ x) hx) w sorry) →
    ∀ (H : ∀ (x_1 : β), x_1 ∈ (map f₂ (x ::ᵥ w)).toList → p x_1),
      pmap (p := p) f₁ (map f₂ (x ::ᵥ w)) H =
        pmap (p := fun (x : α) ↦ p (f₂ x)) (fun (x : α) (hx : p (f₂ x)) ↦ f₁ (f₂ x) hx) (x ::ᵥ w) sorry
Tactic: induction xs
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_4
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : γ → β → σ₁ → σ₁ × ζ
f₂ : α → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ (mapAccumr f₂ xs s₂).2 ys s₁ =
    let m : (σ₁ × σ₂) × Vector ζ n :=
      mapAccumr₂
        (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
          let r₂ := f₂ x s.2;
          let r₁ := f₁ r₂.2 y s.1;
          ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)
have nil : ∀ {s₁ : σ₁} {s₂ : σ₂},
  mapAccumr₂ f₁ (mapAccumr f₂ nil s₂).2 nil s₁ =
    let m : (σ₁ × σ₂) × Vector ζ 0 :=
      mapAccumr₂
        (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
          let r₂ := f₂ x s.2;
          let r₁ := f₁ r₂.2 y s.1;
          ((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_4
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : γ → β → σ₁ → σ₁ × ζ
f₂ : α → σ₂ → σ₂ × γ
nil :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr₂ f₁ (mapAccumr f₂ Vector.nil s₂).2 Vector.nil s₁ =
      let m : (σ₁ × σ₂) × Vector ζ 0 :=
        mapAccumr₂
          (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
            let r₂ := f₂ x s.2;
            let r₁ := f₁ r₂.2 y s.1;
            ((r₁.1, r₂.1), r₁.2))
          Vector.nil Vector.nil (s₁, s₂);
      (m.1.1, m.2)
⊢ mapAccumr₂ f₁ (mapAccumr f₂ xs s₂).2 ys s₁ =
    let m : (σ₁ × σ₂) × Vector ζ n :=
      mapAccumr₂
        (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
          let r₂ := f₂ x s.2;
          let r₁ := f₁ r₂.2 y s.1;
          ((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 s₂).2 ys s₁ =
        let m : (σ₁ × σ₂) × Vector ζ n :=
          mapAccumr₂
            (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
              let r₂ := f₂ x s.2;
              let r₁ := f₁ r₂.2 y s.1;
              ((r₁.1, r₂.1), r₁.2))
            xs ys (s₁, s₂);
        (m.1.1, m.2)) →
    ∀ {s₁ : σ₁} {s₂ : σ₂},
      mapAccumr₂ f₁ (mapAccumr f₂ (xs.snoc x) s₂).2 (ys.snoc y) s₁ =
        let m : (σ₁ × σ₂) × Vector ζ (n + 1) :=
          mapAccumr₂
            (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
              let r₂ := f₂ x s.2;
              let r₁ := f₁ r₂.2 y s.1;
              ((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_4
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : γ → β → ζ
f₂ : α → γ
⊢ map₂ f₁ (map f₂ xs) ys = map₂ (fun (x : α) (y : β) ↦ f₁ (f₂ x) y) xs ys
have nil : map₂ f₁ (map f₂ nil) nil = map₂ (fun (x : α) (y : β) ↦ f₁ (f₂ x) y) nil nil
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
ζ : 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
⊢ map₂ f₁ (map f₂ xs) ys = map₂ (fun (x : α) (y : β) ↦ f₁ (f₂ x) y) xs ys
have 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)
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
ζ : Type u_4
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : α → γ → σ₁ → σ₁ × ζ
f₂ : β → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ xs (mapAccumr f₂ ys s₂).2 s₁ =
    let m : (σ₁ × σ₂) × Vector ζ n :=
      mapAccumr₂
        (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
          let r₂ := f₂ y s.2;
          let r₁ := f₁ x r₂.2 s.1;
          ((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 s₂).2 s₁ =
    let m : (σ₁ × σ₂) × Vector ζ 0 :=
      mapAccumr₂
        (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
          let r₂ := f₂ y s.2;
          let r₁ := f₁ x r₂.2 s.1;
          ((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_4
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : α → γ → σ₁ → σ₁ × ζ
f₂ : β → σ₂ → σ₂ × γ
nil :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr₂ f₁ Vector.nil (mapAccumr f₂ Vector.nil s₂).2 s₁ =
      let m : (σ₁ × σ₂) × Vector ζ 0 :=
        mapAccumr₂
          (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
            let r₂ := f₂ y s.2;
            let r₁ := f₁ x r₂.2 s.1;
            ((r₁.1, r₂.1), r₁.2))
          Vector.nil Vector.nil (s₁, s₂);
      (m.1.1, m.2)
⊢ mapAccumr₂ f₁ xs (mapAccumr f₂ ys s₂).2 s₁ =
    let m : (σ₁ × σ₂) × Vector ζ n :=
      mapAccumr₂
        (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
          let r₂ := f₂ y s.2;
          let r₁ := f₁ x r₂.2 s.1;
          ((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₂ ys s₂).2 s₁ =
        let m : (σ₁ × σ₂) × Vector ζ n :=
          mapAccumr₂
            (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
              let r₂ := f₂ y s.2;
              let r₁ := f₁ x r₂.2 s.1;
              ((r₁.1, r₂.1), r₁.2))
            xs ys (s₁, s₂);
        (m.1.1, m.2)) →
    ∀ {s₁ : σ₁} {s₂ : σ₂},
      mapAccumr₂ f₁ (xs.snoc x) (mapAccumr f₂ (ys.snoc y) s₂).2 s₁ =
        let m : (σ₁ × σ₂) × Vector ζ (n + 1) :=
          mapAccumr₂
            (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
              let r₂ := f₂ y s.2;
              let r₁ := f₁ x r₂.2 s.1;
              ((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_4
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : α → γ → ζ
f₂ : β → γ
⊢ map₂ f₁ xs (map f₂ ys) = map₂ (fun (x : α) (y : β) ↦ f₁ x (f₂ y)) xs ys
have nil : map₂ f₁ nil (map f₂ nil) = map₂ (fun (x : α) (y : β) ↦ f₁ x (f₂ y)) nil nil
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
ζ : Type u_4
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : α → γ → ζ
f₂ : β → γ
nil : map₂ f₁ Vector.nil (map f₂ Vector.nil) = map₂ (fun (x : α) (y : β) ↦ f₁ x (f₂ y)) Vector.nil Vector.nil
⊢ map₂ f₁ xs (map f₂ ys) = map₂ (fun (x : α) (y : β) ↦ f₁ x (f₂ y)) xs ys
have snoc : ∀ {n : ℕ} (xs : Vector α n) (ys : Vector β n) (x : α) (y : β),
  map₂ f₁ xs (map f₂ ys) = map₂ (fun (x : α) (y : β) ↦ f₁ x (f₂ y)) xs ys →
    map₂ f₁ (xs.snoc x) (map f₂ (ys.snoc y)) = map₂ (fun (x : α) (y : β) ↦ f₁ x (f₂ y)) (xs.snoc x) (ys.snoc y)
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
ζ : Type u_4
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : γ → σ₁ → σ₁ × ζ
f₂ : α → β → σ₂ → σ₂ × γ
⊢ mapAccumr f₁ (mapAccumr₂ f₂ xs ys s₂).2 s₁ =
    let m : (σ₁ × σ₂) × Vector ζ n :=
      mapAccumr₂
        (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
          let r₂ := f₂ x y s.2;
          let r₁ := f₁ r₂.2 s.1;
          ((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 s₁ =
    let m : (σ₁ × σ₂) × Vector ζ 0 :=
      mapAccumr₂
        (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
          let r₂ := f₂ x y s.2;
          let r₁ := f₁ r₂.2 s.1;
          ((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_4
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : γ → σ₁ → σ₁ × ζ
f₂ : α → β → σ₂ → σ₂ × γ
nil :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr f₁ (mapAccumr₂ f₂ Vector.nil Vector.nil s₂).2 s₁ =
      let m : (σ₁ × σ₂) × Vector ζ 0 :=
        mapAccumr₂
          (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
            let r₂ := f₂ x y s.2;
            let r₁ := f₁ r₂.2 s.1;
            ((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 s₁ =
    let m : (σ₁ × σ₂) × Vector ζ n :=
      mapAccumr₂
        (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
          let r₂ := f₂ x y s.2;
          let r₁ := f₁ r₂.2 s.1;
          ((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 s₁ =
        let m : (σ₁ × σ₂) × Vector ζ n :=
          mapAccumr₂
            (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
              let r₂ := f₂ x y s.2;
              let r₁ := f₁ r₂.2 s.1;
              ((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 s₁ =
        let m : (σ₁ × σ₂) × Vector ζ (n + 1) :=
          mapAccumr₂
            (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
              let r₂ := f₂ x y s.2;
              let r₁ := f₁ r₂.2 s.1;
              ((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_4
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : γ → ζ
f₂ : α → β → γ
⊢ map f₁ (map₂ f₂ xs ys) = map₂ (fun (x : α) (y : β) ↦ f₁ (f₂ x y)) xs ys
have nil : map f₁ (map₂ f₂ nil nil) = map₂ (fun (x : α) (y : β) ↦ f₁ (f₂ x y)) nil nil
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
ζ : 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
⊢ map f₁ (map₂ f₂ xs ys) = map₂ (fun (x : α) (y : β) ↦ f₁ (f₂ x y)) xs ys
have 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)
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
σ₁ : 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 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)
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 x 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 x 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 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)
have 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)
Tactic: induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
Cleared hypotheses: s₁, s₂, xs, ys