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))      ∧ ρ.exp_val T = 1 - ε := by  obtain ⟨T, hT₁, hT₂⟩ := exists_min' ρ ε S   --Instead of just `use T`, we (may) have to reduce it so that it saturates the ⟪ρ,T⟫ = 1 - ε bound.  --We do this by multiplying it by a scalar less than 1 to get a `T'`. Since this operator is less  --than T, it's still optimal in terms of achieving `β_ ε(ρ‖S)`, but it can get the `1 - ε` bound instead.  set δ := ρ.exp_val ↑T - (1 - ε)-- with δ_def  by_cases hδ : δ = 0  · use T, hT₁    linarith  replace hδ : 0 < δ := by linarith +splitNe  have hδ_le : δ ≤ 1 := by    linarith [ρ.exp_val_le_one T.2.2.2, ε.2]   have hTr : 0 < ρ.exp_val T := by    linarith [ε.coe_le_one]   set T' : HermitianMat d ℂ :=    (1 - δ / ρ.exp_val T) • T with hT'_def  have hT'_le : T' ≤ T := by    rw [← one_smul ℝ T.val, hT'_def]    gcongr    · exact T.2.2.1    · simp; positivity  have hρT' : ρ.exp_val (1 - T') = ε := by    simp [T', MState.exp_val_sub, δ, field]   have hT' : ρ.exp_val (1 - T') ≤ ε ∧ 0 ≤ T' ∧ T' ≤ 1 := by    use hρT'.le    constructor    · simp [T']      refine smul_nonneg ?_ T.2.2.1      bound    · exact hT'_le.trans T.2.2.2  use ⟨T', hT'⟩   constructor  · rw [OptimalHypothesisRate] at hT₁ ⊢    apply le_antisymm    · apply le_iInf      intro i      refine le_trans ?_ (le_of_eq_of_le hT₁ ?_)      · gcongr      · exact iInf_le_iff.mpr fun _ a ↦ a i    · exact iInf_le_iff.mpr fun _ a ↦ a ⟨T', hT'⟩  · simp [MState.exp_val_sub, ← hρT']