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

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
j : ι
hj : (eval s (s.seek q i)) j ≠ 0
⊢ coeLex (toOrder s q) ≤ coeLex (j, false)
Tactic:
rw [← Stream.coeLex_toOrder]
State after:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
j : ι
hj : (eval s (s.seek q i)) j ≠ 0
⊢ toOrder' s ↑q ≤ coeLex (j, false)

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
j : ι
hj : (eval s (s.seek q i)) j ≠ 0
⊢ toOrder' s ↑q ≤ coeLex (j, false)
Tactic:
refine (hs.spec q hi).trans ?_
State after:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
j : ι
hj : (eval s (s.seek q i)) j ≠ 0
⊢ (index' s (s.seek q i), false) ≤ coeLex (j, false)

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
j : ι
hj : (eval s (s.seek q i)) j ≠ 0
⊢ (index' s (s.seek q i), false) ≤ coeLex (j, false)
Tactic:
simpa using hs.1.index_le_of_mem_support j hj
State after:
no goals