English
If the right-hand list l2 is nonempty, then modifying the last element of the concatenation l1 ++ l2 equals concatenating l1 with the modification of l2: modifyLast f (l1 ++ l2) = l1 ++ modifyLast f l2.
Русский
Если правая часть списка l2 непуста, то изменение последнего элемента конкатенации l1 ++ l2 эквивалентно конкатенации l1 со списком, где в конце стоит mодифицированный элемент: modifyLast f (l1 ++ l2) = l1 ++ modifyLast f l2.
LaTeX
$$$\\forall {\\alpha} f : \\alpha \\to \\alpha, \\forall l1 l2 : \\List(\\alpha), \\big( l2 \\neq [] \\Rightarrow modifyLast f (l1 \\append l2) = l1 \\append modifyLast f l2 \bigr)$$$
Lean4
theorem modifyLast_append_of_right_ne_nil (f : α → α) (l₁ l₂ : List α) (_ : l₂ ≠ []) :
modifyLast f (l₁ ++ l₂) = l₁ ++ modifyLast f l₂ := by
cases l₂ with
| nil => contradiction
| cons hd tl =>
cases tl with
| nil => exact modifyLast_concat _ hd _
| cons hd'
tl' =>
rw [append_cons, ← nil_append (hd :: hd' :: tl'), append_cons [], nil_append,
modifyLast_append_of_right_ne_nil _ (l₁ ++ [hd]) (hd' :: tl') _,
modifyLast_append_of_right_ne_nil _ [hd] (hd' :: tl') _, append_assoc]
all_goals { exact cons_ne_nil _ _
}
