∀ {A : Type u_1} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [inst_5 : PartialOrder A] [inst_6 : StarOrderedRing A]
  [inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_8 : NonnegSpectrumClass ℝ A]
  (f : NNReal → NNReal) (a : A),
  autoParam (ContinuousOn f (quasispectrum NNReal a)) IsGreatest.nnnorm_cfcₙ_nnreal._auto_1 →
    autoParam (f 0 = 0) IsGreatest.nnnorm_cfcₙ_nnreal._auto_3 →
      autoParam (0 ≤ a) IsGreatest.nnnorm_cfcₙ_nnreal._auto_5 → IsGreatest (f '' quasispectrum NNReal a) ‖cfcₙ f a‖₊