ProbabilityTheory.setRuzsaDist_add_const

lemma setRuzsaDist_add_const (A B : Set G) [hA : Finite A] [hB : Finite B] [Nonempty A] [Nonempty B]    (c c' : G) : dᵤ[A + {c} # B + {c'}] = dᵤ[A # B] := by  obtain ⟨Ω, mΩ, UA, hμ, hUA_mes, hUA_unif, -, hUA_fin ⟩ :=    exists_isUniform_measureSpace' A hA .of_subtype  obtain ⟨Ω', mΩ', UB, hμ', hUB_mes, hUB_unif, -, hUB_fin ⟩ :=    exists_isUniform_measureSpace' B hB .of_subtype  rw [setRuzsaDist_eq_rdist hUA_unif hUB_unif hUA_mes hUB_mes,    ← rdist_add_const' c c' hUA_mes hUB_mes]  classical  have : Finite (A + ({c} : Set G)) := Set.Finite.add hA (Set.finite_singleton c)  have : Finite (B + ({c'} : Set G)) := Set.Finite.add hB (Set.finite_singleton c')  convert setRuzsaDist_eq_rdist (A := A+{c}) (B := B+{c'}) (μ := (volume : Measure Ω))      (μ' := (volume : Measure Ω')) ?_ ?_ ?_ ?_  · convert! (A.toFinite.coe_toFinset.symm ▸ hUA_unif).comp (add_left_injective c) using 1    simp  · convert! (B.toFinite.coe_toFinset.symm ▸ hUB_unif).comp (add_left_injective c') using 1    simp  · fun_prop  · fun_prop