case intro.intro
n : ℕ
α : Type u_2
β : Type u_1
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ head (map f v) = f (head v)
n : ℕ
α : Type u_2
β : Type u_1
v : Vector α (n + 1)
f : α → β
⊢ head (map f v) = f (head v)
obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v
no goals
case intro.intro
n : ℕ
α : Type u_2
β : Type u_1
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ head (map f v) = f (head v)
rw [h, map_cons, head_cons, head_cons]