simp only [Function.iterate_succ, Function.comp_apply, ih, ←Nat.add_one]
case succ
α : Type ?u.25506
σ : Stream' α
z✝ x y : ℕ
ih : ∀ {z : ℕ}, (fun x_1 => x_1 + x)^[y] z = x * y + z
z : ℕ
⊢ (fun x_1 => x_1 + x)^[Nat.succ y] z = x * Nat.succ y + z
case succ
α : Type ?u.25506
σ : Stream' α
z✝ x y : ℕ
ih : ∀ {z : ℕ}, (fun x_1 => x_1 + x)^[y] z = x * y + z
z : ℕ
⊢ x * y + (z + x) = x * (y + 1) + z