Theorem: Etch.Verification.Stream.IsStrictMono.eval₀_eq_eval_filter (Etch/StreamFusion/Proofs/StreamProof.lean)

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
⊢ eval₀ s q = Finsupp.filter (fun i => (i, false) < toOrder s q) (eval s ↑q)
Tactic:
rw [s.eval_valid, Finsupp.filter_add]
State after:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
⊢ eval₀ s q =
    Finsupp.filter (fun i => (i, false) < toOrder s q) (eval₀ s q) +
      Finsupp.filter (fun i => (i, false) < toOrder s q) (eval s (advance s ↑q))

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
⊢ eval₀ s q =
    Finsupp.filter (fun i => (i, false) < toOrder s q) (eval₀ s q) +
      Finsupp.filter (fun i => (i, false) < toOrder s q) (eval s (advance s ↑q))
Tactic:
convert (add_zero (M := ι →₀ α) _).symm
State after:
case h.e'_3.h.e'_5
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
⊢ Finsupp.filter (fun i => (i, false) < toOrder s q) (eval₀ s q) = eval₀ s q

case h.e'_3.h.e'_6
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
⊢ Finsupp.filter (fun i => (i, false) < toOrder s q) (eval s (advance s ↑q)) = 0

State before:
case h.e'_3.h.e'_5
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
⊢ Finsupp.filter (fun i => (i, false) < toOrder s q) (eval₀ s q) = eval₀ s q
Tactic:
rw [Finsupp.filter_eq_self_iff]
State after:
case h.e'_3.h.e'_5
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
⊢ ∀ (x : ι), (eval₀ s q) x ≠ 0 → (x, false) < toOrder s q

State before:
case h.e'_3.h.e'_5
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
⊢ ∀ (x : ι), (eval₀ s q) x ≠ 0 → (x, false) < toOrder s q
Tactic:
intro i hi
State after:
case h.e'_3.h.e'_5
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : ι
hi : (eval₀ s q) i ≠ 0
⊢ (i, false) < toOrder s q

State before:
case h.e'_3.h.e'_5
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : ι
hi : (eval₀ s q) i ≠ 0
⊢ (i, false) < toOrder s q
Tactic:
rw [s.eval₀_support' q hi]
State after:
case h.e'_3.h.e'_5
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : ι
hi : (eval₀ s q) i ≠ 0
⊢ (i, false) < (i, true)

State before:
case h.e'_3.h.e'_5
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : ι
hi : (eval₀ s q) i ≠ 0
⊢ (i, false) < (i, true)
Tactic:
simp
State after:
no goals

State before:
case h.e'_3.h.e'_6
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
⊢ Finsupp.filter (fun i => (i, false) < toOrder s q) (eval s (advance s ↑q)) = 0
Tactic:
rw [Finsupp.filter_eq_zero_iff]
State after:
case h.e'_3.h.e'_6
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
⊢ ∀ (x : ι), (x, false) < toOrder s q → (eval s (advance s ↑q)) x = 0

State before:
case h.e'_3.h.e'_6
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
⊢ ∀ (x : ι), (x, false) < toOrder s q → (eval s (advance s ↑q)) x = 0
Tactic:
intro i hi
State after:
case h.e'_3.h.e'_6
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : ι
hi : (i, false) < toOrder s q
⊢ (eval s (advance s ↑q)) i = 0

State before:
case h.e'_3.h.e'_6
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : ι
hi : (i, false) < toOrder s q
⊢ (eval s (advance s ↑q)) i = 0
Tactic:
rw [Stream.advance_val]
State after:
case h.e'_3.h.e'_6
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : ι
hi : (i, false) < toOrder s q
⊢ (eval s (s.seek q (toOrder s q))) i = 0

State before:
case h.e'_3.h.e'_6
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : ι
hi : (i, false) < toOrder s q
⊢ (eval s (s.seek q (toOrder s q))) i = 0
Tactic:
exact hs.eq_zero_of_lt_index q rfl.le i hi
State after:
no goals