English
Let t ∈ α, ts ∈ List α, and r, L ∈ List (List α) with n ∈ ℕ and H saying every l ∈ L has length n. Then length (foldr (λ y r, (permutationsAux2 t ts r y id).2) r L) = n * length L + length r.
Русский
Пусть t ∈ α, ts ∈ List α, и r, L ∈ List (List α) такие, что существует число n ∈ ℕ и H: для каждого l ∈ L имеет длину n. Тогда длина (foldr (λ y r, (permutationsAux2 t ts r y id).2) r L) равна n * length L + length r.
LaTeX
$$$$\operatorname{length}\left(\mathrm{foldr}\left(\lambda y\, r,\; (\mathrm{permutationsAux2}\ t\ ts\ r\ y\ id).2\right)\ r\ L\right) = n \cdot \operatorname{length} L + \operatorname{length} r.$$$$
Lean4
theorem length_foldr_permutationsAux2' (t : α) (ts : List α) (r L : List (List α)) (n) (H : ∀ l ∈ L, length l = n) :
length (foldr (fun y r => (permutationsAux2 t ts r y id).2) r L) = n * length L + length r :=
by
rw [length_foldr_permutationsAux2, (_ : (map length L).sum = n * length L)]
induction L with
| nil => simp
| cons l L
ih =>
have sum_map : (map length L).sum = n * length L := ih fun l m => H l (mem_cons_of_mem _ m)
have length_l : length l = n := H _ mem_cons_self
simp [sum_map, length_l, Nat.add_comm, mul_succ]
