tau_minimizer_exists

lemma tau_minimizer_exists [MeasurableSingletonClass G] :    ∃ (Ω : Type uG) (_ : MeasureSpace Ω) (X₁ : Ω → G) (X₂ : Ω → G),    Measurable X₁ ∧ Measurable X₂ ∧ IsProbabilityMeasure (ℙ : Measure Ω) ∧    tau_minimizes p X₁ X₂ := by  let μ := (tau_min_exists_measure p).choose  have : IsProbabilityMeasure μ.1 := (tau_min_exists_measure p).choose_spec.1  have : IsProbabilityMeasure μ.2 := (tau_min_exists_measure p).choose_spec.2.1  have P : IsProbabilityMeasure (μ.1.prod μ.2) := by infer_instance  let M : MeasureSpace (G × G) := ⟨μ.1.prod μ.2⟩  refine ⟨G × G, M, Prod.fst, Prod.snd, measurable_fst, measurable_snd, P, ?_⟩  intro ν₁ ν₂ h₁ h₂  have A : τ[@Prod.fst G G # @Prod.snd G G | p] = τ[id ; μ.1 # id ; μ.2 | p] :=    ProbabilityTheory.IdentDistrib.tau_eq p IdentDistrib.fst_id IdentDistrib.snd_id  convert (tau_min_exists_measure p).choose_spec.2.2 ν₁ ν₂ h₁ h₂