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

State before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : Zero α
s : Stream ι α
inst✝ : IsBounded s
x : { q // s.valid q = true }
⊢ (eval₀ s x).support ⊆ {s.index x}
Tactic:
rw [Stream.eval₀]
State after:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : Zero α
s : Stream ι α
inst✝ : IsBounded s
x : { q // s.valid q = true }
⊢ (if h₂ : s.ready x = true then fun₀ | s.index x => s.value { val := x, property := h₂ } else 0).support ⊆ {s.index x}

State before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : Zero α
s : Stream ι α
inst✝ : IsBounded s
x : { q // s.valid q = true }
⊢ (if h₂ : s.ready x = true then fun₀ | s.index x => s.value { val := x, property := h₂ } else 0).support ⊆ {s.index x}
Tactic:
split_ifs
State after:
case pos
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : Zero α
s : Stream ι α
inst✝ : IsBounded s
x : { q // s.valid q = true }
h✝ : s.ready x = true
⊢ (fun₀ | s.index x => s.value { val := x, property := h✝ }).support ⊆ {s.index x}

case neg
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : Zero α
s : Stream ι α
inst✝ : IsBounded s
x : { q // s.valid q = true }
h✝ : ¬s.ready x = true
⊢ 0.support ⊆ {s.index x}

State before:
case pos
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : Zero α
s : Stream ι α
inst✝ : IsBounded s
x : { q // s.valid q = true }
h✝ : s.ready x = true
⊢ (fun₀ | s.index x => s.value { val := x, property := h✝ }).support ⊆ {s.index x}
Tactic:
exact Finsupp.support_single_subset
State after:
no goals

State before:
case neg
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : Zero α
s : Stream ι α
inst✝ : IsBounded s
x : { q // s.valid q = true }
h✝ : ¬s.ready x = true
⊢ 0.support ⊆ {s.index x}
Tactic:
simp
State after:
no goals