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

State before:
α : Type u_1
σ✝ σ : Stream' α
⊢ dropEveryNth 2 σ = fun i => σ (i * 2)
Tactic:
rw [dropEveryNth_two_eq_even, even_eq_mul_two]
State after:
no goals