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

State before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
h : mul.ready a b q = true
⊢ toOrder a (mul.valid.fst q) = toOrder (zip a b) q ∧ toOrder b (mul.valid.snd q) = toOrder (zip a b) q
Tactic:
dsimp only [Stream.toOrder]
State after:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
h : mul.ready a b q = true
⊢ (a.index (mul.valid.fst q), a.ready (mul.valid.fst q)) = ((zip a b).index q, (zip a b).ready q) ∧
    (b.index (mul.valid.snd q), b.ready (mul.valid.snd q)) = ((zip a b).index q, (zip a b).ready q)

State before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
h : mul.ready a b q = true
⊢ (a.index (mul.valid.fst q), a.ready (mul.valid.fst q)) = ((zip a b).index q, (zip a b).ready q) ∧
    (b.index (mul.valid.snd q), b.ready (mul.valid.snd q)) = ((zip a b).index q, (zip a b).ready q)
Tactic:
aesop
State after:
no goals