ProbabilityTheory.IsUniform.measureReal_preimage_sub_zero

lemma IsUniform.measureReal_preimage_sub_zero [DecidableEq G] (Uunif : IsUniform A U)    (Umeas : Measurable U) (Vunif : IsUniform B V) (Vmeas : Measurable V) (h_indep : IndepFun U V) :    (ℙ : Measure Ω).real ((U - V) ⁻¹' {0})      = (A ∩ B).card / (A.card * B.card) := by  cases nonempty_fintype G  have : (U - V) ⁻¹' {0} = ⋃ (g : G), (U ⁻¹' {g} ∩ V⁻¹' {g}) := by    ext ω; simp [sub_eq_zero, eq_comm]  rw [this, measureReal_iUnion_fintype _ (fun i ↦ (Umeas .of_discrete).inter <| Vmeas .of_discrete)]  swap  · intro g g' hgg'    apply Set.disjoint_iff_inter_eq_empty.2    ext a    simp (config := {contextual := True}) [hgg']  let W : Finset G := A ∩ B  calc    ∑ p, (ℙ : Measure Ω).real (U ⁻¹' {p} ∩ V ⁻¹' {p})      = ∑ p, (ℙ : Measure Ω).real (U ⁻¹' {p}) * (ℙ : Measure Ω).real (V ⁻¹' {p}) := by        apply sum_congr _ _ (fun g ↦ ?_)        rw [h_indep.measureReal_inter_preimage_eq_mul .of_discrete .of_discrete]    _ = ∑ p ∈ W, (ℙ : Measure Ω).real (U ⁻¹' {p}) * (ℙ : Measure Ω).real (V ⁻¹' {p}) := by        apply (Finset.sum_subset W.subset_univ _).symm        intro i _ hi        obtain hi | hi : i ∉ A ∨ i ∉ B := by simpa [or_iff_not_imp_left, W] using hi        · simp [Uunif.measureReal_preimage_of_nmem hi]        · simp [Vunif.measureReal_preimage_of_nmem hi]    _ = ∑ p ∈ W, (1 / A.card : ℝ) * (1 / B.card) := by        congr! 1 with i hi        replace hi : i ∈ A ∧ i ∈ B := by simpa [W] using hi        rw [Uunif.measureReal_preimage_of_mem (by trivial) hi.1,            Vunif.measureReal_preimage_of_mem (by trivial) hi.2]    _ = (W.card : ℝ) / (A.card * B.card) := by simp [div_eq_inv_mul]; ring