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

State before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
q : s.σ
⊢ index' s q < ⊤ ↔ s.valid q = true
Tactic:
rw [Stream.index']
State after:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
q : s.σ
⊢ (if h : s.valid q = true then ↑(s.index { val := q, property := h }) else ⊤) < ⊤ ↔ s.valid q = true

State before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
q : s.σ
⊢ (if h : s.valid q = true then ↑(s.index { val := q, property := h }) else ⊤) < ⊤ ↔ s.valid q = true
Tactic:
split_ifs
State after:
case pos
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
q : s.σ
h✝ : s.valid q = true
⊢ ↑(s.index { val := q, property := h✝ }) < ⊤ ↔ s.valid q = true

case neg
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
q : s.σ
h✝ : ¬s.valid q = true
⊢ ⊤ < ⊤ ↔ s.valid q = true

State before:
case pos
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
q : s.σ
h✝ : s.valid q = true
⊢ ↑(s.index { val := q, property := h✝ }) < ⊤ ↔ s.valid q = true
Tactic:
simpa [WithTop.coe_lt_top]
State after:
no goals

State before:
case neg
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
q : s.σ
h✝ : ¬s.valid q = true
⊢ ⊤ < ⊤ ↔ s.valid q = true
Tactic:
simp [*]
State after:
no goals