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

State before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : AddZeroClass α
⊢ eval 0 = 0
Tactic:
ext
State after:
case h.h
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : AddZeroClass α
x✝ : 0.σ
a✝ : ι
⊢ (eval 0 x✝) a✝ = (0 x✝) a✝

State before:
case h.h
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : AddZeroClass α
x✝ : 0.σ
a✝ : ι
⊢ (eval 0 x✝) a✝ = (0 x✝) a✝
Tactic:
rw [Stream.eval]
State after:
case h.h
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : AddZeroClass α
x✝ : 0.σ
a✝ : ι
⊢ (if h : 0.valid x✝ = true then
        let_fun this := ⋯;
        eval₀ 0 { val := x✝, property := h } + eval 0 (advance 0 x✝)
      else 0)
      a✝ =
    (0 x✝) a✝

State before:
case h.h
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : AddZeroClass α
x✝ : 0.σ
a✝ : ι
⊢ (if h : 0.valid x✝ = true then
        let_fun this := ⋯;
        eval₀ 0 { val := x✝, property := h } + eval 0 (advance 0 x✝)
      else 0)
      a✝ =
    (0 x✝) a✝
Tactic:
simp
State after:
no goals