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

State before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : s.valid q = true
⊢ WfRel s (seek' s q i) q ∨ coeLex i < toOrder' s q ∧ seek' s q i = q
Tactic:
rw [← wf_valid_iff (q := ⟨q, hq⟩)]
State after:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : s.valid q = true
⊢ WfRel s (s.seek { val := q, property := hq } i) ↑{ val := q, property := hq } ∨
    i < toOrder s { val := q, property := hq } ∧ s.seek { val := q, property := hq } i = ↑{ val := q, property := hq }

State before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : s.valid q = true
⊢ WfRel s (s.seek { val := q, property := hq } i) ↑{ val := q, property := hq } ∨
    i < toOrder s { val := q, property := hq } ∧ s.seek { val := q, property := hq } i = ↑{ val := q, property := hq }
Tactic:
exact s.wf_valid ⟨q, hq⟩ i
State after:
no goals

State before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : ¬s.valid q = true
⊢ WfRel s (seek' s q i) q ∨ coeLex i < toOrder' s q ∧ seek' s q i = q
Tactic:
right
State after:
case h
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : ¬s.valid q = true
⊢ coeLex i < toOrder' s q ∧ seek' s q i = q

State before:
case h
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : ¬s.valid q = true
⊢ coeLex i < toOrder' s q ∧ seek' s q i = q
Tactic:
constructor
State after:
case h.left
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : ¬s.valid q = true
⊢ coeLex i < toOrder' s q

case h.right
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : ¬s.valid q = true
⊢ seek' s q i = q

State before:
case h.left
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : ¬s.valid q = true
⊢ coeLex i < toOrder' s q
Tactic:
rw [Prod.Lex.lt_iff']
State after:
case h.left
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : ¬s.valid q = true
⊢ (coeLex i).1 < (toOrder' s q).1 ∨ (coeLex i).1 = (toOrder' s q).1 ∧ (coeLex i).2 < (toOrder' s q).2

State before:
case h.left
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : ¬s.valid q = true
⊢ (coeLex i).1 < (toOrder' s q).1 ∨ (coeLex i).1 = (toOrder' s q).1 ∧ (coeLex i).2 < (toOrder' s q).2
Tactic:
left
State after:
case h.left.h
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : ¬s.valid q = true
⊢ (coeLex i).1 < (toOrder' s q).1

State before:
case h.left.h
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : ¬s.valid q = true
⊢ (coeLex i).1 < (toOrder' s q).1
Tactic:
simp [hq]
State after:
no goals

State before:
case h.right
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : ¬s.valid q = true
⊢ seek' s q i = q
Tactic:
simp [hq]
State after:
no goals