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

State before:
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h : IsMonotonic s
q : s.σ
⊢ index' s q ≤ index' s (advance s q)
Tactic:
by_cases H : s.valid q
State after:
case pos
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h : IsMonotonic s
q : s.σ
H : s.valid q = true
⊢ index' s q ≤ index' s (advance s q)

case neg
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h : IsMonotonic s
q : s.σ
H : ¬s.valid q = true
⊢ index' s q ≤ index' s (advance s q)

State before:
case pos
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h : IsMonotonic s
q : s.σ
H : s.valid q = true
⊢ index' s q ≤ index' s (advance s q)

case neg
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h : IsMonotonic s
q : s.σ
H : ¬s.valid q = true
⊢ index' s q ≤ index' s (advance s q)
Tactic:
swap
State after:
case neg
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h : IsMonotonic s
q : s.σ
H : ¬s.valid q = true
⊢ index' s q ≤ index' s (advance s q)

case pos
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h : IsMonotonic s
q : s.σ
H : s.valid q = true
⊢ index' s q ≤ index' s (advance s q)

State before:
case neg
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h : IsMonotonic s
q : s.σ
H : ¬s.valid q = true
⊢ index' s q ≤ index' s (advance s q)
Tactic:
simp [H]
State after:
no goals

State before:
case pos
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h : IsMonotonic s
q : s.σ
H : s.valid q = true
⊢ index' s q ≤ index' s (advance s q)
Tactic:
simp only [Stream.advance, H, dif_pos]
State after:
case pos
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h : IsMonotonic s
q : s.σ
H : s.valid q = true
⊢ index' s q ≤ index' s (s.seek { val := q, property := ⋯ } (toOrder s { val := q, property := ⋯ }))

State before:
case pos
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h : IsMonotonic s
q : s.σ
H : s.valid q = true
⊢ index' s q ≤ index' s (s.seek { val := q, property := ⋯ } (toOrder s { val := q, property := ⋯ }))
Tactic:
apply h
State after:
no goals