English
For any list L and x, the identity x ++ (L.map (· ++ x)).flatten = (L.map (x ++ ·)).flatten ++ x holds; it rewrites bracketing of concatenations.
Русский
Для списка L и x выполняется равенство: x ++ (L.map (· ++ x)).flatten = (L.map (x ++ ·)).flatten ++ x, демонстрирующее изменение скобок при конкатенациях.
LaTeX
$$$$ x \\;\\|\\+\\; (L.\\mathrm{map}(\\cdot ++ x)).\\mathrm{flatten} = (L.\\mathrm{map}(x ++ \\cdot)).\\mathrm{flatten} \\;\\|\\; x. $$$$
Lean4
/-- We can rebracket `x ++ (l₁ ++ x) ++ (l₂ ++ x) ++ ... ++ (lₙ ++ x)` to
`(x ++ l₁) ++ (x ++ l₂) ++ ... ++ (x ++ lₙ) ++ x` where `L = [l₁, l₂, ..., lₙ]`. -/
theorem append_flatten_map_append (L : List (List α)) (x : List α) :
x ++ (L.map (· ++ x)).flatten = (L.map (x ++ ·)).flatten ++ x := by induction L with grind
