English
For any list l and maps f,g, l.flatMap f ++ l.flatMap g is permuted with l.flatMap (λ x, f x ++ g x).
Русский
Для любого списка l и отображений f,g, l.flatMap f ++ l.flatMap g перестановочно эквивалентен l.flatMap (λ x, f x ++ g x).
LaTeX
$$$l.flatMap f \\; \\text{and} \\; l.flatMap g \\sim l.flatMap (\\lambda x. f\\,x \\;\\cup\\; g\\,x)$$$
Lean4
theorem flatMap_append_perm (l : List α) (f g : α → List β) :
l.flatMap f ++ l.flatMap g ~ l.flatMap fun x => f x ++ g x :=
by
induction l with
| nil => simp
| cons a l IH => ?_
simp only [flatMap_cons, append_assoc]
refine (Perm.trans ?_ (IH.append_left _)).append_left _
rw [← append_assoc, ← append_assoc]
exact perm_append_comm.append_right _
