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

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

State before:
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
hs : IsStrictMono s
q : { q // s.valid q = true }
hr : s.ready q = true
⊢ index' s ↑q ≠ index' s (s.seek q (toOrder s q))
Tactic:
exact hs.2 q _ rfl.le hr
State after:
no goals