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

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
⊢ evalMultiset s (s.seek q i) = evalMultiset s ↑q
Tactic:
ext j
State after:
case h
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
j : ι
⊢ (evalMultiset s (s.seek q i)) j = (evalMultiset s ↑q) j

State before:
case h
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
j : ι
⊢ (evalMultiset s (s.seek q i)) j = (evalMultiset s ↑q) j
Tactic:
by_cases H : s.toOrder q ≤ (j, true)
State after:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
j : ι
H : toOrder s q ≤ (j, true)
⊢ (evalMultiset s (s.seek q i)) j = (evalMultiset s ↑q) j

case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
j : ι
H : ¬toOrder s q ≤ (j, true)
⊢ (evalMultiset s (s.seek q i)) j = (evalMultiset s ↑q) j

State before:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
j : ι
H : ¬toOrder s q ≤ (j, true)
⊢ (evalMultiset s (s.seek q i)) j = (evalMultiset s ↑q) j
Tactic:
have : ↑j < s.index' q := by
  simpa using fst_lt_of_lt_of_lt (show (j, false) <ₗ (j, true) by simp) (not_le.mp H)
State after:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
j : ι
H : ¬toOrder s q ≤ (j, true)
this : ↑j < index' s ↑q
⊢ (evalMultiset s (s.seek q i)) j = (evalMultiset s ↑q) j

State before:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
j : ι
H : ¬toOrder s q ≤ (j, true)
this : ↑j < index' s ↑q
⊢ (evalMultiset s (s.seek q i)) j = (evalMultiset s ↑q) j
Tactic:
rw [s.mono.eq_empty_of_lt_index j this,
  s.mono.eq_empty_of_lt_index _ (this.trans_le (s.mono q i))]
State after:
no goals

State before:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
j : ι
H : toOrder s q ≤ (j, true)
⊢ (evalMultiset s (s.seek q i)) j = (evalMultiset s ↑q) j
Tactic:
rw [IsLawful.seek_spec q]
State after:
case pos.a
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
j : ι
H : toOrder s q ≤ (j, true)
⊢ i ≤ (j, false)

State before:
case pos.a
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
j : ι
H : toOrder s q ≤ (j, true)
⊢ i ≤ (j, false)
Tactic:
simpa [Prod.Lex.lt_iff'', Prod.Lex.le_iff''] using lt_of_lt_of_le hi H
State after:
no goals

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
j : ι
H : ¬toOrder s q ≤ (j, true)
⊢ ↑j < index' s ↑q
Tactic:
simpa using fst_lt_of_lt_of_lt (show (j, false) <ₗ (j, true) by simp) (not_le.mp H)
State after:
no goals

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
j : ι
H : ¬toOrder s q ≤ (j, true)
⊢ (j, false) < (j, true)
Tactic:
simp
State after:
no goals