Vector Map Equalities in Mathlib

Stream: new members

[Anton Mueller]

I tried to find theorems like this in mathlib, essentially reducing Vector.map equalities to the underlying List.map equalities. One such theorem in question:

import Mathlib.Data.Vector.Defs
import Mathlib.Data.Vector.Basic

open Mathlib Set Vector

example (ts : Vector ℕ m) : map v ts = map v' ts ↔ ∀ t ∈ ts.1, v' t = v t := by
  sorry

This should't be too hard to prove, but i think a theorem like this should already be available?

Edit: This should be an #mwe as suggested by @Kevin Buzzard

[Kevin Buzzard]

Your question will probably get more attention if you ask it in the form of a #mwe