Vector heq

Stream: Is there code for X?

[Praneeth Kolichala]

The following type:

lemma vector.heq {α : Type*} { m n : ℕ } {v1 : vector α m} {v2 : vector α n}
  (list_eq : v1.to_list = v2.to_list) (H : m = n) : v1 == v2 := sorry

(Note that H is not necessary, but I can get H easily from the hypothesis list_eq already anyway).
Hovering over == in VSCode, it says that I might be doing something wrong if I need to prove ==. My use case is that I want to convert a finite type involving vectors to a more general one that uses lists. I want the finite type to use vectors so that I can easily get finset.univ and those kinds of things. But in order to prove that my embedding is injective, I need that when two lists of the same length are equal, the corresponding vectors are equal. Maybe there's a better way?