Exists min

theorem exists_min' (ρ : MState d) (ε : Prob) (S : Set (MState d)):    ∃ (T : { m : HermitianMat d ℂ // ρ.exp_val (1 - m) ≤ ε ∧ 0 ≤ m ∧ m ≤ 1}),      (⨆ σ ∈ S, ⟨_, σ.exp_val_prob T.prop.right⟩ = β_ ε(ρ‖S))      ∧ 1 - ε ≤ ρ.exp_val T := by  have _ : Nonempty d := ρ.nonempty  rcases S.eq_empty_or_nonempty with rfl | hS  · simpa [-Subtype.exists] using ⟨rfl, ⟨1, by simp⟩, by simp⟩  rw [← Set.nonempty_coe_sort] at hS  obtain ⟨T, hT₁, hT₂⟩ := IsCompact.exists_isMinOn (α := Prob)    (isCompact_iff_isCompact_univ.mp (iInf_IsCompact ρ ε)) Set.univ_nonempty    (f := fun T ↦ ⨆ σ ∈ S, ⟨_, σ.exp_val_prob T.prop.right⟩)    (by      have h := HermitianMat.innerₗ.continuous_iSup_fst        (Bornology.isBounded_induced.mp (Bornology.IsBounded.all S))      apply Continuous.continuousOn      simp_rw [← iSup_subtype'', subtype_val_iSup' (ι := S)]      refine Continuous.subtype_mk ?_ _      refine Continuous.comp (g := fun T ↦ ⨆ (i : S), i.val.exp_val T) ?_ continuous_subtype_val      convert h with T      rw [← sSup_image' (s := S) (f := fun i ↦ i.exp_val T)]      rw [← sSup_image' (s := (MState.M '' S)) (f := fun i ↦ i.innerₗ T)]      simp [Set.image, MState.exp_val, HermitianMat.innerₗ]    )  clear hT₁   use T  constructor  · simp only [isMinOn_univ_iff] at hT₂    rw [OptimalHypothesisRate]    --Why is the following three bundled together not a theorem? Is it, and I can't find it? TODO    apply le_antisymm    · exact le_iInf hT₂    · exact iInf_le_iff.mpr fun _ a ↦ a T  · simpa [MState.exp_val_sub, add_comm (ε : ℝ) _] using T.2.1