Hermitian Mat trace rpow le trace of le one

lemma HermitianMat.trace_rpow_le_trace_of_le_one    (A : HermitianMat d ℂ) (hA : 0 ≤ A) (hA1 : A ≤ 1)    (p : ℝ) (hp : 1 ≤ p) :    (A ^ p).trace ≤ A.trace := by  -- Rewrite both sides using trace_rpow_eq_sum: Tr[A^p] = ∑ λ_i^p and Tr[A] = ∑ λ_i (using trace_rpow_eq_sum and rpow_one for the latter).  have h_trace_eq_sum : (A ^ p).trace = ∑ i, (A.H.eigenvalues i) ^ p ∧ A.trace = ∑ i, (A.H.eigenvalues i) := by    exact ⟨ by rw [ HermitianMat.trace_rpow_eq_sum ], by rw [ show A.trace = ∑ i, ( A.H.eigenvalues i ) by simpa using HermitianMat.trace_rpow_eq_sum A 1 ] ⟩;  rw [ h_trace_eq_sum.1, h_trace_eq_sum.2 ];  apply_rules [ Finset.sum_le_sum ];  intro i hi; by_cases hi0 : A.H.eigenvalues i = 0 <;> simp_all  · rw [ Real.zero_rpow ( by positivity ) ];  · conv_rhs => rw [← (A.H.eigenvalues i).rpow_one]    apply Real.rpow_le_rpow_of_exponent_ge    · exact lt_of_le_of_ne' (le_of_not_gt fun hi => hi0 <| by linarith [ show 0 ≤ A.H.eigenvalues i by simpa using hA.eigenvalues_nonneg i ] ) hi0    · exact A.eigenvalues_le_one_of_le_one hA1 i    · exact hp