English
A specialized version of dest-map for the MvPFunctor M: the decomposition of a mapped element can be obtained by applying a corresponding mapping to its destination and reassembling using appendFun.
Русский
Специализированная версия dest-map для MvPFunctor M: разложение отображенного элемента получается применением соответствующего отображения к его разрушению и повторной сборкой через appendFun.
LaTeX
$$$\forall {\alpha \beta : TypeVec n} (g : \alpha \Rightarrow \beta) (x : P.M α) \\ (h : \forall x : P.M α, lastFun g x = (dropFun g <$$> x : P.M β)) : g <$$> M.dest P x = M.dest P (dropFun g <$$> x)$$$
Lean4
theorem map_dest {α β : TypeVec n} (g : (α ::: P.M α) ⟹ (β ::: P.M β)) (x : P.M α)
(h : ∀ x : P.M α, lastFun g x = (dropFun g <$$> x : P.M β)) : g <$$> M.dest P x = M.dest P (dropFun g <$$> x) :=
by
rw [M.dest_map]; congr
apply eq_of_drop_last_eq (by simp)
simp only [lastFun_appendFun]
ext1; apply h
