rdist_le_of_isUniform_of_card_add_le'

theorem rdist_le_of_isUniform_of_card_add_le' {G : Type*} [AddCommGroup G] {A : Set G}    {K : ℝ} [Countable G] [A_fin : Finite A] [MeasurableSpace G]    [MeasurableSingletonClass G]    (h₀A : A.Nonempty) (hA : (A + A).ncard ≤ K * A.ncard)    {Ω : Type*} [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)] {U₀ : Ω → G}    (U₀unif : IsUniform A U₀) (U₀meas : Measurable U₀) : d[U₀ # -U₀] ≤ log K := by  obtain ⟨A_pos, AA_pos, K_pos⟩ : (0 : ℝ) < A.ncard ∧ (0 : ℝ) < (A + A).ncard ∧ 0 < K :=    PFR_conjecture_pos_aux' A_fin h₀A hA  rcases independent_copies_two U₀meas U₀meas with ⟨Ω, mΩ, U, U', hP, hU, hU', UU'_indep, idU, idU'⟩  have Uunif : IsUniform A U := U₀unif.of_identDistrib idU.symm .of_discrete  have U'unif : IsUniform A U' := U₀unif.of_identDistrib idU'.symm .of_discrete  have IU : d[U # -U'] ≤ log K := by    have I : H[U - (-U')] ≤ log (A + A).ncard := by      simp only [sub_neg_eq_add]      apply entropy_le_log_card_of_mem_finite (Set.Finite.add A_fin A_fin) (hU.add hU')      filter_upwards [Uunif.ae_mem, U'unif.ae_mem] with ω h1 h2      exact Set.add_mem_add h1 h2    have J : log (A + A).ncard ≤ log K + log A.ncard := by      apply (log_le_log AA_pos hA).trans (le_of_eq _)      rw [log_mul K_pos.ne' A_pos.ne']    have A_fin_neg : Finite (-A: Set G) := Set.Finite.neg A_fin    replace UU'_indep : IndepFun U (-U') ℙ := UU'_indep.neg_right    replace U'unif : IsUniform (-A) (-U') := by      let A' := A.toFinite.toFinset      have hAA' : A' = A := Finite.coe_toFinset (toFinite A)      rw [←hAA'] at U'unif      classical      simpa [hAA', Function.comp_def, Pi.neg_def] using IsUniform.comp U'unif neg_injective    rw [UU'_indep.rdist_eq hU hU'.neg, Uunif.entropy_eq' A_fin hU,      U'unif.entropy_eq' A_fin_neg hU'.neg]    have : log (-A).ncard = log A.ncard := by congr 2; simp    linarith  replace idU' : IdentDistrib (-U') (-U₀) ℙ ℙ := idU'.comp (u := fun x ↦ -x) (by fun_prop)  rwa [idU.rdist_congr idU'] at IU