Theorem: Etch.Verification.Stream.IsStrictMono.eq_zero_of_lt_index (Etch/StreamFusion/Proofs/StreamProof.lean)

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
j : ι
⊢ (j, false) < toOrder s q → (eval s (s.seek q i)) j = 0
Tactic:
contrapose
State after:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
j : ι
⊢ ¬(eval s (s.seek q i)) j = 0 → ¬(j, false) < toOrder s q

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
j : ι
⊢ ¬(eval s (s.seek q i)) j = 0 → ¬(j, false) < toOrder s q
Tactic:
simpa using hs.index_le_of_mem_support q hi j
State after:
no goals