multiTau_min_exists_measure

lemma multiTau_min_exists_measure {G Ω₀ : Type u} [MeasurableFinGroup G] [MeasureSpace Ω₀]    (p : multiRefPackage G Ω₀) :    ∃ (μ : Fin p.m → Measure G), (∀ i, IsProbabilityMeasure (μ i)) ∧    ∀ (ν : Fin p.m → Measure G), (∀ i, IsProbabilityMeasure (ν i)) →    multiTau p (fun _ ↦ G) (fun i ↦ ⟨μ i⟩) (fun _ ↦ id) ≤      multiTau p (fun _ ↦ G) (fun i ↦ ⟨ν i⟩) (fun _ ↦ id) := by  let _i : TopologicalSpace G := (⊥ : TopologicalSpace G) -- Equip G with the discrete topology.  have : DiscreteTopology G := ⟨rfl⟩  let T : (Π (i : Fin p.m), ProbabilityMeasure G) → ℝ := -- restrict τ to the compact subspace    fun μ ↦ multiTau p (fun _ ↦ G) (fun i ↦ ⟨μ i⟩) (fun _ ↦ id)  have T_cont : Continuous T := multiTau_continuous p  have : Inhabited G := ⟨0⟩ -- Need to record this for Lean to know that proba measures exist.  obtain ⟨μ, _, hμ⟩ := IsCompact.exists_isMinOn isCompact_univ (by simp) T_cont.continuousOn  refine ⟨fun i ↦ μ i, fun i ↦ by infer_instance, fun ν hν ↦ ?_⟩  rw [isMinOn_univ_iff] at hμ  let ν' : Fin p.m → ProbabilityMeasure G := fun i ↦ ⟨ν i, hν i⟩  exact hμ ν'