English
The second component of permutationsAux2 equals an appended map of the previous stage, followed by r.
Русский
Вторая компонента permutationsAux2 равна объединению отображения и r.
LaTeX
$$$\forall {\alpha}, {\beta}, {t}, {ts}, {r}, {ys}, {f}: List\;\alpha \to \beta, (permutationsAux2 t ts r ys f).2 = ((List.map (fun x => f (x ++ ts)) (permutationsAux2 t List.nil List.nil ys id).2) ++ r)$$$
Lean4
/-- An expository lemma to show how all of `ts`, `r`, and `f` can be eliminated from
`permutationsAux2`.
`(permutationsAux2 t [] [] ys id).2`, which appears on the RHS, is a list whose elements are
produced by inserting `t` into every non-terminal position of `ys` in order. As an example:
```lean
#eval permutationsAux2 1 [] [] [2, 3, 4] id
-- [[1, 2, 3, 4], [2, 1, 3, 4], [2, 3, 1, 4]]
```
-/
theorem permutationsAux2_snd_eq (t : α) (ts : List α) (r : List β) (ys : List α) (f : List α → β) :
(permutationsAux2 t ts r ys f).2 = ((permutationsAux2 t [] [] ys id).2.map fun x => f (x ++ ts)) ++ r := by
rw [← permutationsAux2_append, map_permutationsAux2, permutationsAux2_comp_append]
