feat: μ (Prod.fst ⁻¹' {x}) = ∑' y, μ {(x, y)} (#18390) From PFR
μ (Prod.fst ⁻¹' {x}) = ∑' y, μ {(x, y)}