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

State before:
α : Type u_1
σ✝ σ : Stream' α
⊢ even σ = fun i => σ (i * 2)
Tactic:
funext i
State after:
case h
α : Type u_1
σ✝ σ : Stream' α
i : ℕ
⊢ even σ i = σ (i * 2)

State before:
case h
α : Type u_1
σ✝ σ : Stream' α
i : ℕ
⊢ even σ i = σ (i * 2)
Tactic:
simp [even, corec, map, head, nth, tail, iterate_stream_eq_index_iterate, iterate_add_eq_mul 2]
State after:
case h
α : Type u_1
σ✝ σ : Stream' α
i : ℕ
⊢ σ (2 * i) = σ (i * 2)

State before:
case h
α : Type u_1
σ✝ σ : Stream' α
i : ℕ
⊢ σ (2 * i) = σ (i * 2)
Tactic:
rw [Nat.mul_comm]
State after:
no goals