Theorem: Etch.Verification.Stream.seek_spec (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 ι
⊢ Finsupp.filter (fun j => i ≤ (j, false)) (evalMultiset s (s.seek q i)) =
    Finsupp.filter (fun j => i ≤ (j, false)) (evalMultiset s ↑q)
Tactic:
rw [Finsupp.filter_ext_iff]
State after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
⊢ ∀ (a : ι), i ≤ (a, false) → (evalMultiset s (s.seek q i)) a = (evalMultiset s ↑q) a

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
⊢ ∀ (a : ι), i ≤ (a, false) → (evalMultiset s (s.seek q i)) a = (evalMultiset s ↑q) a
Tactic:
exact IsLawful.seek_spec q i
State after:
no goals