English
For any a,b and l, the lists (permutations'Aux a l).flatMap (permutations'Aux b) and (permutations'Aux b l).flatMap (permutations'Aux a) are permutation-equivalent.
Русский
Для любых a,b и l списки (permutations'Aux a l).flatMap (permutations'Aux b) и (permutations'Aux b l).flatMap (permutations'Aux a) эквивалентны по перестановке.
LaTeX
$$$$ (permutations'Aux a l).flatMap (permutations'Aux b) \;\sim\; (permutations'Aux b l).flatMap (permutations'Aux a) $$$$
Lean4
theorem perm_permutations'Aux_comm (a b : α) (l : List α) :
(permutations'Aux a l).flatMap (permutations'Aux b) ~ (permutations'Aux b l).flatMap (permutations'Aux a) :=
by
induction l with
| nil => exact Perm.swap [a, b] [b, a] []
| cons c l ih => ?_
simp only [permutations'Aux, flatMap_cons, map_cons, map_map, cons_append]
apply Perm.swap'
have :
∀ a b,
(map (cons c) (permutations'Aux a l)).flatMap (permutations'Aux b) ~
map (cons b ∘ cons c) (permutations'Aux a l) ++
map (cons c) ((permutations'Aux a l).flatMap (permutations'Aux b)) :=
by
intro a' b'
simp only [flatMap_map, permutations'Aux]
change (permutations'Aux _ l).flatMap (fun a => ([b' :: c :: a] ++ map (cons c) (permutations'Aux _ a))) ~ _
refine (flatMap_append_perm _ (fun x => [b' :: c :: x]) _).symm.trans ?_
rw [← map_eq_flatMap, ← map_flatMap]
exact Perm.refl _
refine (((this _ _).append_left _).trans ?_).trans ((this _ _).append_left _).symm
rw [← append_assoc, ← append_assoc]
exact perm_append_comm.append (ih.map _)
