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

State before:
α : Type u_1
σ✝ : Stream' α
i j : ℕ
σ : Stream' α
f : ℕ → ℕ
⊢ iterate (fun s i => s (f i)) σ i j = σ (f^[i] j)
Tactic:
rw [iterate_eq_Nat_iterate]
State after:
α : Type u_1
σ✝ : Stream' α
i j : ℕ
σ : Stream' α
f : ℕ → ℕ
⊢ (fun s i => s (f i))^[i] σ j = σ (f^[i] j)

State before:
α : Type u_1
σ✝ : Stream' α
i j : ℕ
σ : Stream' α
f : ℕ → ℕ
⊢ (fun s i => s (f i))^[i] σ j = σ (f^[i] j)
Tactic:
induction' i with i ih generalizing σ
State after:
case zero
α : Type u_1
σ✝¹ : Stream' α
j : ℕ
σ✝ : Stream' α
f : ℕ → ℕ
σ : Stream' α
⊢ (fun s i => s (f i))^[Nat.zero] σ j = σ (f^[Nat.zero] j)

case succ
α : Type u_1
σ✝¹ : Stream' α
j : ℕ
σ✝ : Stream' α
f : ℕ → ℕ
i : ℕ
ih : ∀ (σ : Stream' α), (fun s i => s (f i))^[i] σ j = σ (f^[i] j)
σ : Stream' α
⊢ (fun s i => s (f i))^[Nat.succ i] σ j = σ (f^[Nat.succ i] j)

State before:
case zero
α : Type u_1
σ✝¹ : Stream' α
j : ℕ
σ✝ : Stream' α
f : ℕ → ℕ
σ : Stream' α
⊢ (fun s i => s (f i))^[Nat.zero] σ j = σ (f^[Nat.zero] j)
Tactic:
rfl
State after:
no goals

State before:
case succ
α : Type u_1
σ✝¹ : Stream' α
j : ℕ
σ✝ : Stream' α
f : ℕ → ℕ
i : ℕ
ih : ∀ (σ : Stream' α), (fun s i => s (f i))^[i] σ j = σ (f^[i] j)
σ : Stream' α
⊢ (fun s i => s (f i))^[Nat.succ i] σ j = σ (f^[Nat.succ i] j)
Tactic:
simp [ih]
State after:
case succ
α : Type u_1
σ✝¹ : Stream' α
j : ℕ
σ✝ : Stream' α
f : ℕ → ℕ
i : ℕ
ih : ∀ (σ : Stream' α), (fun s i => s (f i))^[i] σ j = σ (f^[i] j)
σ : Stream' α
⊢ σ (f (f^[i] j)) = σ (f^[i] (f j))

State before:
case succ
α : Type u_1
σ✝¹ : Stream' α
j : ℕ
σ✝ : Stream' α
f : ℕ → ℕ
i : ℕ
ih : ∀ (σ : Stream' α), (fun s i => s (f i))^[i] σ j = σ (f^[i] j)
σ : Stream' α
⊢ σ (f (f^[i] j)) = σ (f^[i] (f j))
Tactic:
congr
State after:
case succ.e_a
α : Type u_1
σ✝¹ : Stream' α
j : ℕ
σ✝ : Stream' α
f : ℕ → ℕ
i : ℕ
ih : ∀ (σ : Stream' α), (fun s i => s (f i))^[i] σ j = σ (f^[i] j)
σ : Stream' α
⊢ f (f^[i] j) = f^[i] (f j)

State before:
case succ.e_a
α : Type u_1
σ✝¹ : Stream' α
j : ℕ
σ✝ : Stream' α
f : ℕ → ℕ
i : ℕ
ih : ∀ (σ : Stream' α), (fun s i => s (f i))^[i] σ j = σ (f^[i] j)
σ : Stream' α
⊢ f (f^[i] j) = f^[i] (f j)
Tactic:
exact (Function.iterate_succ_apply' f i j).symm
State after:
no goals