I Inf Is Convex

theorem iInf_IsConvex (ρ : MState d) (ε : Prob) : Convex ℝ { m | ρ.exp_val (1 - m) ≤ ε ∧ 0 ≤ m ∧ m ≤ 1 } := by  --We *could* get this from a more general fact that any linear subspace is convex,  --and the intersection of convex spaces is convex, and this is an intersection of  --three convex spaces. That would be more broken-down and lemmaified.  rintro x ⟨hx₁, hx₂, hx₃⟩ y ⟨hy₁, hy₂, hy₃⟩ a b ha hb hab  rw [← eq_sub_iff_add_eq'] at hab  subst b  refine And.intro ?_ (And.intro ?_ ?_)  · simp only [MState.exp_val, inner_sub_right, HermitianMat.inner_one, MState.tr,      tsub_le_iff_right, inner_add_right, inner_smul_right] at hx₁ hy₁ ⊢    linear_combination a * hx₁ + (1 - a) * hy₁  · apply HermitianMat.convex_cone <;> assumption  · rw [← sub_nonneg] at hx₃ hy₃ ⊢    convert HermitianMat.convex_cone hx₃ hy₃ ha hb using 1    simp only [sub_smul, one_smul, smul_sub]    abel