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

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
⊢ ∀ (i : ι), (eval s q) i ≠ 0 → index' s q ≤ ↑i
Tactic:
simp only [← Finsupp.mem_support_iff]
State after:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
⊢ ∀ i ∈ (eval s q).support, index' s q ≤ ↑i

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
⊢ ∀ i ∈ (eval s q).support, index' s q ≤ ↑i
Tactic:
apply s.wf.induction q
State after:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ), WfRel s y x → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i) → ∀ i ∈ (eval s x).support, index' s x ≤ ↑i

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ), WfRel s y x → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i) → ∀ i ∈ (eval s x).support, index' s x ≤ ↑i
Tactic:
clear q
State after:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ), WfRel s y x → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i) → ∀ i ∈ (eval s x).support, index' s x ≤ ↑i

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ), WfRel s y x → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i) → ∀ i ∈ (eval s x).support, index' s x ≤ ↑i
Tactic:
intro q ih i hi
State after:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
hi : i ∈ (eval s q).support
⊢ index' s q ≤ ↑i

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
hi : i ∈ (eval s q).support
⊢ index' s q ≤ ↑i
Tactic:
by_cases H : s.valid q
State after:
case pos
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
hi : i ∈ (eval s q).support
H : s.valid q = true
⊢ index' s q ≤ ↑i

case neg
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
hi : i ∈ (eval s q).support
H : ¬s.valid q = true
⊢ index' s q ≤ ↑i

State before:
case pos
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
hi : i ∈ (eval s q).support
H : s.valid q = true
⊢ index' s q ≤ ↑i

case neg
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
hi : i ∈ (eval s q).support
H : ¬s.valid q = true
⊢ index' s q ≤ ↑i
Tactic:
swap
State after:
case neg
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
hi : i ∈ (eval s q).support
H : ¬s.valid q = true
⊢ index' s q ≤ ↑i

case pos
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
hi : i ∈ (eval s q).support
H : s.valid q = true
⊢ index' s q ≤ ↑i

State before:
case neg
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
hi : i ∈ (eval s q).support
H : ¬s.valid q = true
⊢ index' s q ≤ ↑i
Tactic:
simp [H] at hi
State after:
no goals

State before:
case pos
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
hi : i ∈ (eval s q).support
H : s.valid q = true
⊢ index' s q ≤ ↑i
Tactic:
rw [s.eval_valid ⟨_, H⟩] at hi
State after:
case pos
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
H : s.valid q = true
hi : i ∈ (eval₀ s { val := q, property := H } + eval s (advance s ↑{ val := q, property := H })).support
⊢ index' s q ≤ ↑i

State before:
case pos
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
H : s.valid q = true
hi : i ∈ (eval₀ s { val := q, property := H } + eval s (advance s ↑{ val := q, property := H })).support
⊢ index' s q ≤ ↑i
Tactic:
rcases Finset.mem_union.mp (Finsupp.support_add hi) with hi | hi
State after:
case pos.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
H : s.valid q = true
hi✝ : i ∈ (eval₀ s { val := q, property := H } + eval s (advance s ↑{ val := q, property := H })).support
hi : i ∈ (eval₀ s { val := q, property := H }).support
⊢ index' s q ≤ ↑i

case pos.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
H : s.valid q = true
hi✝ : i ∈ (eval₀ s { val := q, property := H } + eval s (advance s ↑{ val := q, property := H })).support
hi : i ∈ (eval s (advance s ↑{ val := q, property := H })).support
⊢ index' s q ≤ ↑i

State before:
case pos.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
H : s.valid q = true
hi✝ : i ∈ (eval₀ s { val := q, property := H } + eval s (advance s ↑{ val := q, property := H })).support
hi : i ∈ (eval₀ s { val := q, property := H }).support
⊢ index' s q ≤ ↑i
Tactic:
rw [Finset.mem_singleton.mp (s.eval₀_support ⟨_, H⟩ hi)]
State after:
case pos.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
H : s.valid q = true
hi✝ : i ∈ (eval₀ s { val := q, property := H } + eval s (advance s ↑{ val := q, property := H })).support
hi : i ∈ (eval₀ s { val := q, property := H }).support
⊢ index' s q ≤ ↑(s.index { val := q, property := H })

State before:
case pos.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
H : s.valid q = true
hi✝ : i ∈ (eval₀ s { val := q, property := H } + eval s (advance s ↑{ val := q, property := H })).support
hi : i ∈ (eval₀ s { val := q, property := H }).support
⊢ index' s q ≤ ↑(s.index { val := q, property := H })
Tactic:
exact le_of_eq (Stream.index'_val' _ _)
State after:
no goals

State before:
case pos.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
H : s.valid q = true
hi✝ : i ∈ (eval₀ s { val := q, property := H } + eval s (advance s ↑{ val := q, property := H })).support
hi : i ∈ (eval s (advance s ↑{ val := q, property := H })).support
⊢ index' s q ≤ ↑i
Tactic:
exact (hs.index_le_index_advance q).trans (ih (s.advance q) (s.next_wf ⟨q, H⟩) i hi)
State after:
no goals