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

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : ¬s.ready q = true ∨ s.index q ≠ i
⊢ evalOption s (↑q) i = evalOption s (advance s ↑q) i
Tactic:
simp only [Stream.evalOption]
State after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : ¬s.ready q = true ∨ s.index q ≠ i
⊢ Multiset.get ((evalMultiset s ↑q) i) = Multiset.get ((evalMultiset s (advance s ↑q)) i)

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : ¬s.ready q = true ∨ s.index q ≠ i
⊢ Multiset.get ((evalMultiset s ↑q) i) = Multiset.get ((evalMultiset s (advance s ↑q)) i)
Tactic:
rw [s.evalMultiset_not_ready q i hr]
State after:
no goals