English
A compatibility property for the auxiliary function: applying a composed function to the input and appending preserves append structure after mapping.
Русский
Свойство совместимости вспомогательной функции: применение композиции функций к входу и дополнение сохраняет структуру конкатенации после отображения.
LaTeX
$$$\\forall n\\ l\\ a\\ g\\ r\\ s:\\sublistsLenAux\\ n\\ l\\ (g \\circ f)\\ (r.map g ++ s) = (\\sublistsLenAux\\ n\\ l\\ f\\ r).map g ++ s$$$
Lean4
theorem sublistsLenAux_append :
∀ (n : ℕ) (l : List α) (f : List α → β) (g : β → γ) (r : List β) (s : List γ),
sublistsLenAux n l (g ∘ f) (r.map g ++ s) = (sublistsLenAux n l f r).map g ++ s
| 0, l, f, g, r, s => by unfold sublistsLenAux; simp
| _ + 1, [], _, _, _, _ => rfl
| n + 1, a :: l, f, g, r, s => by
unfold sublistsLenAux
simp only [show (g ∘ f) ∘ List.cons a = g ∘ f ∘ List.cons a by rfl, sublistsLenAux_append]
