Theorem: Etch.Verification.Stream.order_eq_of_mul_ready (Etch/StreamFusion/Proofs/StreamMul.lean)

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { p // mul.valid a b p = true }
h : mul.ready a b q = true
⊢ toOrder a (mul.valid.fst q) = toOrder (mul a b) q ∧ toOrder b (mul.valid.snd q) = toOrder (mul a b) q
Tactic:
dsimp only [Stream.toOrder]
State after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a 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)) = ((mul a b).index q, (mul a b).ready q) ∧
    (b.index (mul.valid.snd q), b.ready (mul.valid.snd q)) = ((mul a b).index q, (mul a b).ready q)

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a 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)) = ((mul a b).index q, (mul a b).ready q) ∧
    (b.index (mul.valid.snd q), b.ready (mul.valid.snd q)) = ((mul a b).index q, (mul a b).ready q)
Tactic:
aesop
State after:
no goals