Theorem: Etch.Verification.Stream.mul.ready.order_eq (Etch/StreamFusion/Proofs/StreamMul.lean)

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

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