-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma IsGreatest.norm_cfcₙ (f : 𝕜 → 𝕜) (a : A)
    (hf : ContinuousOn f (σₙ 𝕜 a)

Proof state:
case h.e'_4.a
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σₙ 𝕜 a)) _auto✝
hf₀ : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
x : 𝕜
hx' : x ∈ σₙ 𝕜 a
hx : IsGreatest ((fun x => ‖f x‖) '' σₙ 𝕜 a) ((fun x => ‖f x‖) x)
⊢ (fun x => ‖f x‖) x ≤ ‖{ toFun := (σₙ 𝕜 a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ }‖

Tactic:
exact le_trans (by simp) <| ContinuousMap.norm_coe_le_norm _ (⟨x, hx'⟩ : σₙ 𝕜 a)

Result:
no goals

Proof state:
case h.e'_4.a
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σₙ 𝕜 a)) _auto✝
hf₀ : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
x : 𝕜
hx' : x ∈ σₙ 𝕜 a
hx : IsGreatest ((fun x => ‖f x‖) '' σₙ 𝕜 a) ((fun x => ‖f x‖) x)
⊢ ‖{ toFun := (σₙ 𝕜 a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ }‖ ≤ (fun x => ‖f x‖) x

Tactic:
apply ContinuousMap.norm_le _ (norm_nonneg _) |>.mpr

Result:
case h.e'_4.a
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σₙ 𝕜 a)) _auto✝
hf₀ : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
x : 𝕜
hx' : x ∈ σₙ 𝕜 a
hx : IsGreatest ((fun x => ‖f x‖) '' σₙ 𝕜 a) ((fun x => ‖f x‖) x)
⊢ ∀ (x_1 : ↑(σₙ 𝕜 a)), ‖↑{ toFun := (σₙ 𝕜 a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } x_1‖ ≤ ‖f x‖

Proof state:
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σₙ 𝕜 a)) _auto✝
hf₀ : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
⊢ IsGreatest ((fun x => ‖f x‖) '' σₙ 𝕜 a) ‖cfcₙ f a‖

Tactic:
obtain ⟨x, hx⟩ := NonUnitalContinuousFunctionalCalculus.isCompact_quasispectrum a
    |>.image_of_continuousOn hf.norm |>.exists_isGreatest <|
    (quasispectrum.nonempty 𝕜 a).image _

Result:
case intro
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σₙ 𝕜 a)) _auto✝
hf₀ : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
x : ℝ
hx : IsGreatest ((fun x => ‖f x‖) '' σₙ 𝕜 a) x
⊢ IsGreatest ((fun x => ‖f x‖) '' σₙ 𝕜 a) ‖cfcₙ f a‖