Theorem: Etch.Verification.Stream.zip_ready_eq (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 : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
⊢ evalOption (zip a b) (↑q) ((zip a b).index q) =
    some (a.value (mul.ready.fst { val := q, property := h }), b.value (mul.ready.snd { val := q, property := h }))
Tactic:
rw [(zip_strict_mono a.strictMono b.strictMono).evalOption_ready h]
State after:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
⊢ some ((zip a b).value { val := q, property := h }) =
    some (a.value (mul.ready.fst { val := q, property := h }), b.value (mul.ready.snd { val := q, property := h }))

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
⊢ some ((zip a b).value { val := q, property := h }) =
    some (a.value (mul.ready.fst { val := q, property := h }), b.value (mul.ready.snd { val := q, property := h }))
Tactic:
rfl
State after:
no goals