tau_min_exists_measure

lemma tau_min_exists_measure [MeasurableSingletonClass G] :    ∃ (μ : Measure G × Measure G),    IsProbabilityMeasure μ.1 ∧ IsProbabilityMeasure μ.2 ∧    ∀ (ν₁ : Measure G) (ν₂ : Measure G), IsProbabilityMeasure ν₁ → IsProbabilityMeasure ν₂ →      τ[id ; μ.1 # id ; μ.2 | p] ≤ τ[id ; ν₁ # id ; ν₂ | p] := by  let _i : TopologicalSpace G := (⊥ : TopologicalSpace G) -- Equip G with the discrete topology.  have : DiscreteTopology G := ⟨rfl⟩  let T : ProbabilityMeasure G × ProbabilityMeasure G → ℝ := -- restrict τ to the compact subspace    fun ⟨μ₁, μ₂⟩ ↦ τ[id ; μ₁ # id ; μ₂ | p]  have T_cont : Continuous T := by apply continuous_tau_restrict_probabilityMeasure  have : Inhabited G := ⟨0⟩ -- Need to record this for Lean to know that proba measures exist.  obtain ⟨μ, _, hμ⟩ := @IsCompact.exists_isMinOn ℝ (ProbabilityMeasure G × ProbabilityMeasure G)                          _ _ _ _ Set.univ isCompact_univ ⟨default, trivial⟩ T T_cont.continuousOn  use ⟨μ.1.toMeasure, μ.2.toMeasure⟩  refine ⟨μ.1.prop, μ.2.prop, ?_⟩  intro ν₁ ν₂ Pν₁ Pν₂  rw [isMinOn_univ_iff] at hμ  let ν : ProbabilityMeasure G × ProbabilityMeasure G := ⟨⟨ν₁, Pν₁⟩, ν₂, Pν₂⟩  exact hμ ν