Theorem: Etch.Verification.Stream.zip_seek_spec (Etch/StreamFusion/Proofs/StreamZip.lean)

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (zip a b).valid q = true }
i : StreamOrder ι
j : ι
h : i ≤ (j, false)
⊢ (evalMultiset (zip a b) ((zip a b).seek q i)) j = (evalMultiset (zip a b) ↑q) j
Tactic:
simp only [zip_spec', evalOption, zip_seek]
State after:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (zip a b).valid q = true }
i : StreamOrder ι
j : ι
h : i ≤ (j, false)
⊢ Option.getD
      (Option.map (fun x => {x})
        (Option.map₂ Prod.mk (Multiset.get ((evalMultiset a (a.seek (mul.valid.fst q) i)) j))
          (Multiset.get ((evalMultiset b (b.seek (mul.valid.snd q) i)) j))))
      0 =
    Option.getD
      (Option.map (fun x => {x})
        (Option.map₂ Prod.mk (Multiset.get ((evalMultiset a (↑q).1) j)) (Multiset.get ((evalMultiset b (↑q).2) j))))
      0

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (zip a b).valid q = true }
i : StreamOrder ι
j : ι
h : i ≤ (j, false)
⊢ Option.getD
      (Option.map (fun x => {x})
        (Option.map₂ Prod.mk (Multiset.get ((evalMultiset a (a.seek (mul.valid.fst q) i)) j))
          (Multiset.get ((evalMultiset b (b.seek (mul.valid.snd q) i)) j))))
      0 =
    Option.getD
      (Option.map (fun x => {x})
        (Option.map₂ Prod.mk (Multiset.get ((evalMultiset a (↑q).1) j)) (Multiset.get ((evalMultiset b (↑q).2) j))))
      0
Tactic:
congr 4 <;>
  apply IsLawful.seek_spec _ _ _ h
State after:
no goals