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

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