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

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
⊢ evalMultiset s (s.seek q (s.index q, false)) = evalMultiset s ↑q
Tactic:
by_cases hr : s.ready q
State after:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
hr : s.ready q = true
⊢ evalMultiset s (s.seek q (s.index q, false)) = evalMultiset s ↑q

case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
hr : ¬s.ready q = true
⊢ evalMultiset s (s.seek q (s.index q, false)) = evalMultiset s ↑q

State before:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
hr : ¬s.ready q = true
⊢ evalMultiset s (s.seek q (s.index q, false)) = evalMultiset s ↑q
Tactic:
. ext i
  simp [s.evalMultiset_not_ready q i (.inl hr), Stream.toOrder, hr]
State after:
no goals

State before:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
hr : s.ready q = true
⊢ evalMultiset s (s.seek q (s.index q, false)) = evalMultiset s ↑q
Tactic:
apply Stream.seek_lt_toOrder
State after:
case pos.hi
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
hr : s.ready q = true
⊢ (s.index q, false) < toOrder s q

State before:
case pos.hi
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
hr : s.ready q = true
⊢ (s.index q, false) < toOrder s q
Tactic:
simp [Stream.toOrder, hr]
State after:
no goals

State before:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
hr : ¬s.ready q = true
⊢ evalMultiset s (s.seek q (s.index q, false)) = evalMultiset s ↑q
Tactic:
ext i
State after:
case neg.h
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
hr : ¬s.ready q = true
i : ι
⊢ (evalMultiset s (s.seek q (s.index q, false))) i = (evalMultiset s ↑q) i

State before:
case neg.h
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
hr : ¬s.ready q = true
i : ι
⊢ (evalMultiset s (s.seek q (s.index q, false))) i = (evalMultiset s ↑q) i
Tactic:
simp [s.evalMultiset_not_ready q i (.inl hr), Stream.toOrder, hr]
State after:
no goals