no goals
α : Type u_1
β : Type ?u.12788
L : List (List α)
i j : ℕ
hi : i < length L
hj : j < length (nthLe L i hi)
⊢ sum (take i (map length L)) + j < sum (take (i + 1) (map length L))
simp [hi, sum_take_succ, hj]