Pos of lt one

theorem pos_of_lt_one {ρ : MState d} (S : Set (MState d))  (hρ : ∃ σ ∈ S, σ.M.ker ≤ ρ.M.ker)  {ε : Prob} (hε : ε < 1) : 0 < β_ ε(ρ‖S) := by  obtain ⟨σ, hσ₁, hσ₂⟩ := hρ  --Assume the converse: that the infimum is zero. The set of such T's is inhabited  --and closed, so there is some T that attains the value zero. This T has zero  --inner product with σ (`σ.exp_val T = 0`), and yet (by definition of T's type) we  --also have that `ρ.exp_val (1 - T) ≤ ε < 1`. So `T` lives entirely in σ's kernel,  --which (by `h_supp`) is contained in ρ's kernel. So  --`ρ.exp_val (1 - T) = ρ.exp_val 1 - ρ.exp_val T = ρ.trace - 0 = 1`, a contradiction.  by_contra h  obtain ⟨⟨T, hT₁, hT₂, hT₃⟩, hT₄, hT₅⟩ := exists_min ρ ε S  rw [← bot_eq_zero'', not_bot_lt_iff] at h  rw [h, iSup_eq_bot, bot_eq_zero''] at hT₄  specialize hT₄ σ  simp only [iSup_pos hσ₁, Subtype.ext_iff, Set.Icc.coe_zero, MState.exp_val] at hT₄  rw [HermitianMat.inner_zero_iff σ.nonneg hT₂] at hT₄  replace hT₁ : ρ.exp_val (1 - T) ≠ 1 := (lt_of_le_of_lt hT₁ hε).ne  absurd hT₁  rw [ρ.exp_val_eq_one_iff ?_, sub_sub_cancel]  · grw [← hT₄]    rwa [HermitianMat.ker, HermitianMat.ker, ContinuousLinearMap.ker_le_ker_iff_range_le_range] at hσ₂    · simp    · simp  · exact sub_le_self 1 hT₂