induction' n with pn hpn
case h.e_a
α : Type
n : ℕ
⊢ ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get n).2 =
      Stream'.drop (∑ j ∈ Finset.range n, lengths j) a
case h.e_a.zero
α : Type
⊢ ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get 0).2 =
      Stream'.drop (∑ j ∈ Finset.range 0, lengths j) a

case h.e_a.succ
α : Type
pn : ℕ
hpn :
  ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get pn).2 =
      Stream'.drop (∑ j ∈ Finset.range pn, lengths j) a
⊢ ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get (pn + 1)).2 =
      Stream'.drop (∑ j ∈ Finset.range (pn + 1), lengths j) a