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

State before:
α : Type ?u.15
σ : Stream' α
α✝ : Type u_1
f : α✝ → α✝
a : α✝
i : ℕ
⊢ iterate f a i = f^[i] a
Tactic:
induction' i with i ih
State after:
case zero
α : Type ?u.15
σ : Stream' α
α✝ : Type u_1
f : α✝ → α✝
a : α✝
⊢ iterate f a Nat.zero = f^[Nat.zero] a

case succ
α : Type ?u.15
σ : Stream' α
α✝ : Type u_1
f : α✝ → α✝
a : α✝
i : ℕ
ih : iterate f a i = f^[i] a
⊢ iterate f a (Nat.succ i) = f^[Nat.succ i] a

State before:
case zero
α : Type ?u.15
σ : Stream' α
α✝ : Type u_1
f : α✝ → α✝
a : α✝
⊢ iterate f a Nat.zero = f^[Nat.zero] a
Tactic:
rfl
State after:
no goals

State before:
case succ
α : Type ?u.15
σ : Stream' α
α✝ : Type u_1
f : α✝ → α✝
a : α✝
i : ℕ
ih : iterate f a i = f^[i] a
⊢ iterate f a (Nat.succ i) = f^[Nat.succ i] a
Tactic:
unfold iterate Nat.iterate
State after:
case succ
α : Type ?u.15
σ : Stream' α
α✝ : Type u_1
f : α✝ → α✝
a : α✝
i : ℕ
ih : iterate f a i = f^[i] a
⊢ f (iterate f a i) = f^[i] (f a)

State before:
case succ
α : Type ?u.15
σ : Stream' α
α✝ : Type u_1
f : α✝ → α✝
a : α✝
i : ℕ
ih : iterate f a i = f^[i] a
⊢ f (iterate f a i) = f^[i] (f a)
Tactic:
rw [ih, Function.Commute.iterate_self]
State after:
no goals