α : Type u_1
β : Type ?u.11187
L : List (List α)
i : ℕ
hi : i < length L
this : take i (map length L) = take i (map length (take (i + 1) L))
⊢ drop (sum (take i (map length L))) (take (sum (take (i + 1) (map length L))) (join L)) = nthLe L i hi
α : Type u_1
β : Type ?u.11187
L : List (List α)
i : ℕ
hi : i < length L
⊢ drop (sum (take i (map length L))) (take (sum (take (i + 1) (map length L))) (join L)) = nthLe L i hi
have : (L.map length).take i = ((L.take (i + 1)).map length).take i := by
  simp [map_take, take_take]
no goals
α : Type u_1
β : Type ?u.11187
L : List (List α)
i : ℕ
hi : i < length L
this : take i (map length L) = take i (map length (take (i + 1) L))
⊢ drop (sum (take i (map length L))) (take (sum (take (i + 1) (map length L))) (join L)) = nthLe L i hi
simp [take_sum_join, this, drop_sum_join, drop_take_succ_eq_cons_nthLe _ hi]
no goals
α : Type u_1
β : Type ?u.11187
L : List (List α)
i : ℕ
hi : i < length L
⊢ take i (map length L) = take i (map length (take (i + 1) L))
simp [map_take, take_take]