Theorem: Etch.Verification.Stream.IsStrictMono.eval_seek_eq_zero (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 ι
j : ι
h₁ : (j, false) < i
h₂ : i ≤ toOrder s q
⊢ (eval s (s.seek q i)) j = 0
Tactic:
rcases eq_or_lt_of_le h₂ with h₂ | h₂
State after:
case inl
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
j : ι
h₁ : (j, false) < i
h₂✝ : i ≤ toOrder s q
h₂ : i = toOrder s q
⊢ (eval s (s.seek q i)) j = 0

case inr
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
j : ι
h₁ : (j, false) < i
h₂✝ : i ≤ toOrder s q
h₂ : i < toOrder s q
⊢ (eval s (s.seek q i)) j = 0

State before:
case inl
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
j : ι
h₁ : (j, false) < i
h₂✝ : i ≤ toOrder s q
h₂ : i = toOrder s q
⊢ (eval s (s.seek q i)) j = 0
Tactic:
refine hs.eq_zero_of_lt_index _ h₂.symm.le _ ?_
State after:
case inl
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
j : ι
h₁ : (j, false) < i
h₂✝ : i ≤ toOrder s q
h₂ : i = toOrder s q
⊢ (j, false) < toOrder s q

State before:
case inl
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
j : ι
h₁ : (j, false) < i
h₂✝ : i ≤ toOrder s q
h₂ : i = toOrder s q
⊢ (j, false) < toOrder s q
Tactic:
rwa [← h₂]
State after:
no goals

State before:
case inr
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
j : ι
h₁ : (j, false) < i
h₂✝ : i ≤ toOrder s q
h₂ : i < toOrder s q
⊢ (eval s (s.seek q i)) j = 0
Tactic:
apply hs.1.eq_zero_of_lt_index
State after:
case inr.a
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
j : ι
h₁ : (j, false) < i
h₂✝ : i ≤ toOrder s q
h₂ : i < toOrder s q
⊢ ↑j < index' s (s.seek q i)

State before:
case inr.a
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
j : ι
h₁ : (j, false) < i
h₂✝ : i ≤ toOrder s q
h₂ : i < toOrder s q
⊢ ↑j < index' s (s.seek q i)
Tactic:
refine lt_of_lt_of_le ?_ (hs.1 _ _)
State after:
case inr.a
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
j : ι
h₁ : (j, false) < i
h₂✝ : i ≤ toOrder s q
h₂ : i < toOrder s q
⊢ ↑j < index' s ↑q

State before:
case inr.a
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
j : ι
h₁ : (j, false) < i
h₂✝ : i ≤ toOrder s q
h₂ : i < toOrder s q
⊢ ↑j < index' s ↑q
Tactic:
simpa using fst_lt_of_lt_of_lt h₁ h₂
State after:
no goals