multiTau_min_exists

lemma multiTau_min_exists {G Ω₀ : Type u} [MeasurableFinGroup G] [MeasureSpace Ω₀]    (p : multiRefPackage G Ω₀) :    ∃ (Ω : Fin p.m → Type u) (hΩ : ∀ i, MeasureSpace (Ω i)) (X : ∀ i, Ω i → G),    (∀ i, Measurable (X i)) ∧ (∀ i, IsProbabilityMeasure (hΩ i).volume)    ∧ multiTauMinimizes p Ω hΩ X := by  let μ := (multiTau_min_exists_measure p).choose  refine ⟨fun i ↦ G, fun i ↦ ⟨μ i⟩, fun i ↦ id, fun i ↦ measurable_id,    (multiTau_min_exists_measure p).choose_spec.1, ?_⟩  intro Ω' ν hν X hX  have : multiTau p (fun i ↦ G) (fun i ↦ ⟨(volume : Measure (Ω' i)).map (X i)⟩) (fun i ↦ id) =      multiTau p Ω' ν X := by    apply multiTau_of_ident _ _ _ (fun i ↦ ?_)    apply identDistrib_map (hX i) measurable_id  rw [← this]  apply (multiTau_min_exists_measure p).choose_spec.2  intro i  apply Measure.isProbabilityMeasure_map  exact (hX i).aemeasurable