English
For any predicate p and function f, the pmap of l after inserting a at n behaves as inserting a at n then pmapping with updated proofs.
Русский
Для любого предиката p и функции f pmap дает равенство после вставки a на позиции n с обновлением доказательств.
LaTeX
$$$\\text{(pmap f l hl).insertIdx n (f a ha) = pmap f (l.insertIdx n a) (\\lambda _ h, (eq\\_or\\_mem\\_of\\_mem\\_insertIdx h).elim (\\lambda heq, heq \\Rightarrow ha) (hl _))}$$$
Lean4
theorem insertIdx_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} {a : α} {n : ℕ} (hl : ∀ x ∈ l, p x) (ha : p a) :
(l.pmap f hl).insertIdx n (f a ha) =
(l.insertIdx n a).pmap f (fun _ h ↦ (eq_or_mem_of_mem_insertIdx h).elim (fun heq ↦ heq ▸ ha) (hl _)) :=
by
induction n generalizing l with
| zero => cases l <;> simp
| succ n ihn => cases l <;> simp_all
