induction' i with i ih
case h
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ sum σ i = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).fst
case h.zero
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
⊢ sum σ Nat.zero = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) Nat.zero).fst

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
⊢ sum σ (Nat.succ i) = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) (Nat.succ i)).fst