-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma norm_cfc_lt {f : 𝕜 → 𝕜} {a : A} {c : ℝ} (hc : 0 < c) (h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c) :
    ‖cfc f a‖ < c

Proof state:
case inr.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
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
h✝ : Nontrivial A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
x : 𝕜
hx : x ∈ σ 𝕜 a
⊢ (fun x => ‖f x‖) x < c

Tactic:
exact h x hx

Result:
no goals

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
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
h✝ : Nontrivial A
⊢ (fun x => ‖x‖ < c) 0

Tactic:
simpa

Result:
no goals

Proof state:
case inl
𝕜 : 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
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
h✝ : Subsingleton A
⊢ ‖cfc f a‖ < c

Tactic:
simpa [Subsingleton.elim (cfc f a) 0]

Result:
no goals

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
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
⊢ ‖cfc f a‖ < c

Tactic:
obtain (_ | _) := subsingleton_or_nontrivial A

Result:
case inl
𝕜 : 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
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
h✝ : Subsingleton A
⊢ ‖cfc f a‖ < c

case inr
𝕜 : 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
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
h✝ : Nontrivial A
⊢ ‖cfc f a‖ < c

Proof state:
case inr
𝕜 : 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
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
h✝ : Nontrivial A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
⊢ (fun x => ‖x‖ < c) ((cfcHom ha) { toFun := (σ 𝕜 a).restrict f, continuous_toFun := ⋯ })

Tactic:
simp only [← cfc_apply f a, (IsGreatest.norm_cfc f a hf ha |>.lt_iff)]

Result:
case inr
𝕜 : 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
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
h✝ : Nontrivial A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
⊢ ∀ x ∈ (fun x => ‖f x‖) '' σ 𝕜 a, x < c

Proof state:
case inr
𝕜 : 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
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
h✝ : Nontrivial A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
⊢ ∀ x ∈ (fun x => ‖f x‖) '' σ 𝕜 a, x < c

Tactic:
rintro - ⟨x, hx, rfl⟩

Result:
case inr.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
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
h✝ : Nontrivial A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
x : 𝕜
hx : x ∈ σ 𝕜 a
⊢ (fun x => ‖f x‖) x < c