ProbabilityTheory.IsUniform.measure_preimage_of_mem

lemma IsUniform.measure_preimage_of_mem    {H : Finset S} (h : IsUniform H X μ) (hX : Measurable X)    {s : S} (hs : s ∈ H) :    μ (X ⁻¹' {s}) = μ univ / Nat.card H := by  have B : μ univ = (Nat.card H) * μ (X ⁻¹' {s}) := calc    μ univ = μ (X ⁻¹' Hᶜ) + μ (X ⁻¹' H) := by      rw [← measure_union (disjoint_compl_left.preimage _) (hX .of_discrete)]      simp    _ = μ (X ⁻¹' H) := by rw [h.measure_preimage_compl, zero_add]    _ = ∑ x ∈ H, μ (X ⁻¹' {x}) := by      have : X ⁻¹' H = ⋃ x ∈ H, X ⁻¹' ({x} : Set S) := by simp      rw [this, measure_biUnion_finset]      · intro y _hy z _hz hyz        apply Disjoint.preimage        simp [hyz]      · intro y _hy        exact hX .of_discrete    _ = ∑ _x ∈ H, μ (X ⁻¹' {s}) :=      Finset.sum_congr rfl fun x hx ↦ h.eq_of_mem (by simpa using hx) hs    _ = H.card * μ (X ⁻¹' {s}) := by simp    _ = (Nat.card H) * μ (X ⁻¹' {s}) := by      congr; simp  rcases Nat.eq_zero_or_pos (Nat.card H) with hH|hH  · simp only [hH, CharP.cast_eq_zero, zero_mul, Measure.measure_univ_eq_zero] at B    simp [B]  · rwa [eq_comm, ← ENNReal.eq_div_iff] at B    · simpa using Nat.pos_iff_ne_zero.mp hH    · simp