ProbabilityTheory.IsUniform.measureReal_preimage_sub

lemma IsUniform.measureReal_preimage_sub [DecidableEq G] (Uunif : IsUniform A U)    (Umeas : Measurable U) (Vunif : IsUniform B V) (Vmeas : Measurable V) (h_indep : IndepFun U V)    (x : G) :    (ℙ : Measure Ω).real ((U - V) ⁻¹' {x}) = (A ∩ (B + {x})).card / (A.card * B.card) := by  classical  let W := fun ω ↦ V ω + x  have Wunif : IsUniform (B + {x} : Set G) W := by    simpa [W, Function.comp_def] using Vunif.comp (add_left_injective x)  have Wmeas : Measurable W := Vmeas.add_const _  have UWindep : IndepFun U W := by    have : Measurable (fun g ↦ g + x) := measurable_add_const x    exact h_indep.comp measurable_id this  have : (U - V) ⁻¹' {x} = (U - W) ⁻¹' {0} := by    ext ω    simp [W, ← sub_eq_zero (b := x)]    abel_nf  have h : (B : Set G)+{x} = (B+{x}:Finset G) := by simp  rw [h] at Wunif  simp [this, Uunif.measureReal_preimage_sub_zero Umeas Wunif Wmeas UWindep]