case mk
n : ℕ
α : Type u_2
β : Type u_1
f : α → β
val✝ : List α
property✝ : List.length val✝ = n
⊢ toList (map f { val := val✝, property := property✝ }) = List.map f (toList { val := val✝, property := property✝ })
n : ℕ
α : Type u_2
β : Type u_1
v : Vector α n
f : α → β
⊢ toList (map f v) = List.map f (toList v)
cases v
no goals
case mk
n : ℕ
α : Type u_2
β : Type u_1
f : α → β
val✝ : List α
property✝ : List.length val✝ = n
⊢ toList (map f { val := val✝, property := property✝ }) = List.map f (toList { val := val✝, property := property✝ })
rfl