English
The auxiliary operation sublists'Aux is equal to folding over the toArray representation of r1, pushing a :: l at each step starting from r2.toArray.
Русский
Вспомогательная операция sublists'Aux равна сведению по массиву (foldl) над representацией r1, добавляя в каждый шаг a :: l, начиная с r2.toArray.
LaTeX
$$$\\text{sublists'Aux}\\ a\\ r_1\\ r_2 = \\bigl( (r_1.toArray) \\text{foldl} (\\lambda R\\ l. R.push (a :: l)) (r_2.toArray) \\bigr).toList$$$
Lean4
theorem sublists'Aux_eq_array_foldl (a : α) :
∀ (r₁ r₂ : List (List α)),
sublists'Aux a r₁ r₂ = ((r₁.toArray).foldl (init := r₂.toArray) (fun r l => r.push (a :: l))).toList :=
by
intro r₁ r₂
rw [sublists'Aux, Array.foldl_toList]
have :=
List.foldl_hom Array.toList (g₁ := fun r l => r.push (a :: l)) (g₂ := fun r l => r ++ [a :: l]) (l := r₁) (init :=
r₂.toArray) (by simp)
simpa using this
