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

Proof state:
case intro.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
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)
⊢ 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✝⁵ : 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)
⊢ ‖cfcₙ f a‖ = (fun x => ‖f x‖) 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✝
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' := ⋯ } ⟨x, hx'⟩‖

Tactic:
simp

Result:
no goals

Proof state:
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‖

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✝⁵ : 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)
⊢ 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✝⁵ : 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 le_antisymm

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)
⊢ ‖{ toFun := (σₙ 𝕜 a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ }‖ ≤ (fun x => ‖f x‖) x

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' := ⋯ }‖

Proof state:
case h.e'_4.a.mk
𝕜 : 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)
y : 𝕜
hy : y ∈ σₙ 𝕜 a
⊢ ‖↑{ toFun := (σₙ 𝕜 a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } ⟨y, hy⟩‖ ≤ ‖f x‖

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

Result:
no goals

Proof state:
case h.e'_4
𝕜 : 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)
⊢ ‖cfcₙ f a‖ = (fun x => ‖f x‖) x

Tactic:
rw [cfcₙ_apply f a, norm_cfcₙHom a _]

Result:
case h.e'_4
𝕜 : 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

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)
⊢ ∀ (x_1 : ↑(σₙ 𝕜 a)), ‖↑{ toFun := (σₙ 𝕜 a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } x_1‖ ≤ ‖f x‖

Tactic:
rintro ⟨y, hy⟩

Result:
case h.e'_4.a.mk
𝕜 : 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)
y : 𝕜
hy : y ∈ σₙ 𝕜 a
⊢ ‖↑{ toFun := (σₙ 𝕜 a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } ⟨y, hy⟩‖ ≤ ‖f x‖