feat(data/multiset): lemmas on intersecting a multiset with `repeat x n` (#13355)
feat(data/multiset): lemmas on intersecting a multiset with `repeat x n` (#13355)

Intersecting a multiset `s` with `repeat x n` gives `repeat x (min n (s.count x))`.





leanprover-community/mathlib,leanprover-community/mathlib