English
Let is, is', ts be lists. Then the auxiliary permutations of is ++ ts with is' equals the concatenation of (permutationsAux is is').map (append ts) with permutationsAux ts (is.reverse ++ is').
Русский
Пусть is, is', ts — списки. Тогда permutationsAux (is ++ ts) is' = (permutationsAux is is').map (append ts) ++ permutationsAux ts (is.reverse ++ is').
LaTeX
$$$$\mathrm{permutationsAux}(is ++ ts)\; is' = (\mathrm{permutationsAux} is is').map (\cdot\;\, ts) ++ \mathrm{permutationsAux}\ ts\ (is.reverse ++ is')$$$$
Lean4
theorem permutationsAux_append (is is' ts : List α) :
permutationsAux (is ++ ts) is' = (permutationsAux is is').map (· ++ ts) ++ permutationsAux ts (is.reverse ++ is') :=
by
induction is generalizing is' with
| nil => simp
| cons t is
ih =>
simp only [foldr_permutationsAux2, ih, map_flatMap, cons_append, permutationsAux_cons, map_append, reverse_cons,
append_assoc]
congr 2
funext _
rw [map_permutationsAux2]
simp +singlePass only [← permutationsAux2_comp_append]
simp only [id, append_assoc]
