phi_min_exists

lemma phi_min_exists (hA : A.Nonempty) : ∃ (μ : Measure (G × G)), IsProbabilityMeasure μ ∧    phiMinimizes Prod.fst Prod.snd η A μ := by  let _i : TopologicalSpace G := (⊥ : TopologicalSpace G)  have : DiscreteTopology G := ⟨rfl⟩  let iG : Inhabited G := ⟨0⟩  have T : Continuous (fun (μ : ProbabilityMeasure (G × G)) ↦ phi Prod.fst Prod.snd η A μ) := by    apply continuous_iff_continuousAt.2 (fun μ ↦ ?_)    apply Tendsto.add    · apply tendsto_rdist_probabilityMeasure continuous_fst continuous_snd tendsto_id    apply Tendsto.const_mul    apply Tendsto.add    · apply tendsto_rho_probabilityMeasure continuous_fst hA tendsto_id    · apply tendsto_rho_probabilityMeasure continuous_snd hA tendsto_id  obtain ⟨μ, _, hμ⟩ := @IsCompact.exists_isMinOn ℝ (ProbabilityMeasure (G × G))                          _ _ _ _ Set.univ isCompact_univ ⟨default, trivial⟩ _ T.continuousOn  refine ⟨μ, by infer_instance, ?_⟩  intro Ω' mΩ' X' Y' hP hX' hY'  let ν : Measure (G × G) := Measure.map (⟨X', Y'⟩) ℙ  have : IsProbabilityMeasure ν := isProbabilityMeasure_map (by fun_prop)  let ν' : ProbabilityMeasure (G × G) := ⟨ν, this⟩  have : phi Prod.fst Prod.snd η A ↑μ ≤ phi Prod.fst Prod.snd η A ↑ν' := hμ (mem_univ _)  apply this.trans_eq  have h₁ : IdentDistrib Prod.fst X' (ν' : Measure (G × G)) ℙ := by    refine ⟨measurable_fst.aemeasurable, hX'.aemeasurable, ?_⟩    simp only [ProbabilityMeasure.coe_mk, ν', ν]    rw [Measure.map_map measurable_fst (by fun_prop)]    rfl  have h₂ : IdentDistrib Prod.snd Y' (ν' : Measure (G × G)) ℙ := by    refine ⟨measurable_snd.aemeasurable, hY'.aemeasurable, ?_⟩    simp only [ProbabilityMeasure.coe_mk, ν', ν]    rw [Measure.map_map measurable_snd (by fun_prop)]    rfl  simp [phi, h₁.rdist_congr h₂, rho_eq_of_identDistrib h₁, rho_eq_of_identDistrib h₂]