intro j
α : Type
is_decent : List α → Prop
a : Stream' α
hinit : all_prefixes is_decent a
hnot : ∀ (n : ℕ), ∃ k, 0 < k ∧ all_prefixes is_decent (Stream'.drop (n + k) a)
⊢ Stream'.All is_decent fun i =>
    Stream'.take ((choose_decent_words is_decent a hinit hnot).get i).length
      (Stream'.drop ((choose_decent_words is_decent a hinit hnot).get i).start a)
α : Type
is_decent : List α → Prop
a : Stream' α
hinit : all_prefixes is_decent a
hnot : ∀ (n : ℕ), ∃ k, 0 < k ∧ all_prefixes is_decent (Stream'.drop (n + k) a)
j : ℕ
⊢ is_decent
    (Stream'.get
      (fun i =>
        Stream'.take ((choose_decent_words is_decent a hinit hnot).get i).length
          (Stream'.drop ((choose_decent_words is_decent a hinit hnot).get i).start a))
      j)