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

Proof state:
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ IsGreatest ((fun x => ‖f x‖) '' σ 𝕜 a) ‖cfc f a‖

Tactic:
obtain ⟨x, hx⟩ := ContinuousFunctionalCalculus.isCompact_spectrum a
  |>.image_of_continuousOn hf.norm |>.exists_isGreatest <|
  (ContinuousFunctionalCalculus.spectrum_nonempty a ha).image _

Result:
case intro
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _auto✝
ha : autoParam (p a) _auto✝
x : ℝ
hx : IsGreatest ((fun x => ‖f x‖) '' σ 𝕜 a) x
⊢ IsGreatest ((fun x => ‖f x‖) '' σ 𝕜 a) ‖cfc f a‖

Proof state:
case h.e'_4.a.mk
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _auto✝
ha : autoParam (p a) _auto✝
x : 𝕜
hx' : x ∈ σ 𝕜 a
hx : IsGreatest ((fun x => ‖f x‖) '' σ 𝕜 a) ((fun x => ‖f x‖) x)
y : 𝕜
hy : y ∈ σ 𝕜 a
⊢ ‖{ toFun := (σ 𝕜 a).restrict f, continuous_toFun := ⋯ } ⟨y, hy⟩‖ ≤ ‖f x‖

Tactic:
exact hx.2 ⟨y, hy, rfl⟩

Result:
no goals

Proof state:
case intro.intro.intro
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _auto✝
ha : autoParam (p a) _auto✝
x : 𝕜
hx' : x ∈ σ 𝕜 a
hx : IsGreatest ((fun x => ‖f x‖) '' σ 𝕜 a) ((fun x => ‖f x‖) x)
⊢ IsGreatest ((fun x => ‖f x‖) '' σ 𝕜 a) ‖cfc f a‖

Tactic:
convert hx

Result:
case h.e'_4
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _auto✝
ha : autoParam (p a) _auto✝
x : 𝕜
hx' : x ∈ σ 𝕜 a
hx : IsGreatest ((fun x => ‖f x‖) '' σ 𝕜 a) ((fun x => ‖f x‖) x)
⊢ ‖cfc f a‖ = (fun x => ‖f x‖) x

Proof state:
case h.e'_4
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _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 := ⋯ }‖ = (fun x => ‖f x‖) x

Tactic:
apply le_antisymm

Result:
case h.e'_4.a
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _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 := ⋯ }‖ ≤ (fun x => ‖f x‖) x

case h.e'_4.a
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _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 := ⋯ }‖

Proof state:
case h.e'_4.a
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _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 := ⋯ }‖ ≤ (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✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _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 := ⋯ } x_1‖ ≤ ‖f x‖

Proof state:
case intro
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _auto✝
ha : autoParam (p a) _auto✝
x : ℝ
hx : IsGreatest ((fun x => ‖f x‖) '' σ 𝕜 a) x
⊢ IsGreatest ((fun x => ‖f x‖) '' σ 𝕜 a) ‖cfc f a‖

Tactic:
obtain ⟨x, hx', rfl⟩ := hx.1

Result:
case intro.intro.intro
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _auto✝
ha : autoParam (p a) _auto✝
x : 𝕜
hx' : x ∈ σ 𝕜 a
hx : IsGreatest ((fun x => ‖f x‖) '' σ 𝕜 a) ((fun x => ‖f x‖) x)
⊢ IsGreatest ((fun x => ‖f x‖) '' σ 𝕜 a) ‖cfc f a‖

Proof state:
case h.e'_4
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _auto✝
ha : autoParam (p a) _auto✝
x : 𝕜
hx' : x ∈ σ 𝕜 a
hx : IsGreatest ((fun x => ‖f x‖) '' σ 𝕜 a) ((fun x => ‖f x‖) x)
⊢ ‖cfc f a‖ = (fun x => ‖f x‖) x

Tactic:
rw [cfc_apply f a, norm_cfcHom a _]

Result:
case h.e'_4
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _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 := ⋯ }‖ = (fun x => ‖f x‖) x

Proof state:
case h.e'_4.a
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _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 := ⋯ }‖

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

Result:
no goals