α : Type u_1
β : Type ?u.25223
t : α
ts : List α
r L : List (List α)
n : ℕ
H : ∀ (l : List α), l ∈ L → length l = n
⊢ sum (map length L) = n * length L
α : Type u_1
β : Type ?u.25223
t : α
ts : List α
r L : List (List α)
n : ℕ
H : ∀ (l : List α), l ∈ L → length l = n
⊢ length (foldr (fun y r => (permutationsAux2 t ts r y id).snd) r L) = n * length L + length r
rw [length_foldr_permutationsAux2, (_ : List.sum (map length L) = n * length L)]
case nil
α : Type u_1
β : Type ?u.25223
t : α
ts : List α
r L : List (List α)
n : ℕ
H✝ : ∀ (l : List α), l ∈ L → length l = n
H : ∀ (l : List α), l ∈ [] → length l = n
⊢ sum (map length []) = n * length []

case cons
α : Type u_1
β : Type ?u.25223
t : α
ts : List α
r L✝ : List (List α)
n : ℕ
H✝ : ∀ (l : List α), l ∈ L✝ → length l = n
l : List α
L : List (List α)
ih : (∀ (l : List α), l ∈ L → length l = n) → sum (map length L) = n * length L
H : ∀ (l_1 : List α), l_1 ∈ l :: L → length l_1 = n
⊢ sum (map length (l :: L)) = n * length (l :: L)
α : Type u_1
β : Type ?u.25223
t : α
ts : List α
r L : List (List α)
n : ℕ
H : ∀ (l : List α), l ∈ L → length l = n
⊢ sum (map length L) = n * length L
induction' L with l L ih
case cons
α : Type u_1
β : Type ?u.25223
t : α
ts : List α
r L✝ : List (List α)
n : ℕ
H✝ : ∀ (l : List α), l ∈ L✝ → length l = n
l : List α
L : List (List α)
ih : (∀ (l : List α), l ∈ L → length l = n) → sum (map length L) = n * length L
H : ∀ (l_1 : List α), l_1 ∈ l :: L → length l_1 = n
sum_map : sum (map length L) = n * length L
⊢ sum (map length (l :: L)) = n * length (l :: L)
case cons
α : Type u_1
β : Type ?u.25223
t : α
ts : List α
r L✝ : List (List α)
n : ℕ
H✝ : ∀ (l : List α), l ∈ L✝ → length l = n
l : List α
L : List (List α)
ih : (∀ (l : List α), l ∈ L → length l = n) → sum (map length L) = n * length L
H : ∀ (l_1 : List α), l_1 ∈ l :: L → length l_1 = n
⊢ sum (map length (l :: L)) = n * length (l :: L)
have sum_map : sum (map length L) = n * length L := ih fun l m => H l (mem_cons_of_mem _ m)
case cons
α : Type u_1
β : Type ?u.25223
t : α
ts : List α
r L✝ : List (List α)
n : ℕ
H✝ : ∀ (l : List α), l ∈ L✝ → length l = n
l : List α
L : List (List α)
ih : (∀ (l : List α), l ∈ L → length l = n) → sum (map length L) = n * length L
H : ∀ (l_1 : List α), l_1 ∈ l :: L → length l_1 = n
sum_map : sum (map length L) = n * length L
length_l : length l = n
⊢ sum (map length (l :: L)) = n * length (l :: L)
case cons
α : Type u_1
β : Type ?u.25223
t : α
ts : List α
r L✝ : List (List α)
n : ℕ
H✝ : ∀ (l : List α), l ∈ L✝ → length l = n
l : List α
L : List (List α)
ih : (∀ (l : List α), l ∈ L → length l = n) → sum (map length L) = n * length L
H : ∀ (l_1 : List α), l_1 ∈ l :: L → length l_1 = n
sum_map : sum (map length L) = n * length L
⊢ sum (map length (l :: L)) = n * length (l :: L)
have length_l : length l = n := H _ (mem_cons_self _ _)
no goals
case cons
α : Type u_1
β : Type ?u.25223
t : α
ts : List α
r L✝ : List (List α)
n : ℕ
H✝ : ∀ (l : List α), l ∈ L✝ → length l = n
l : List α
L : List (List α)
ih : (∀ (l : List α), l ∈ L → length l = n) → sum (map length L) = n * length L
H : ∀ (l_1 : List α), l_1 ∈ l :: L → length l_1 = n
sum_map : sum (map length L) = n * length L
length_l : length l = n
⊢ sum (map length (l :: L)) = n * length (l :: L)
simp [sum_map, length_l, mul_add, add_comm, mul_succ]
no goals
case nil
α : Type u_1
β : Type ?u.25223
t : α
ts : List α
r L : List (List α)
n : ℕ
H✝ : ∀ (l : List α), l ∈ L → length l = n
H : ∀ (l : List α), l ∈ [] → length l = n
⊢ sum (map length []) = n * length []
simp