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

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
q : { q // s.valid q = true }
hr : s.ready q = true
⊢ (evalMultiset s (advance s ↑q)) (s.index q) = 0
Tactic:
apply h.1.eq_empty_of_lt_index
State after:
case a
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
q : { q // s.valid q = true }
hr : s.ready q = true
⊢ ↑(s.index q) < index' s (advance s ↑q)

State before:
case a
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
q : { q // s.valid q = true }
hr : s.ready q = true
⊢ ↑(s.index q) < index' s (advance s ↑q)
Tactic:
rw [advance_val]
State after:
case a
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
q : { q // s.valid q = true }
hr : s.ready q = true
⊢ ↑(s.index q) < index' s (s.seek q (toOrder s q))

State before:
case a
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
q : { q // s.valid q = true }
hr : s.ready q = true
⊢ ↑(s.index q) < index' s (s.seek q (toOrder s q))
Tactic:
exact h.lt' rfl.le hr
State after:
no goals