condRuzsaDist_of_copy

lemma condRuzsaDist_of_copy {X : Ω → G} (hX : Measurable X) {Z : Ω → S} (hZ : Measurable Z)    {Y : Ω' → G} (hY : Measurable Y) {W : Ω' → T} (hW : Measurable W)    {X' : Ω'' → G} (hX' : Measurable X') {Z' : Ω'' → S} (hZ' : Measurable Z')    {Y' : Ω''' → G} (hY' : Measurable Y') {W' : Ω''' → T} (hW' : Measurable W')    [IsFiniteMeasure μ] [IsFiniteMeasure μ'] [IsFiniteMeasure μ''] [IsFiniteMeasure μ''']    (h1 : IdentDistrib (⟨X, Z⟩) (⟨X', Z'⟩) μ μ'') (h2 : IdentDistrib (⟨Y, W⟩) (⟨Y', W'⟩) μ' μ''')    [FiniteRange Z] [FiniteRange W] [FiniteRange Z'] [FiniteRange W'] :    d[X | Z ; μ # Y | W ; μ'] = d[X' | Z' ; μ'' # Y' | W' ; μ'''] := by  classical  set A := (FiniteRange.toFinset Z) ∪ (FiniteRange.toFinset Z')  set B := (FiniteRange.toFinset W) ∪ (FiniteRange.toFinset W')  have hfull : ∀ᵐ x ∂Measure.prod (μ.map Z) (μ'.map W), x ∈      ((A ×ˢ B : Finset (S × T)): Set (S × T)) := by    simp only [A, B]    apply Measure.prod_of_full_measure_finset    all_goals {      rw [Measure.map_apply ‹_›]      convert measure_empty (μ := μ)      simp [← FiniteRange.range]      measurability    }  have hfull' : ∀ᵐ x ∂Measure.prod (μ''.map Z') (μ'''.map W'), x ∈    ((A ×ˢ B : Finset (S × T)): Set (S × T)) := by    simp only [A, B]    apply Measure.prod_of_full_measure_finset    all_goals {      rw [Measure.map_apply ‹_›]      convert measure_empty (μ := μ)      simp [← FiniteRange.range]      measurability    }  rw [condRuzsaDist_def, condRuzsaDist_def, Kernel.rdist, Kernel.rdist,    integral_eq_setIntegral hfull, integral_eq_setIntegral hfull', setIntegral_finset _ .finset,    setIntegral_finset _ .finset]  have hZZ' : μ.map Z = μ''.map Z' := (h1.comp measurable_snd).map_eq  have hWW' : μ'.map W = μ'''.map W' := (h2.comp measurable_snd).map_eq  simp_rw [Measure.prod_real_apply_singleton, ← hZZ', ← hWW',    map_measureReal_apply hZ (.singleton _), map_measureReal_apply hW (.singleton _)]  congr with x  by_cases hz : μ (Z ⁻¹' {x.1}) = 0  · simp only [smul_eq_mul, mul_eq_mul_left_iff, mul_eq_zero]    refine .inr <| .inl ?_    simp [Measure.real, hz]  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  · have hZZ'x : μ (Z ⁻¹' {x.1}) = μ'' (Z' ⁻¹' {x.1}) := by      have : μ.map Z {x.1} = μ''.map Z' {x.1} := by rw [hZZ']      rwa [Measure.map_apply hZ (.singleton _),        Measure.map_apply hZ' (.singleton _)] at this    ext s hs    rw [condDistrib_apply' hX hZ _ _ hz hs, condDistrib_apply' hX' hZ' _ _ _ hs]    swap; · rwa [hZZ'x] at hz    congr    have : μ.map (⟨X, Z⟩) (s ×ˢ {x.1}) = μ''.map (⟨X', Z'⟩) (s ×ˢ {x.1}) := by rw [h1.map_eq]    rwa [Measure.map_apply (hX.prodMk hZ) (hs.prod (.singleton _)),      Measure.map_apply (hX'.prodMk hZ') (hs.prod (.singleton _)),      Set.mk_preimage_prod, Set.mk_preimage_prod, Set.inter_comm,      Set.inter_comm ((fun a ↦ X' a) ⁻¹' s)] at this  · 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