Theorem: Stream'.iterate_add_eq_mul (ListPowersProblem/StreamLemmas.lean)

State before:
α : Type ?u.25506
σ : Stream' α
y z x : ℕ
⊢ (fun x_1 => x_1 + x)^[y] z = x * y + z
Tactic:
induction' y with y ih generalizing z
State after:
case zero
α : Type ?u.25506
σ : Stream' α
z✝ x z : ℕ
⊢ (fun x_1 => x_1 + x)^[Nat.zero] z = x * Nat.zero + z

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

State before:
case zero
α : Type ?u.25506
σ : Stream' α
z✝ x z : ℕ
⊢ (fun x_1 => x_1 + x)^[Nat.zero] z = x * Nat.zero + z
Tactic:
simp only [Nat.zero_eq, Function.iterate_zero, id_eq, mul_zero, zero_add]
State after:
no goals

State before:
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
Tactic:
simp only [Function.iterate_succ, Function.comp_apply, ih, ←Nat.add_one]
State after:
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

State before:
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
Tactic:
ring_nf
State after:
no goals