-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma norm_cfcₙ_le {f : 𝕜 → 𝕜} {a : A} {c : ℝ} (h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ ≤ c) :
    ‖cfcₙ f a‖ ≤ c

Proof state:
case refine_2
𝕜 : 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
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ ≤ c
hf : ContinuousOn f (σₙ 𝕜 a)
hf0 : { toFun := (σₙ 𝕜 a).restrict f, continuous_toFun := ⋯ } 0 = 0
ha : p a
⊢ c ∈ upperBounds ((fun x => ‖f x‖) '' σₙ 𝕜 a)

Tactic:
rintro - ⟨x, hx, rfl⟩

Result:
case refine_2.intro.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
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ ≤ c
hf : ContinuousOn f (σₙ 𝕜 a)
hf0 : { toFun := (σₙ 𝕜 a).restrict f, continuous_toFun := ⋯ } 0 = 0
ha : p a
x : 𝕜
hx : x ∈ σₙ 𝕜 a
⊢ (fun x => ‖f x‖) x ≤ c

Proof state:
case refine_2
𝕜 : 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
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ ≤ c
hf : ContinuousOn f (σₙ 𝕜 a)
hf0 : { toFun := (σₙ 𝕜 a).restrict f, continuous_toFun := ⋯ } 0 = 0
ha : p a
⊢ (fun x => ‖x‖ ≤ c) ((cfcₙHom ha) { toFun := (σₙ 𝕜 a).restrict f, continuous_toFun := ⋯, map_zero' := hf0 })

Tactic:
simp only [← cfcₙ_apply f a, isLUB_le_iff (IsGreatest.norm_cfcₙ f a hf hf0 ha |>.isLUB)]

Result:
case refine_2
𝕜 : 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
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ ≤ c
hf : ContinuousOn f (σₙ 𝕜 a)
hf0 : { toFun := (σₙ 𝕜 a).restrict f, continuous_toFun := ⋯ } 0 = 0
ha : p a
⊢ c ∈ upperBounds ((fun x => ‖f x‖) '' σₙ 𝕜 a)

Proof state:
case refine_2.intro.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
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ ≤ c
hf : ContinuousOn f (σₙ 𝕜 a)
hf0 : { toFun := (σₙ 𝕜 a).restrict f, continuous_toFun := ⋯ } 0 = 0
ha : p a
x : 𝕜
hx : x ∈ σₙ 𝕜 a
⊢ (fun x => ‖f x‖) x ≤ c

Tactic:
exact h x hx

Result:
no goals

Proof state:
case refine_1
𝕜 : 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
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ ≤ c
⊢ (fun x => ‖x‖ ≤ c) 0

Tactic:
simpa using (norm_nonneg _).trans <| h 0 (quasispectrum.zero_mem 𝕜 a)

Result:
no goals