α : Type u_1
β : Type ?u.15601
L : List (List α)
i j : ℕ
hi : i < length L
hj : j < length (nthLe L i hi)
this :
  nthLe (join L) (sum (take i (map length L)) + j) (_ : sum (take i (map length L)) + j < length (join L)) =
    nthLe (take (sum (take (i + 1) (map length L))) (join L)) (sum (take i (map length L)) + j)
      (_ : sum (take i (map length L)) + j < length (take (sum (take (i + 1) (map length L))) (join L)))
⊢ nthLe (join L) (sum (take i (map length L)) + j) (_ : sum (take i (map length L)) + j < length (join L)) =
    nthLe (nthLe L i hi) j hj
α : Type u_1
β : Type ?u.15601
L : List (List α)
i j : ℕ
hi : i < length L
hj : j < length (nthLe L i hi)
⊢ nthLe (join L) (sum (take i (map length L)) + j) (_ : sum (take i (map length L)) + j < length (join L)) =
    nthLe (nthLe L i hi) j hj
have := nthLe_take L.join (sum_take_map_length_lt2 L hi hj) (sum_take_map_length_lt1 L hi hj)
no goals
α : Type u_1
β : Type ?u.15601
L : List (List α)
i j : ℕ
hi : i < length L
hj : j < length (nthLe L i hi)
this :
  nthLe (join L) (sum (take i (map length L)) + j) (_ : sum (take i (map length L)) + j < length (join L)) =
    nthLe (take (sum (take (i + 1) (map length L))) (join L)) (sum (take i (map length L)) + j)
      (_ : sum (take i (map length L)) + j < length (take (sum (take (i + 1) (map length L))) (join L)))
⊢ nthLe (join L) (sum (take i (map length L)) + j) (_ : sum (take i (map length L)) + j < length (join L)) =
    nthLe (nthLe L i hi) j hj
rw [this, nthLe_drop, nthLe_of_eq (drop_take_succ_join_eq_nthLe L hi)]