Theorem: Etch.Verification.Stream.LawfulOfStream.get_fold (Etch/StreamFusion/Proofs/OfStream.lean)

State before:
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
⊢ ∀ (b : m),
    evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) q b) i) =
      evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) q) i
Tactic:
apply s.wf.induction q
State after:
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ),
        WfRel s y x →
          ∀ (b : m),
            evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
              evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i) →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) x b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) x) i

State before:
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ),
        WfRel s y x →
          ∀ (b : m),
            evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
              evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i) →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) x b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) x) i
Tactic:
clear q
State after:
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ),
        WfRel s y x →
          ∀ (b : m),
            evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
              evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i) →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) x b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) x) i

State before:
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ),
        WfRel s y x →
          ∀ (b : m),
            evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
              evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i) →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) x b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) x) i
Tactic:
intro q ih b
State after:
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
⊢ evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) q b) i) =
    evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) q) i

State before:
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
⊢ evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) q b) i) =
    evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) q) i
Tactic:
by_cases hv : s.valid q
State after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : s.valid q = true
⊢ evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) q b) i) =
    evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) q) i

case neg
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) q b) i) =
    evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) q) i

State before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : s.valid q = true
⊢ evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) q b) i) =
    evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) q) i
Tactic:
revert ih
State after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
b : m
hv : s.valid q = true
⊢ (∀ (y : s.σ),
      WfRel s y q →
        ∀ (b : m),
          evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
            evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i) →
    evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) q b) i) =
      evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) q) i

State before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
b : m
hv : s.valid q = true
⊢ (∀ (y : s.σ),
      WfRel s y q →
        ∀ (b : m),
          evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
            evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i) →
    evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) q b) i) =
      evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) q) i
Tactic:
refine Subtype.with_prop (fun t => s.valid t) q hv ?_
State after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
b : m
hv : s.valid q = true
⊢ ∀ (x : { t // s.valid t = true }),
    (∀ (y : s.σ),
        WfRel s y ↑x →
          ∀ (b : m),
            evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
              evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i) →
      evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) (↑x) b) i) =
        evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) ↑x) i

State before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
b : m
hv : s.valid q = true
⊢ ∀ (x : { t // s.valid t = true }),
    (∀ (y : s.σ),
        WfRel s y ↑x →
          ∀ (b : m),
            evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
              evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i) →
      evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) (↑x) b) i) =
        evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) ↑x) i
Tactic:
clear q hv
State after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
⊢ ∀ (x : { t // s.valid t = true }),
    (∀ (y : s.σ),
        WfRel s y ↑x →
          ∀ (b : m),
            evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
              evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i) →
      evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) (↑x) b) i) =
        evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) ↑x) i

State before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
⊢ ∀ (x : { t // s.valid t = true }),
    (∀ (y : s.σ),
        WfRel s y ↑x →
          ∀ (b : m),
            evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
              evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i) →
      evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) (↑x) b) i) =
        evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) ↑x) i
Tactic:
intro q ih
State after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) (↑q) b) i) =
    evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) ↑q) i

State before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) (↑q) b) i) =
    evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) ↑q) i
Tactic:
rw [Stream.fold_wf_spec, Stream.eval_valid, Stream.eval₀]
State after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ evalFinsupp
      (Readable.get
        (fold_wf Modifiable.update (map OfStream.eval s) (advance (map OfStream.eval s) ↑q)
          (if hr : (map OfStream.eval s).ready q = true then
            Modifiable.update b ((map OfStream.eval s).index q)
              ((map OfStream.eval s).value { val := q, property := hr })
          else b))
        i) =
    evalFinsupp (Readable.get b i) +
      ((if h₂ : (map (⇑evalFinsupp) s).ready q = true then
            fun₀ | (map (⇑evalFinsupp) s).index q => (map (⇑evalFinsupp) s).value { val := q, property := h₂ }
          else 0) +
          eval (map (⇑evalFinsupp) s) (advance (map (⇑evalFinsupp) s) ↑q))
        i

State before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ evalFinsupp
      (Readable.get
        (fold_wf Modifiable.update (map OfStream.eval s) (advance (map OfStream.eval s) ↑q)
          (if hr : (map OfStream.eval s).ready q = true then
            Modifiable.update b ((map OfStream.eval s).index q)
              ((map OfStream.eval s).value { val := q, property := hr })
          else b))
        i) =
    evalFinsupp (Readable.get b i) +
      ((if h₂ : (map (⇑evalFinsupp) s).ready q = true then
            fun₀ | (map (⇑evalFinsupp) s).index q => (map (⇑evalFinsupp) s).value { val := q, property := h₂ }
          else 0) +
          eval (map (⇑evalFinsupp) s) (advance (map (⇑evalFinsupp) s) ↑q))
        i
Tactic:
dsimp only [map_σ, map_valid, map_ready, map_index, map_value, Finsupp.coe_add, Pi.add_apply]
State after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ evalFinsupp
      (Readable.get
        (fold_wf Modifiable.update (map OfStream.eval s) (advance (map OfStream.eval s) ↑q)
          (if hr : s.ready q = true then
            Modifiable.update b (s.index q) (OfStream.eval (s.value { val := q, property := hr }))
          else b))
        i) =
    evalFinsupp (Readable.get b i) +
      ((if h₂ : s.ready q = true then fun₀ | s.index q => evalFinsupp (s.value { val := q, property := h₂ }) else 0) i +
        (eval (map (⇑evalFinsupp) s) (advance (map (⇑evalFinsupp) s) ↑q)) i)

State before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ evalFinsupp
      (Readable.get
        (fold_wf Modifiable.update (map OfStream.eval s) (advance (map OfStream.eval s) ↑q)
          (if hr : s.ready q = true then
            Modifiable.update b (s.index q) (OfStream.eval (s.value { val := q, property := hr }))
          else b))
        i) =
    evalFinsupp (Readable.get b i) +
      ((if h₂ : s.ready q = true then fun₀ | s.index q => evalFinsupp (s.value { val := q, property := h₂ }) else 0) i +
        (eval (map (⇑evalFinsupp) s) (advance (map (⇑evalFinsupp) s) ↑q)) i)
Tactic:
simp only [advance_val, map_seek, map_toOrder]
State after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ evalFinsupp
      (Readable.get
        (fold_wf Modifiable.update (map OfStream.eval s) (s.seek q (toOrder s q))
          (if hr : s.ready q = true then
            Modifiable.update b (s.index q) (OfStream.eval (s.value { val := q, property := hr }))
          else b))
        i) =
    evalFinsupp (Readable.get b i) +
      ((if h₂ : s.ready q = true then fun₀ | s.index q => evalFinsupp (s.value { val := q, property := h₂ }) else 0) i +
        (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)

State before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ evalFinsupp
      (Readable.get
        (fold_wf Modifiable.update (map OfStream.eval s) (s.seek q (toOrder s q))
          (if hr : s.ready q = true then
            Modifiable.update b (s.index q) (OfStream.eval (s.value { val := q, property := hr }))
          else b))
        i) =
    evalFinsupp (Readable.get b i) +
      ((if h₂ : s.ready q = true then fun₀ | s.index q => evalFinsupp (s.value { val := q, property := h₂ }) else 0) i +
        (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)
Tactic:
rw [ih]
State after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ evalFinsupp
        (Readable.get
          (if hr : s.ready q = true then
            Modifiable.update b (s.index q) (OfStream.eval (s.value { val := q, property := hr }))
          else b)
          i) +
      (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) +
      ((if h₂ : s.ready q = true then fun₀ | s.index q => evalFinsupp (s.value { val := q, property := h₂ }) else 0) i +
        (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)

case pos.a
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ WfRel s (s.seek q (toOrder s q)) ↑q

State before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ evalFinsupp
        (Readable.get
          (if hr : s.ready q = true then
            Modifiable.update b (s.index q) (OfStream.eval (s.value { val := q, property := hr }))
          else b)
          i) +
      (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) +
      ((if h₂ : s.ready q = true then fun₀ | s.index q => evalFinsupp (s.value { val := q, property := h₂ }) else 0) i +
        (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)

case pos.a
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ WfRel s (s.seek q (toOrder s q)) ↑q
Tactic:
split_ifs with hr
State after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
hr : s.ready q = true
⊢ evalFinsupp
        (Readable.get (Modifiable.update b (s.index q) (OfStream.eval (s.value { val := q, property := hr }))) i) +
      (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) +
      ((fun₀ | s.index q => evalFinsupp (s.value { val := q, property := hr })) i +
        (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)

case neg
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
hr : ¬s.ready q = true
⊢ evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) + (0 i + (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)

case pos.a
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ WfRel s (s.seek q (toOrder s q)) ↑q

State before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
hr : s.ready q = true
⊢ evalFinsupp
        (Readable.get (Modifiable.update b (s.index q) (OfStream.eval (s.value { val := q, property := hr }))) i) +
      (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) +
      ((fun₀ | s.index q => evalFinsupp (s.value { val := q, property := hr })) i +
        (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)
Tactic:
rw [Finsupp.single_apply, LawfulModifiable.get_update']
State after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
hr : s.ready q = true
⊢ evalFinsupp
        (if s.index q = i then OfStream.eval (s.value { val := q, property := hr }) (Readable.get b i)
        else Readable.get b i) +
      (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) +
      ((if s.index q = i then evalFinsupp (s.value { val := q, property := hr }) else 0) +
        (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)

State before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
hr : s.ready q = true
⊢ evalFinsupp
        (if s.index q = i then OfStream.eval (s.value { val := q, property := hr }) (Readable.get b i)
        else Readable.get b i) +
      (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) +
      ((if s.index q = i then evalFinsupp (s.value { val := q, property := hr }) else 0) +
        (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)
Tactic:
split_ifs with heq
State after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
hr : s.ready q = true
heq : s.index q = i
⊢ evalFinsupp (OfStream.eval (s.value { val := q, property := hr }) (Readable.get b i)) +
      (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) +
      (evalFinsupp (s.value { val := q, property := hr }) + (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)

case neg
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
hr : s.ready q = true
heq : ¬s.index q = i
⊢ evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) + (0 + (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)

State before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
hr : s.ready q = true
heq : s.index q = i
⊢ evalFinsupp (OfStream.eval (s.value { val := q, property := hr }) (Readable.get b i)) +
      (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) +
      (evalFinsupp (s.value { val := q, property := hr }) + (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)
Tactic:
rw [← add_assoc]
State after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
hr : s.ready q = true
heq : s.index q = i
⊢ evalFinsupp (OfStream.eval (s.value { val := q, property := hr }) (Readable.get b i)) +
      (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) + evalFinsupp (s.value { val := q, property := hr }) +
      (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i

State before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
hr : s.ready q = true
heq : s.index q = i
⊢ evalFinsupp (OfStream.eval (s.value { val := q, property := hr }) (Readable.get b i)) +
      (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) + evalFinsupp (s.value { val := q, property := hr }) +
      (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i
Tactic:
rw [LawfulOfStream.eval_of_stream]
State after:
no goals

State before:
case neg
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
hr : s.ready q = true
heq : ¬s.index q = i
⊢ evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) + (0 + (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)
Tactic:
simp
State after:
no goals

State before:
case neg
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
hr : ¬s.ready q = true
⊢ evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) + (0 i + (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)
Tactic:
simp
State after:
no goals

State before:
case pos.a
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ WfRel s (s.seek q (toOrder s q)) ↑q
Tactic:
exact s.progress rfl.le
State after:
no goals

State before:
case neg
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) q b) i) =
    evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) q) i
Tactic:
rw [Stream.fold_wf_invalid, Stream.eval_invalid]
State after:
case neg
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ evalFinsupp (Readable.get b i) = evalFinsupp (Readable.get b i) + 0 i

case neg.h
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ ¬(map (⇑evalFinsupp) s).valid q = true

case neg.h
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ ¬(map OfStream.eval s).valid q = true

State before:
case neg
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ evalFinsupp (Readable.get b i) = evalFinsupp (Readable.get b i) + 0 i

case neg.h
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ ¬(map (⇑evalFinsupp) s).valid q = true

case neg.h
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ ¬(map OfStream.eval s).valid q = true
Tactic:
all_goals (try exact hv)
State after:
case neg
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ evalFinsupp (Readable.get b i) = evalFinsupp (Readable.get b i) + 0 i

State before:
case neg
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ evalFinsupp (Readable.get b i) = evalFinsupp (Readable.get b i) + 0 i
Tactic:
simp
State after:
no goals

State before:
case neg.h
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ ¬(map OfStream.eval s).valid q = true
Tactic:
(try exact hv)
State after:
no goals

State before:
case neg.h
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ ¬(map OfStream.eval s).valid q = true
Tactic:
try exact hv
State after:
no goals

State before:
case neg.h
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ ¬(map OfStream.eval s).valid q = true
Tactic:
exact hv
State after:
no goals