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

State before:
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
⊢ (toOrder' s ↑q).1 ≤ (index' s (s.seek q i), false).1
Tactic:
simpa using hs.1 q i
State after:
no goals

State before:
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
⊢ (toOrder' s ↑q).1 = (index' s (s.seek q i), false).1 → (toOrder' s ↑q).2 ≤ (index' s (s.seek q i), false).2
Tactic:
simp
State after:
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
⊢ ↑(s.index q) = index' s (s.seek q i) → s.ready q = false

State before:
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
⊢ ↑(s.index q) = index' s (s.seek q i) → s.ready q = false
Tactic:
contrapose
State after:
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
⊢ ¬s.ready q = false → ¬↑(s.index q) = index' s (s.seek q i)

State before:
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
⊢ ¬s.ready q = false → ¬↑(s.index q) = index' s (s.seek q i)
Tactic:
simpa using hs.2 q i hi
State after:
no goals