awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σ ℝ≥0 a, f x ≤ c
h_1 : Nontrivial A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
inr : c ∈ upperBounds (f '' σ ℝ≥0 a)
⊢ nnnorm (E := A)
      ((cfcHom (p := fun (x : A) ↦ 0 ≤ x) ha : (a : C((↑(σ ℝ≥0 a) : Type), ℝ≥0)) → A)
          { toFun := (σ ℝ≥0 a).restrict (π := fun (a : ℝ≥0) ↦ ℝ≥0) f, continuous_toFun := ⋯ :
            C((↑(σ ℝ≥0 a) : Type), ℝ≥0) } :
        A) ≤
    c

Tactic:
simp only [← cfc_apply f a, isLUB_le_iff (IsGreatest.nnnorm_cfc_nnreal f a hf ha |>.isLUB)]

Premises used: IsGreatest.nnnorm_cfc_nnreal, isLUB_le_iff, IsGreatest.isLUB, cfc_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σ ℝ≥0 a, f x ≤ c
h_1 : Nontrivial A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
x : ℝ≥0
hx : x ∈ σ ℝ≥0 a
⊢ f x ≤ c

Tactic:
h x hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σ ℝ≥0 a, f x ≤ c
h_1 : Nontrivial A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
x : ℝ≥0
hx : x ∈ σ ℝ≥0 a
⊢ f x ≤ c

Tactic:
exact h x hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
⊢ ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ ≤ c ↔ ∀ x ∈ σ ℝ≥0 a, f x ≤ c

Tactic:
⟨fun h _ hx ↦ apply_le_nnnorm_cfc_nnreal f a hx hf ha |>.trans h, nnnorm_cfc_nnreal_le⟩

Premises used: nnnorm_cfc_nnreal_le, apply_le_nnnorm_cfc_nnreal, Iff.intro, LE.le.trans
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hc : 0 < c
h : ∀ x ∈ σ ℝ≥0 a, f x < c
inl : Subsingleton A → ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ < c
inr : Nontrivial A → ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ < c
⊢ ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ < c

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

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hc : 0 < c
h : ∀ x ∈ σ ℝ≥0 a, f x < c
h_1 : Subsingleton A
inl : nnnorm.{u_1} (E := A) 0 < c
⊢ ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ < c

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

Premises used: cfc, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hc : 0 < c
h : ∀ x ∈ σ ℝ≥0 a, f x < c
h_1 : Subsingleton A
⊢ nnnorm.{u_1} (E := A) 0 < c

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hc : 0 < c
h : ∀ x ∈ σ ℝ≥0 a, f x < c
h_1 : Nontrivial A
⊢ (fun (x : A) ↦ ‖x‖₊ < c) 0

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hc : 0 < c
h : ∀ x ∈ σ ℝ≥0 a, f x < c
h_1 : Nontrivial A
inr :
  ∀ (hf : ContinuousOn f (σ ℝ≥0 a)) (ha : 0 ≤ a),
    (fun (x : A) ↦ ‖x‖₊ < c)
      ((cfcHom (p := fun (x : A) ↦ 0 ≤ x) ha : (a : C((↑(σ ℝ≥0 a) : Type), ℝ≥0)) → A)
        { toFun := (σ ℝ≥0 a).restrict (π := fun (a : ℝ≥0) ↦ ℝ≥0) f, continuous_toFun := ⋯ :
          C((↑(σ ℝ≥0 a) : Type), ℝ≥0) })
⊢ ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ < c

Tactic:
refine cfc_cases (‖·‖₊ < c) a f (by simpa) fun hf ha ↦ ?_

Premises used: NNNorm.nnnorm, LT.lt, cfc_cases
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hc : 0 < c
h : ∀ x ∈ σ ℝ≥0 a, f x < c
h_1 : Nontrivial A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
inr : ∀ x ∈ f '' σ ℝ≥0 a, x < c
⊢ nnnorm (E := A)
      ((cfcHom (p := fun (x : A) ↦ 0 ≤ x) ha : (a : C((↑(σ ℝ≥0 a) : Type), ℝ≥0)) → A)
          { toFun := (σ ℝ≥0 a).restrict (π := fun (a : ℝ≥0) ↦ ℝ≥0) f, continuous_toFun := ⋯ :
            C((↑(σ ℝ≥0 a) : Type), ℝ≥0) } :
        A) <
    c

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

Premises used: IsGreatest.lt_iff, IsGreatest.nnnorm_cfc_nnreal, cfc_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hc : 0 < c
h : ∀ x ∈ σ ℝ≥0 a, f x < c
h_1 : Nontrivial A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
x : ℝ≥0
hx : x ∈ σ ℝ≥0 a
⊢ f x < c

Tactic:
h x hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hc : 0 < c
h : ∀ x ∈ σ ℝ≥0 a, f x < c
h_1 : Nontrivial A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
x : ℝ≥0
hx : x ∈ σ ℝ≥0 a
⊢ f x < c

Tactic:
exact h x hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hc : 0 < c
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
⊢ ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ < c ↔ ∀ x ∈ σ ℝ≥0 a, f x < c

Tactic:
⟨fun h _ hx ↦ apply_le_nnnorm_cfc_nnreal f a hx hf ha |>.trans_lt h, nnnorm_cfc_nnreal_lt hc⟩

Premises used: nnnorm_cfc_nnreal_lt, apply_le_nnnorm_cfc_nnreal, Iff.intro, LE.le.trans_lt
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
inst_7 : Nontrivial A
a : A
ha : 0 ≤ a
⊢ IsGreatest (σ ℝ≥0 a) ‖a‖₊

Tactic:
simpa [cfc_id ℝ≥0 a] using IsGreatest.nnnorm_cfc_nnreal id a

Premises used: IsGreatest.nnnorm_cfc_nnreal, id, NNReal, cfc_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
a : A
x : ℝ≥0
hx : x ∈ σ ℝ≥0 a
ha : 0 ≤ a
⊢ x ≤ ‖a‖₊

Tactic:
simpa [cfc_id ℝ≥0 a] using apply_le_nnnorm_cfc_nnreal id a hx

Premises used: id, NNReal, apply_le_nnnorm_cfc_nnreal, cfc_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
inst_7 : Nontrivial A
f : ℝ≥0 → ℝ≥0
a : A
hf : MonotoneOn f (σ ℝ≥0 a)
hf₂ : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
⊢ ‖cfc (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ = f ‖a‖₊

Tactic:
IsGreatest.nnnorm_cfc_nnreal f a |>.unique <| hf.map_isGreatest (isGreatest_spectrum a)

Premises used: MonotoneOn.map_isGreatest, IsGreatest.nnnorm_cfc_nnreal, IsGreatest.unique, IsometricContinuousFunctionalCalculus.isGreatest_spectrum
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
ha : 0 ≤ a
rw : IsGreatest (f '' σₙ ℝ≥0 a) ‖cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a‖₊
⊢ IsGreatest (f '' σₙ ℝ≥0 a) ‖cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a‖₊

Tactic:
rw [cfcₙ_nnreal_eq_real ..]

Premises used: cfcₙ_nnreal_eq_real
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
ha : 0 ≤ a
⊢ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
obtain ⟨-, ha'⟩ := nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts.mp ha

Premises used: Iff.mp, nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
ha : 0 ≤ a
ha' : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ Eq (α := ℝ) ((fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) 0) 0

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
ha : 0 ≤ a
ha' : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
h : f '' σₙ ℝ≥0 a = (fun (x : ℝ) ↦ ‖(↑(f x.toNNReal) : ℝ)‖₊) '' σₙ ℝ a
convert! : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (σₙ ℝ a)
⊢ IsGreatest (f '' σₙ ℝ≥0 a) ‖cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a‖₊

Tactic:
convert! IsGreatest.nnnorm_cfcₙ (fun x : ℝ ↦ (f x.toNNReal : ℝ)) a ?hf_cont (by simpa)

Premises used: IsGreatest.nnnorm_cfcₙ, NNReal.toReal, Real.toNNReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
ha : 0 ≤ a
ha' : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (σₙ ℝ a)

Tactic:
continuous_subtype_val.comp_continuousOn <|
    ContinuousOn.comp ‹_› continuous_real_toNNReal.continuousOn <| ha'.image ▸ Set.mapsTo_image ..

Premises used: Continuous.continuousOn, continuous_subtype_val, Continuous.comp_continuousOn, ContinuousOn.comp, continuous_real_toNNReal, NNReal.toReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
ha : 0 ≤ a
ha' : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (σₙ ℝ a)

Tactic:
exact continuous_subtype_val.comp_continuousOn <|
    ContinuousOn.comp ‹_› continuous_real_toNNReal.continuousOn <| ha'.image ▸ Set.mapsTo_image ..

Premises used: Continuous.continuousOn, continuous_subtype_val, Continuous.comp_continuousOn, ContinuousOn.comp, continuous_real_toNNReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
ha : 0 ≤ a
ha' : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (σₙ ℝ a)

Tactic:
case hf_cont => exact continuous_subtype_val.comp_continuousOn <|
    ContinuousOn.comp ‹_› continuous_real_toNNReal.continuousOn <| ha'.image ▸ Set.mapsTo_image ..

Premises used: Continuous.continuousOn, continuous_subtype_val, Continuous.comp_continuousOn, ContinuousOn.comp, continuous_real_toNNReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
ha : 0 ≤ a
ha' : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ f '' σₙ ℝ≥0 a = (fun (x : ℝ) ↦ ‖(↑(f x.toNNReal) : ℝ)‖₊) '' σₙ ℝ a

Tactic:
simp [Set.image_image, ← ha'.image]

Premises used: Set.image_image, QuasispectrumRestricts.image
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
x : ℝ≥0
hx : x ∈ σₙ ℝ≥0 a
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
ha : 0 ≤ a
revert : ∀ (hx : x ∈ σₙ ℝ≥0 a), f x ≤ ‖cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a‖₊
⊢ f x ≤ ‖cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a‖₊

Tactic:
revert hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
x : ℝ≥0
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
ha : 0 ≤ a
⊢ ∀ (hx : x ∈ σₙ ℝ≥0 a), f x ≤ ‖cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a‖₊

Tactic:
(IsGreatest.nnnorm_cfcₙ_nnreal f a hf hf0 ha |>.2 ⟨x, ·, rfl⟩)

Premises used: IsGreatest.nnnorm_cfcₙ_nnreal, And.right, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
x : ℝ≥0
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
ha : 0 ≤ a
⊢ ∀ (hx : x ∈ σₙ ℝ≥0 a), f x ≤ ‖cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a‖₊

Tactic:
exact (IsGreatest.nnnorm_cfcₙ_nnreal f a hf hf0 ha |>.2 ⟨x, ·, rfl⟩)

Premises used: IsGreatest.nnnorm_cfcₙ_nnreal, And.right, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ ℝ≥0 a, f x ≤ c
⊢ (fun (x : A) ↦ ‖x‖₊ ≤ c) 0

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ ℝ≥0 a, f x ≤ c
refine :
  ∀ (hf : ContinuousOn f (σₙ ℝ≥0 a))
    (hf0 :
      Eq (α := ℝ≥0)
        (({ toFun := (σₙ ℝ≥0 a).restrict (π := fun (a : ℝ≥0) ↦ ℝ≥0) f, continuous_toFun := ⋯ :
              C((↑(σₙ ℝ≥0 a) : Type), ℝ≥0) } :
            (a : (↑(σₙ ℝ≥0 a) : Type)) → ℝ≥0)
          0)
        0)
    (ha : 0 ≤ a),
    (fun (x : A) ↦ ‖x‖₊ ≤ c)
      ((cfcₙHom (p := fun (x : A) ↦ 0 ≤ x) ha : (a : ContinuousMapZero (↑(σₙ ℝ≥0 a) : Type) ℝ≥0) → A)
        { toFun := (σₙ ℝ≥0 a).restrict (π := fun (a : ℝ≥0) ↦ ℝ≥0) f, continuous_toFun := ⋯, map_zero' := hf0 :
          ContinuousMapZero (↑(σₙ ℝ≥0 a) : Type) ℝ≥0 })
⊢ ‖cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ ≤ c

Tactic:
refine cfcₙ_cases (‖·‖₊ ≤ c) a f (by simp) fun hf hf0 ha ↦ ?_

Premises used: NNNorm.nnnorm, LE.le, cfcₙ_cases
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ ℝ≥0 a, f x ≤ c
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 :
  Eq (α := ℝ≥0)
    (({ toFun := (σₙ ℝ≥0 a).restrict (π := fun (a : ℝ≥0) ↦ ℝ≥0) f, continuous_toFun := ⋯ :
          C((↑(σₙ ℝ≥0 a) : Type), ℝ≥0) } :
        (a : (↑(σₙ ℝ≥0 a) : Type)) → ℝ≥0)
      0)
    0
ha : 0 ≤ a
simp : c ∈ upperBounds (f '' σₙ ℝ≥0 a)
⊢ nnnorm (E := A)
      ((cfcₙHom (p := fun (x : A) ↦ 0 ≤ x) ha : (a : ContinuousMapZero (↑(σₙ ℝ≥0 a) : Type) ℝ≥0) → A)
          { toFun := (σₙ ℝ≥0 a).restrict (π := fun (a : ℝ≥0) ↦ ℝ≥0) f, continuous_toFun := ⋯, map_zero' := hf0 :
            ContinuousMapZero (↑(σₙ ℝ≥0 a) : Type) ℝ≥0 } :
        A) ≤
    c

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

Premises used: IsGreatest.nnnorm_cfcₙ_nnreal, isLUB_le_iff, IsGreatest.isLUB, cfcₙ_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ ℝ≥0 a, f x ≤ c
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 :
  Eq (α := ℝ≥0)
    (({ toFun := (σₙ ℝ≥0 a).restrict (π := fun (a : ℝ≥0) ↦ ℝ≥0) f, continuous_toFun := ⋯ :
          C((↑(σₙ ℝ≥0 a) : Type), ℝ≥0) } :
        (a : (↑(σₙ ℝ≥0 a) : Type)) → ℝ≥0)
      0)
    0
ha : 0 ≤ a
x : ℝ≥0
hx : x ∈ σₙ ℝ≥0 a
⊢ f x ≤ c

Tactic:
h x hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ ℝ≥0 a, f x ≤ c
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 :
  Eq (α := ℝ≥0)
    (({ toFun := (σₙ ℝ≥0 a).restrict (π := fun (a : ℝ≥0) ↦ ℝ≥0) f, continuous_toFun := ⋯ :
          C((↑(σₙ ℝ≥0 a) : Type), ℝ≥0) } :
        (a : (↑(σₙ ℝ≥0 a) : Type)) → ℝ≥0)
      0)
    0
ha : 0 ≤ a
x : ℝ≥0
hx : x ∈ σₙ ℝ≥0 a
⊢ f x ≤ c

Tactic:
exact h x hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf₀ : f 0 = 0
ha : 0 ≤ a
⊢ ‖cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ ≤ c ↔ ∀ x ∈ σₙ ℝ≥0 a, f x ≤ c

Tactic:
⟨fun h _ hx ↦ apply_le_nnnorm_cfcₙ_nnreal f a hx hf hf₀ ha |>.trans h, nnnorm_cfcₙ_nnreal_le⟩

Premises used: Iff.intro, LE.le.trans, nnnorm_cfcₙ_nnreal_le, apply_le_nnnorm_cfcₙ_nnreal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ ℝ≥0 a, f x < c
⊢ ‖cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ < c

Tactic:
cfcₙ_cases (‖·‖₊ < c) a f ?_ fun hf hf0 ha ↦ ?_

Premises used: NNNorm.nnnorm, LT.lt, cfcₙ_cases