Two ways of counting a Multiset are equal

Stream: Is there code for X?

[Martin Dvořák]

Any idea how to prove the following technicality? Unfolding definitions doesn't get me there.

import Mathlib

example (s : Multiset Char) (f : Char → ℚ) :
    Finset.univ.sum (fun a : s => f a.fst) = (s.map f).sum := by
  sorry

Note that docs#Multiset.ToType is implicitly used in the first expression.

[Eric Wieser]

import Mathlib

example (s : Multiset Char) (f : Char → ℚ) :
    Finset.univ.sum (fun a : s => f a.fst) = (s.map f).sum := by
  rw [Finset.sum]
  erw [←Multiset.map_map f Sigma.fst,  Multiset.map_univ_coe]

[Eric Wieser]

I think there's a lemma missing about Finset.univ (Multiset.toType s)

[Damiano Testa]

This also seems to work.

import Mathlib

example (s : Multiset Char) (f : Char → ℚ) :
    Finset.univ.sum (fun a : s => f a.fst) = (s.map f).sum := by
  rw [Finset.sum, Multiset.map_univ]

[Martin Dvořák]

Should the missing lemma be in terms of Finset.univ.sigma (fun _ => Finset.univ) ?

[Eric Wieser]

Yes, but you need to launder it through the equiv to Multiset.ToType

[Martin Dvořák]

Damiano Testa said:

This also seems to work.

import Mathlib

example (s : Multiset Char) (f : Char → ℚ) :
    Finset.univ.sum (fun a : s => f a.fst) = (s.map f).sum := by
  rw [Finset.sum, Multiset.map_univ]

Thanks a lot!!
https://github.com/madvorak/vcsp/blob/74b18912b65b174fb059264c6c7e126186de4218/VCSP/LinearRelaxationAndSFP.lean#L232