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

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { x // (zip a b).valid x = true }
hi : i < (zip a b).index q
⊢ evalOption (zip a b) (↑q) i = none
Tactic:
have := (zip_strict_mono a.strictMono b.strictMono).1.eq_empty_of_lt_index (q := q) i (by rwa [index'_val, WithTop.coe_lt_coe])
State after:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { x // (zip a b).valid x = true }
hi : i < (zip a b).index q
this : (evalMultiset (zip a b) ↑q) i = 0
⊢ evalOption (zip a b) (↑q) i = none

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { x // (zip a b).valid x = true }
hi : i < (zip a b).index q
this : (evalMultiset (zip a b) ↑q) i = 0
⊢ evalOption (zip a b) (↑q) i = none
Tactic:
rw [Stream.evalOption, this, Multiset.get_zero]
State after:
no goals

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { x // (zip a b).valid x = true }
hi : i < (zip a b).index q
⊢ ↑i < index' (zip a b) ↑q
Tactic:
rwa [index'_val, WithTop.coe_lt_coe]
State after:
no goals