le_rdist_of_phiMinimizes

lemma le_rdist_of_phiMinimizes (h_min : phiMinimizes X₁ X₂ η A ℙ)    {Ω₁ Ω₂ : Type*} [MeasurableSpace Ω₁]    [MeasurableSpace Ω₂] {μ₁ : Measure Ω₁} {μ₂ : Measure Ω₂}    [IsProbabilityMeasure μ₁] [IsProbabilityMeasure μ₂]    {X₁' : Ω₁ → G} {X₂' : Ω₂ → G} (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') :    d[X₁ # X₂] - η * (ρ[X₁' ; μ₁ # A] - ρ[X₁ # A]) - η * (ρ[X₂' ; μ₂ # A] - ρ[X₂ # A])      ≤ d[X₁' ; μ₁ # X₂' ; μ₂] := by  let Ω' : Type uG := G × G  have : IsProbabilityMeasure (Measure.map X₁' μ₁) := isProbabilityMeasure_map hX₁'.aemeasurable  have : IsProbabilityMeasure (Measure.map X₂' μ₂) := isProbabilityMeasure_map hX₂'.aemeasurable  let m : Measure Ω' := (Measure.map X₁' μ₁).prod (Measure.map X₂' μ₂)  have m_prob : IsProbabilityMeasure m := by infer_instance  let _ : MeasureSpace Ω' := ⟨m⟩  have hP : (ℙ : Measure Ω') = m := rfl  let Y₁ : G × G → G := Prod.fst  let Y₂ : G × G → G := Prod.snd  have : phi X₁ X₂ η A ℙ ≤ phi Y₁ Y₂ η A ℙ := h_min _ _ _ _ m_prob measurable_fst measurable_snd  have Id₁ : IdentDistrib Y₁ X₁' ℙ μ₁ :=    ⟨measurable_fst.aemeasurable, hX₁'.aemeasurable, by simp [Y₁, hP, m]⟩  have Id₂ : IdentDistrib Y₂ X₂' ℙ μ₂ :=    ⟨measurable_snd.aemeasurable, hX₂'.aemeasurable, by simp [Y₂, hP, m]⟩  have I : d[Y₁ # Y₂] = d[X₁' ; μ₁ # X₂' ; μ₂] := Id₁.rdist_congr Id₂  have J : ρ[Y₁ # A] = ρ[X₁' ; μ₁ # A] := rho_eq_of_identDistrib Id₁  have K : ρ[Y₂ # A] = ρ[X₂' ; μ₂ # A] := rho_eq_of_identDistrib Id₂  simp only [phi, I, J, K] at this  linarith