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

State before:
case right
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { q // (zip a b).valid q = true }
hi : toOrder (zip a b) q ≤ (i, false)
⊢ evalOption b (advance (zip a b) ↑q).2 i = evalOption b (↑(mul.valid.snd q)) i
Tactic:
simp only [zip_σ, zip_valid, advance_val, zip_seek, evalOption, coe_mul_valid_fst, coe_mul_valid_snd, mul.valid]
State after:
case right
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { q // (zip a b).valid q = true }
hi : toOrder (zip a b) q ≤ (i, false)
⊢ Multiset.get ((evalMultiset b (b.seek (mul.valid.snd q) (toOrder (zip a b) q))) i) =
    Multiset.get ((evalMultiset b (↑q).2) i)

State before:
case right
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { q // (zip a b).valid q = true }
hi : toOrder (zip a b) q ≤ (i, false)
⊢ Multiset.get ((evalMultiset b (b.seek (mul.valid.snd q) (toOrder (zip a b) q))) i) =
    Multiset.get ((evalMultiset b (↑q).2) i)
Tactic:
rw [IsLawful.seek_spec _ _ _ hi]
State after:
case right
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { q // (zip a b).valid q = true }
hi : toOrder (zip a b) q ≤ (i, false)
⊢ Multiset.get ((evalMultiset b ↑(mul.valid.snd q)) i) = Multiset.get ((evalMultiset b (↑q).2) i)

State before:
case right
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { q // (zip a b).valid q = true }
hi : toOrder (zip a b) q ≤ (i, false)
⊢ Multiset.get ((evalMultiset b ↑(mul.valid.snd q)) i) = Multiset.get ((evalMultiset b (↑q).2) i)
Tactic:
rfl
State after:
no goals