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

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : s.σ
i : ι
⊢ (evalMultiset s q) i = Option.getD (Option.map (fun x => {x}) (evalOption s q i)) 0
Tactic:
cases h : s.evalOption q i <;>
simpa [(hs.evalOption_eq_iff (q := q)).1, (hs.evalOption_eq_iff (q := q)).2] using h
State after:
no goals