ProbabilityTheory.exists_isUniform

lemma exists_isUniform [MeasurableSpace S] [MeasurableSingletonClass S]    (H : Finset S) (h : H.Nonempty) :    ∃ (Ω : Type uS) (_ : MeasurableSpace Ω) (X : Ω → S) (μ : Measure Ω),      IsProbabilityMeasure μ ∧ Measurable X ∧ IsUniform H X μ ∧ (∀ ω, X ω ∈ H) ∧ FiniteRange X := by  refine ⟨H, Subtype.instMeasurableSpace, fun x ↦ x, (Finset.card H : ℝ≥0∞)⁻¹ • ∑ i, .dirac i, ?_,    measurable_subtype_coe, ⟨?_, ?_⟩, fun x ↦ x.2, ?_⟩  · constructor    simp only [Finset.univ_eq_attach, Measure.smul_apply, Measure.coe_finsetSum, Finset.sum_apply,      measure_univ, Finset.sum_const, Finset.card_attach, nsmul_eq_mul, mul_one, smul_eq_mul]    rw [ENNReal.inv_mul_cancel]    · simpa using h.ne_empty    · simp  · intro x hx y hy    simp only [Finset.univ_eq_attach, Measure.smul_apply, Measure.coe_finsetSum,      Finset.sum_apply, Measure.dirac_apply, smul_eq_mul]    rw [Finset.sum_eq_single ⟨x, hx⟩, Finset.sum_eq_single ⟨y, hy⟩]    · simp    · rintro ⟨b, bH⟩ _hb h'b      simp only [ne_eq, Subtype.mk.injEq] at h'b      simp [h'b]    · simp    · rintro ⟨b, bH⟩ _hb h'b      simp only [ne_eq, Subtype.mk.injEq] at h'b      simp [h'b]    · simp  · simp  · apply finiteRange_of_finset _ H _    simp