ProbabilityTheory.setRuzsaDist_of_inj

lemma setRuzsaDist_of_inj (A B : Set G) [hA : Finite A] [hB : Finite B] [Nonempty A] [Nonempty B]    {H : Type*} [hH : MeasurableSpace H] [MeasurableSingletonClass H] [AddCommGroup H]    [Countable H] {φ : G →+ H} (hφ : Function.Injective φ) :    dᵤ[φ '' A # φ '' B] = dᵤ[A # B] := by  obtain ⟨Ω, mΩ, UA, hμ, hUA_mes, hUA_unif, -, - ⟩ :=    exists_isUniform_measureSpace' A hA .of_subtype  obtain ⟨Ω', mΩ', UB, hμ', hUB_mes, hUB_unif, -, - ⟩ :=    exists_isUniform_measureSpace' B hB .of_subtype  rw [setRuzsaDist_eq_rdist hUA_unif hUB_unif hUA_mes hUB_mes, ← rdist_of_inj hUA_mes hUB_mes φ hφ]  classical  convert setRuzsaDist_eq_rdist (A := φ '' A) (B := φ '' B) (μ := (volume : Measure Ω))      (μ' := (volume : Measure Ω')) ?_ ?_ ?_ ?_  · convert IsUniform.comp (A.toFinite.coe_toFinset.symm ▸ hUA_unif) hφ using 1    ext x; simp  · convert IsUniform.comp (B.toFinite.coe_toFinset.symm ▸ hUB_unif) hφ using 1    ext x; simp  · fun_prop  · fun_prop