English
Let p and f be as above and v a vector of length n+1 with hp holding for all elements. Then the tail of the pmap is the pmap of the tail with a corresponding predicate that uses hp restricted to the tail.
Русский
Пусть p и f заданы как выше, и v — вектор длины n+1 с выполнимым hp для всех элементов. Тогда хвост pmap-образа равен pmap f на хвосте v с подходящим ограничением hp для хвоста.
LaTeX
$$$\forall p:\alpha\to\mathrm{Prop},\ f:(a:\alpha)\to p(a)\to\beta,\ v:\mathrm{Vector}\,\alpha\,(n+1),\ hp:\forall x\in v.toList, p\,x\;\to\ (v.pmap\ f\ hp).tail = v.tail.pmap\ f\ (\lambda x\ hx\;\to\;hp\ _ \lvert by rw[\mbox{← cons_head_tail v}, toList_cons, List.mem_cons]; exact .inr hx) $$$
Lean4
@[simp]
theorem tail_pmap {p : α → Prop} (f : (a : α) → p a → β) (v : Vector α (n + 1)) (hp : ∀ x ∈ v.toList, p x) :
(v.pmap f hp).tail =
v.tail.pmap f (fun x hx ↦ hp _ <| by rw [← cons_head_tail v, toList_cons, List.mem_cons]; exact .inr hx) :=
by
obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v
simp_rw [h, pmap_cons, tail_cons]
