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

State before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
⊢ Multiset.sum ((evalMultiset s q) i) = (eval s q) i
Tactic:
have h₁ : (s |> (Stream.map fun x => {x}) |> Stream.map Multiset.sum).eval = s.eval := by
  dsimp only [Stream.map_map]
  rw [Stream.eval_map_id]
  ext; simp
State after:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
h₁ : eval (map Multiset.sum (map (fun x => {x}) s)) = eval s
⊢ Multiset.sum ((evalMultiset s q) i) = (eval s q) i

State before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
h₁ : eval (map Multiset.sum (map (fun x => {x}) s)) = eval s
⊢ Multiset.sum ((evalMultiset s q) i) = (eval s q) i
Tactic:
have h₂ : (s.evalMultiset q i).sum = (s |> (Stream.map fun x => {x}) |> Stream.map Multiset.sumAddMonoidHom).eval q i := by
  rw [Stream.eval_map_apply]
  rfl
State after:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
h₁ : eval (map Multiset.sum (map (fun x => {x}) s)) = eval s
h₂ : Multiset.sum ((evalMultiset s q) i) = (eval (map (⇑Multiset.sumAddMonoidHom) (map (fun x => {x}) s)) q) i
⊢ Multiset.sum ((evalMultiset s q) i) = (eval s q) i

State before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
h₁ : eval (map Multiset.sum (map (fun x => {x}) s)) = eval s
h₂ : Multiset.sum ((evalMultiset s q) i) = (eval (map (⇑Multiset.sumAddMonoidHom) (map (fun x => {x}) s)) q) i
⊢ Multiset.sum ((evalMultiset s q) i) = (eval s q) i
Tactic:
rw [Multiset.coe_sumAddMonoidHom] at h₂
State after:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
h₁ : eval (map Multiset.sum (map (fun x => {x}) s)) = eval s
h₂ : Multiset.sum ((evalMultiset s q) i) = (eval (map Multiset.sum (map (fun x => {x}) s)) q) i
⊢ Multiset.sum ((evalMultiset s q) i) = (eval s q) i

State before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
h₁ : eval (map Multiset.sum (map (fun x => {x}) s)) = eval s
h₂ : Multiset.sum ((evalMultiset s q) i) = (eval (map Multiset.sum (map (fun x => {x}) s)) q) i
⊢ Multiset.sum ((evalMultiset s q) i) = (eval s q) i
Tactic:
rw [h₂, h₁]
State after:
no goals

State before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
⊢ eval (map Multiset.sum (map (fun x => {x}) s)) = eval s
Tactic:
dsimp only [Stream.map_map]
State after:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
⊢ eval (map (Multiset.sum ∘ fun x => {x}) s) = eval s

State before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
⊢ eval (map (Multiset.sum ∘ fun x => {x}) s) = eval s
Tactic:
rw [Stream.eval_map_id]
State after:
case hf
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
⊢ (Multiset.sum ∘ fun x => {x}) = id

State before:
case hf
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
⊢ (Multiset.sum ∘ fun x => {x}) = id
Tactic:
ext
State after:
case hf.h
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
x✝ : α
⊢ (Multiset.sum ∘ fun x => {x}) x✝ = id x✝

State before:
case hf.h
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
x✝ : α
⊢ (Multiset.sum ∘ fun x => {x}) x✝ = id x✝
Tactic:
simp
State after:
no goals

State before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
h₁ : eval (map Multiset.sum (map (fun x => {x}) s)) = eval s
⊢ Multiset.sum ((evalMultiset s q) i) = (eval (map (⇑Multiset.sumAddMonoidHom) (map (fun x => {x}) s)) q) i
Tactic:
rw [Stream.eval_map_apply]
State after:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
h₁ : eval (map Multiset.sum (map (fun x => {x}) s)) = eval s
⊢ Multiset.sum ((evalMultiset s q) i) = Multiset.sumAddMonoidHom ((eval (map (fun x => {x}) s) q) i)

State before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
h₁ : eval (map Multiset.sum (map (fun x => {x}) s)) = eval s
⊢ Multiset.sum ((evalMultiset s q) i) = Multiset.sumAddMonoidHom ((eval (map (fun x => {x}) s) q) i)
Tactic:
rfl
State after:
no goals