α : Type u_1
β : Type ?u.9242
L : List (List α)
i : Fin (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)) = get L i
α : Type u_1
β : Type ?u.9242
L : List (List α)
i : Fin (length L)
⊢ drop (sum (take (↑i) (map length L))) (take (sum (take (↑i + 1) (map length L))) (join L)) = get L i
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.9242
L : List (List α)
i : Fin (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)) = get L i
simp [take_sum_join, this, drop_sum_join, drop_take_succ_eq_cons_get]
no goals
α : Type u_1
β : Type ?u.9242
L : List (List α)
i : Fin (length L)
⊢ take (↑i) (map length L) = take (↑i) (map length (take (↑i + 1) L))
simp [map_take, take_take]