rw [Finset.sum_range_succ, ← pn]
case succ
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
n : ℕ
pn :
  ((choose_indecent_words is_decent a h).get n).start =
    ∑ j ∈ Finset.range n, ((choose_indecent_words is_decent a h).get j).length
⊢ ((choose_indecent_words is_decent a h).get (n + 1)).start =
    ∑ j ∈ Finset.range (n + 1), ((choose_indecent_words is_decent a h).get j).length
case succ
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
n : ℕ
pn :
  ((choose_indecent_words is_decent a h).get n).start =
    ∑ j ∈ Finset.range n, ((choose_indecent_words is_decent a h).get j).length
⊢ ((choose_indecent_words is_decent a h).get (n + 1)).start =
    ((choose_indecent_words is_decent a h).get n).start + ((choose_indecent_words is_decent a h).get n).length