case nil
α : Type u_1
β : Type ?u.6451
i : ℕ
⊢ drop (sum (take i (map length []))) (join []) = join (drop i [])

case cons
α : Type u_1
β : Type ?u.6451
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), drop (sum (take i (map length tail✝))) (join tail✝) = join (drop i tail✝)
i : ℕ
⊢ drop (sum (take i (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) = join (drop i (head✝ :: tail✝))
α : Type u_1
β : Type ?u.6451
L : List (List α)
i : ℕ
⊢ drop (sum (take i (map length L))) (join L) = join (drop i L)
induction L generalizing i
no goals
case nil
α : Type u_1
β : Type ?u.6451
i : ℕ
⊢ drop (sum (take i (map length []))) (join []) = join (drop i [])
simp
no goals
case cons
α : Type u_1
β : Type ?u.6451
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), drop (sum (take i (map length tail✝))) (join tail✝) = join (drop i tail✝)
i : ℕ
⊢ drop (sum (take i (map length (head✝ :: tail✝)))) (join (head✝ :: tail✝)) = join (drop i (head✝ :: tail✝))
cases i <;> simp [drop_append, *]