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

State before:
ι✝ : Type
α : Type u_1
a b s✝ : Stream ι✝ α
inst✝¹ : Preorder ι✝
ι : Type
inst✝ : PartialOrder ι
s : Stream ι α
i : ι
q : { q // s.valid q = true }
h : toOrder s q < (i, true)
⊢ ¬s.ready q = true ∨ s.index q ≠ i
Tactic:
simp only [toOrder, Prod.Lex.lt_iff', lt_true_iff] at h
State after:
ι✝ : Type
α : Type u_1
a b s✝ : Stream ι✝ α
inst✝¹ : Preorder ι✝
ι : Type
inst✝ : PartialOrder ι
s : Stream ι α
i : ι
q : { q // s.valid q = true }
h : s.index q < i ∨ s.index q = i ∧ s.ready q = false
⊢ ¬s.ready q = true ∨ s.index q ≠ i

State before:
ι✝ : Type
α : Type u_1
a b s✝ : Stream ι✝ α
inst✝¹ : Preorder ι✝
ι : Type
inst✝ : PartialOrder ι
s : Stream ι α
i : ι
q : { q // s.valid q = true }
h : s.index q < i ∨ s.index q = i ∧ s.ready q = false
⊢ ¬s.ready q = true ∨ s.index q ≠ i
Tactic:
exact h.symm.imp (by simp) ne_of_lt
State after:
no goals

State before:
ι✝ : Type
α : Type u_1
a b s✝ : Stream ι✝ α
inst✝¹ : Preorder ι✝
ι : Type
inst✝ : PartialOrder ι
s : Stream ι α
i : ι
q : { q // s.valid q = true }
h : s.index q < i ∨ s.index q = i ∧ s.ready q = false
⊢ s.index q = i ∧ s.ready q = false → ¬s.ready q = true
Tactic:
simp
State after:
no goals