map_prod_uniformOn_ne_zero

lemma map_prod_uniformOn_ne_zero {y : G} (hA : A.Nonempty)    {μ : Measure G} [IsProbabilityMeasure μ] (hμ : ∀ x, μ {x} ≠ 0) :    (μ.prod (uniformOn A)).map (Prod.fst + Prod.snd) {y} ≠ 0 := by  cases nonempty_fintype G  intro h  obtain ⟨a, ha⟩ : ∃ x, x ∈ A := by exact hA  let ν := uniformOn (A : Set G)  have : IsProbabilityMeasure ν :=    isProbabilityMeasure_uniformOn A.finite_toSet hA  have h_indep : IndepFun Prod.fst Prod.snd (μ.prod ν) := ProbabilityTheory.indepFun_fst_snd  rw [h_indep.map_add_singleton_eq_sum measurable_fst measurable_snd,    Finset.sum_eq_zero_iff_of_nonneg (fun i _ ↦ by simp)] at h  specialize h a (Finset.mem_univ a)  have : (Measure.map Prod.snd (μ.prod ν)) {a} ≠ 0 := by    simp [Measure.map_snd_prod, ν, uniformOn_apply_singleton_of_mem (by exact ha) A.finite_toSet]  simp only [mul_eq_zero, this, false_or, Measure.map_fst_prod] at h  simp only [measure_univ, one_smul] at h  exact hμ (y - a) h