Theorem: Etch.Verification.Stream.eval₀_map (Etch/StreamFusion/Proofs/StreamProof.lean)

State before:
ι : Type
α : Type u_2
a b s : Stream ι α
β : Type u_1
q : { q // s.valid q = true }
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
hf : f 0 = 0
⊢ eval₀ (map f s) q = Finsupp.mapRange f hf (eval₀ s q)
Tactic:
dsimp [Stream.eval₀]
State after:
ι : Type
α : Type u_2
a b s : Stream ι α
β : Type u_1
q : { q // s.valid q = true }
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
hf : f 0 = 0
⊢ (if h₂ : s.ready q = true then fun₀ | s.index q => f (s.value { val := q, property := h₂ }) else 0) =
    Finsupp.mapRange f hf
      (if h₂ : s.ready q = true then fun₀ | s.index q => s.value { val := q, property := h₂ } else 0)

State before:
ι : Type
α : Type u_2
a b s : Stream ι α
β : Type u_1
q : { q // s.valid q = true }
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
hf : f 0 = 0
⊢ (if h₂ : s.ready q = true then fun₀ | s.index q => f (s.value { val := q, property := h₂ }) else 0) =
    Finsupp.mapRange f hf
      (if h₂ : s.ready q = true then fun₀ | s.index q => s.value { val := q, property := h₂ } else 0)
Tactic:
split_ifs <;> simp
State after:
no goals