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 }
i : ι
h₂ : (eval₀ s x) i ≠ 0
⊢ toOrder s x = (i, true)
Tactic:
obtain rfl := Finset.eq_of_mem_singleton (s.eval₀_support x (Finsupp.mem_support_iff.mpr h₂))
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 }
h₂ : (eval₀ s x) (s.index x) ≠ 0
⊢ toOrder s x = (s.index x, true)

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 }
h₂ : (eval₀ s x) (s.index x) ≠ 0
⊢ toOrder s x = (s.index x, true)
Tactic:
rw [Stream.eval₀] at h₂
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 }
h₂ : (if h₂ : s.ready x = true then fun₀ | s.index x => s.value { val := x, property := h₂ } else 0) (s.index x) ≠ 0
⊢ toOrder s x = (s.index x, true)

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 }
h₂ : (if h₂ : s.ready x = true then fun₀ | s.index x => s.value { val := x, property := h₂ } else 0) (s.index x) ≠ 0
⊢ toOrder s x = (s.index x, true)
Tactic:
split_ifs at h₂ with hr
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 }
hr : s.ready x = true
h₂ : (fun₀ | s.index x => s.value { val := x, property := hr }) (s.index x) ≠ 0
⊢ toOrder s x = (s.index x, true)

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 }
hr : ¬s.ready x = true
h₂ : 0 (s.index x) ≠ 0
⊢ toOrder s x = (s.index x, true)

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 }
hr : s.ready x = true
h₂ : (fun₀ | s.index x => s.value { val := x, property := hr }) (s.index x) ≠ 0
⊢ toOrder s x = (s.index x, true)
Tactic:
simp [Stream.toOrder, hr]
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 }
hr : ¬s.ready x = true
h₂ : 0 (s.index x) ≠ 0
⊢ toOrder s x = (s.index x, true)
Tactic:
simp at h₂
State after:
no goals