condRuzsaDist'_of_copy

lemma condRuzsaDist'_of_copy (X : Ω → G) {Y : Ω' → G} (hY : Measurable Y)    {W : Ω' → T} (hW : Measurable W)    (X' : Ω'' → G) {Y' : Ω''' → G} (hY' : Measurable Y') {W' : Ω''' → T} (hW' : Measurable W')    [IsFiniteMeasure μ'] [IsFiniteMeasure μ''']    (h1 : IdentDistrib X X' μ μ'') (h2 : IdentDistrib (⟨Y, W⟩) (⟨Y', W'⟩) μ' μ''')    [FiniteRange W] [FiniteRange W'] :    d[X ; μ # Y | W ; μ'] = d[X' ; μ'' # Y' | W' ; μ'''] := by  classical  set A := (FiniteRange.toFinset W) ∪ (FiniteRange.toFinset W')  have hfull : ∀ᵐ x ∂Measure.prod (dirac ()) (μ'.map W), x ∈      ((Finset.univ (α := Unit) ×ˢ A : Finset (Unit × T)) : Set (Unit × T)) := by    apply Measure.prod_of_full_measure_finset    · simp    simp only [A]    rw [Measure.map_apply ‹_› (by measurability)]    convert measure_empty (μ := μ)    simp [← FiniteRange.range]  have hfull' : ∀ᵐ x ∂Measure.prod (dirac ()) (μ'''.map W'), x ∈      ((Finset.univ (α := Unit) ×ˢ A : Finset (Unit × T)) : Set (Unit × T)) := by    apply Measure.prod_of_full_measure_finset    · simp    simp only [A]    rw [Measure.map_apply ‹_› (by measurability)]    convert measure_empty (μ := μ)    simp [← FiniteRange.range]  rw [condRuzsaDist'_def, condRuzsaDist'_def, Kernel.rdist, Kernel.rdist,    integral_eq_setIntegral hfull, integral_eq_setIntegral hfull', setIntegral_finset _ .finset,    setIntegral_finset _ .finset]  have hWW' : μ'.map W = μ'''.map W' := (h2.comp measurable_snd).map_eq  simp_rw [Measure.prod_real_apply_singleton, ← hWW', map_measureReal_apply hW (.singleton _)]  congr with x  by_cases hw : μ' (W ⁻¹' {x.2}) = 0  · simp only [smul_eq_mul, mul_eq_mul_left_iff, mul_eq_zero]    refine .inr <| .inr ?_    simp [Measure.real, hw]  congr 2  · rw [Kernel.const_apply, Kernel.const_apply, h1.map_eq]  · have hWW'x : μ' (W ⁻¹' {x.2}) = μ''' (W' ⁻¹' {x.2}) := by      have : μ'.map W {x.2} = μ'''.map W' {x.2} := by rw [hWW']      rwa [Measure.map_apply hW (.singleton _),        Measure.map_apply hW' (.singleton _)] at this    ext s hs    rw [condDistrib_apply' hY hW _ _ hw hs, condDistrib_apply' hY' hW' _ _ _ hs]    swap; · rwa [hWW'x] at hw    congr    have : μ'.map (⟨Y, W⟩) (s ×ˢ {x.2}) = μ'''.map (⟨Y', W'⟩) (s ×ˢ {x.2}) := by rw [h2.map_eq]    rwa [Measure.map_apply (hY.prodMk hW) (hs.prod (.singleton _)),      Measure.map_apply (hY'.prodMk hW') (hs.prod (.singleton _)),      Set.mk_preimage_prod, Set.mk_preimage_prod, Set.inter_comm,      Set.inter_comm ((fun a ↦ Y' a) ⁻¹' s)] at this