\begin{proposition}[Existence of $\tau$-minimizer]\label{tau-min-exist-multi}\lean{multiTau_continuous, multiTau_min_exists}\leanok  If $G$ is finite, then a $\tau$-minimizer exists.
\end{proposition}
\begin{proof}\uses{tau-def-multi} This is similar to the proof of \Cref{tau-min}.
\end{proof}
/-- If $G$ is finite, then a $\tau$-minimizer exists. -/
lemma multiTau_min_exists {G Ω₀ : Type u} [MeasureableFinGroup G] [MeasureSpace Ω₀] (p : multiRefPackage G Ω₀) : ∃ (Ω : Fin p.m → Type u) (hΩ : ∀ i, MeasureSpace (Ω i)) (X : ∀ i, Ω i → G), multiTauMinimizes p Ω hΩ X := by sorry