Theorem: Etch.Verification.Stream.eval_map_apply (Etch/StreamFusion/Proofs/StreamProof.lean)

State before:
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
⊢ (eval (map (⇑f) s) q) i = f ((eval s q) i)
Tactic:
rw [Stream.eval_map, Finsupp.mapRange.addMonoidHom_apply, Finsupp.mapRange_apply]
State after:
no goals