Missing simp lemmas for vector cardinality?

Stream: mathlib4

[Li Xuanji]

Is it expected that the second example is failing?

import Mathlib

example : Nat.card (List.Vector Bool 2) = 4 := by simp -- ok
example : Nat.card (Vector Bool 2) = 4 := by simp -- fails

[Eric Wieser]

This probably belongs in #mathlib4 (someone can probably move it for us), since docs#Nat.card is from mathlib

[Notification Bot]

This topic was moved here from #lean4 > Missing simp lemmas for vector cardinality? by Kevin Buzzard.

[Robin Arnez]

Well these are two different things and List.Vector naturally has more api because of existing for longer.
Your case can be solved using:

import Mathlib.SetTheory.Cardinal.Finite

def Vector.equivListVector : Vector α n ≃ List.Vector α n where
  toFun x := ⟨x.toArray.toList, x.size_toArray⟩
  invFun x := ⟨x.1.toArray, x.2⟩
  left_inv _ := rfl
  right_inv _ := rfl

example : Nat.card (Vector Bool 2) = 4 := by simp [Nat.card_congr Vector.equivListVector]

(but still, both should probably exist)

[Eric Wieser]

That equiv is in an open PR, #25050