simp only [iterate_eq_Nat_iterate, head, nth]
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
ih : sum σ i = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).fst
⊢ σ (i + 1) = head (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).snd
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
ih : sum σ i = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).fst
⊢ σ (i + 1) = Prod.snd ((fun x => (x.fst + Prod.snd x 0, tail x.snd))^[i] (σ 0, tail σ)) 0