English
For all α, a, r1, r2, we have sublists'Aux a r1 r2 equals (r1.toArray).foldl (init := r2.toArray) (λ r l. r.push (a :: l)).toList.
Русский
Для всех α, a, r1, r2 выполняется равенство: sublists'Aux a r1 r2 = (r1.toArray).foldl ...
LaTeX
$$$\\forall {\\alpha} (a: \\alpha) (r_1 r_2: List(\\mathrm{List}(\\alpha))),\\; \\\\text{sublists'Aux a r_1 r_2} = ((r_1.toArray).foldl (init := r_2.toArray) (\\\\lambda r l. r.push (a :: l))).toList$$$
Lean4
theorem sublistsAux_eq_array_foldl :
sublistsAux = fun (a : α) (r : List (List α)) =>
(r.toArray.foldl (init := #[]) fun r l => (r.push l).push (a :: l)).toList :=
by
funext a r
simp only [sublistsAux]
have :=
foldl_hom Array.toList (g₁ := fun r l => (r.push l).push (a :: l)) (g₂ := fun r l => r ++ [l, a :: l]) (l := r)
(init := #[]) (by simp)
simpa using this
