awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : TopologicalSpace X
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
x₀ : X
t : Set X
hx₀ : x₀ ∈ t
ha_cont : ContinuousWithinAt a t x₀
ha : ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in 𝓝[t] x₀, 0 ≤ a x
hf : ContinuousOn f s
⊢ ContinuousWithinAt.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfc (p := fun (x : A) ↦ 0 ≤ x) f (a x)) t x₀

Tactic:
ha_cont.tendsto.cfc_nnreal hs f ha ha' (ha.self_of_nhdsWithin hx₀) (ha'.self_of_nhdsWithin hx₀)

Premises used: Filter.Eventually.self_of_nhdsWithin, ContinuousWithinAt, Filter.Tendsto.cfc_nnreal, ContinuousWithinAt.tendsto
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ContinuousOn a t
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
⊢ ∀ x ∈ t, ContinuousWithinAt a t x

Tactic:
rw [ContinuousOn] at ha_cont ⊢

Premises used: ContinuousOn
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ContinuousOn a t
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
ha_cont₁ : ∀ x ∈ t, ContinuousWithinAt a t x
⊢ ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s x₀

Tactic:
rw [ContinuousOn] at ha_cont ⊢

Premises used: ContinuousOn
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ContinuousOn a t
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
ha_cont₁ : ∀ x ∈ t, ContinuousWithinAt a t x
ha₁ : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
⊢ ∀ x ∈ t, 0 ≤ a x

Tactic:
rw [ContinuousOn] at ha_cont ⊢

Premises used: ContinuousOn
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ContinuousOn a t
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
ha_cont₁ : ∀ x ∈ t, ContinuousWithinAt a t x
ha₁ : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
ha'₁ : ∀ x ∈ t, 0 ≤ a x
⊢ ∀ x ∈ t, ContinuousOn f (s x)

Tactic:
rw [ContinuousOn] at ha_cont ⊢

Premises used: ContinuousOn
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
⊢ ∀ x ∈ t, ContinuousWithinAt.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfc (p := fun (x : A) ↦ 0 ≤ x) f (a x)) t x

Tactic:
fun x hx ↦ (ha_cont x hx).cfc_nnreal (hs x hx) f hx ?_ ?_ (hf x hx)

Premises used: ContinuousWithinAt.cfc_nnreal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
refine_1 : ∀ (x : X) (hx : x ∈ t), ∀ᶠ (x_1 : X) in 𝓝[t] x, spectrum ℝ≥0 (a x_1) ⊆ s x
refine_2 : ∀ (x : X) (hx : x ∈ t), ∀ᶠ (x : X) in 𝓝[t] x, 0 ≤ a x
⊢ ∀ x ∈ t, ContinuousWithinAt.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfc (p := fun (x : A) ↦ 0 ≤ x) f (a x)) t x

Tactic:
refine fun x hx ↦ (ha_cont x hx).cfc_nnreal (hs x hx) f hx ?_ ?_ (hf x hx)

Premises used: ContinuousWithinAt.cfc_nnreal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
x : X
hx : x ∈ t
h : ∀ (x_1 : X) (hx : spectrum ℝ≥0 (a x_1) ⊆ s x) (hxt : x_1 ∈ t), spectrum ℝ≥0 (a x_1) ⊆ s x
⊢ ∀ᶠ (x_1 : X) in 𝓝[t] x, spectrum ℝ≥0 (a x_1) ⊆ s x

Tactic:
filter_upwards [ha x hx, self_mem_nhdsWithin] with x hx hxt

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
x : X
hx : x ∈ t
h : ∀ (x_1 : X) (hx : spectrum ℝ≥0 (a x_1) ⊆ s x) (hxt : x_1 ∈ t), 0 ≤ a x_1
⊢ ∀ᶠ (x : X) in 𝓝[t] x, 0 ≤ a x

Tactic:
filter_upwards [ha x hx, self_mem_nhdsWithin] with x hx hxt

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
x_1 : X
hx_1 : x_1 ∈ t
x : X
hx : spectrum ℝ≥0 (a x) ⊆ s x_1
hxt : x ∈ t
⊢ spectrum ℝ≥0 (a x) ⊆ s x_1

Tactic:
hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
x_1 : X
hx_1 : x_1 ∈ t
x : X
hx : spectrum ℝ≥0 (a x) ⊆ s x_1
hxt : x ∈ t
⊢ 0 ≤ a x

Tactic:
ha' x hxt
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
x_1 : X
hx_1 : x_1 ∈ t
x : X
hx : spectrum ℝ≥0 (a x) ⊆ s x_1
hxt : x ∈ t
⊢ spectrum ℝ≥0 (a x) ⊆ s x_1

Tactic:
exacts [hx, ha' x hxt]
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : TopologicalSpace X
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
ha_cont : ContinuousOn a t
ha : ∀ x ∈ t, spectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
⊢ ContinuousOn.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfc (p := fun (x : A) ↦ 0 ≤ x) f (a x)) t

Tactic:
ContinuousOn.cfc_nnreal _ (fun _ _ ↦ hs) ha_cont (fun _ _ ↦ ?_) ha'

Premises used: ContinuousOn.cfc_nnreal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : TopologicalSpace X
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
ha_cont : ContinuousOn a t
ha : ∀ x ∈ t, spectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
refine : ∀ x ∈ t, ∀ᶠ (x : X) in 𝓝[t] x, spectrum ℝ≥0 (a x) ⊆ s
⊢ ContinuousOn.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfc (p := fun (x : A) ↦ 0 ≤ x) f (a x)) t

Tactic:
refine ContinuousOn.cfc_nnreal _ (fun _ _ ↦ hs) ha_cont (fun _ _ ↦ ?_) ha'

Premises used: ContinuousOn.cfc_nnreal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : TopologicalSpace X
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
ha_cont : ContinuousOn a t
ha : ∀ x ∈ t, spectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
x : X
h_1 : x ∈ t
h : ∀ (x : X) (hx : x ∈ t), spectrum ℝ≥0 (a x) ⊆ s
⊢ ∀ᶠ (x : X) in 𝓝[t] x, spectrum ℝ≥0 (a x) ⊆ s

Tactic:
filter_upwards [self_mem_nhdsWithin] with x hx

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : TopologicalSpace X
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
ha_cont : ContinuousOn a t
ha : ∀ x ∈ t, spectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
x_1 : X
h : x_1 ∈ t
x : X
hx : x ∈ t
⊢ spectrum ℝ≥0 (a x) ⊆ s

Tactic:
ha x hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : TopologicalSpace X
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
ha_cont : ContinuousOn a t
ha : ∀ x ∈ t, spectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
x_1 : X
h : x_1 ∈ t
x : X
hx : x ∈ t
⊢ spectrum ℝ≥0 (a x) ⊆ s

Tactic:
exact ha x hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : CompleteSpace A
inst_11 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, spectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
⊢ Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, spectrum ℝ≥0 (a x))) s

Tactic:
have hs' := hs
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : CompleteSpace A
inst_11 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, spectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hs' : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, spectrum ℝ≥0 (a x))) s
⊢ ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (spectrum ℝ≥0 (a i))

Tactic:
simp only [nhdsSet_iUnion, mem_iSup] at hs'

Premises used: nhdsSet_iUnion, Filter.mem_iSup
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : CompleteSpace A
inst_11 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, spectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (spectrum ℝ≥0 (a i))
x : (↑t : Type u_1)
obtain :
  ∀ (S : Set ℝ≥0) (hS₃ : id S ⊆ s) (hS₁ : S ∈ 𝓝ˢ (spectrum ℝ≥0 (a (↑x : X)))) (hS₂ : IsCompact S),
    ∃ (S : Set ℝ≥0), IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), spectrum ℝ≥0 x' ⊆ S) ∧ S ⊆ s
⊢ ∃ (S : Set ℝ≥0), IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), spectrum ℝ≥0 x' ⊆ S) ∧ S ⊆ s

Tactic:
obtain ⟨S, ⟨hS₁, hS₂⟩, hS₃⟩ :=
      spectrum.isCompact_nnreal (a x) |>.nhdsSet_basis_isCompact.mem_iff.mp (hs' x x.2)

Premises used: Filter.HasBasis.mem_iff, Iff.mp, spectrum.isCompact_nnreal, Subtype.val, Subtype.property, IsCompact.nhdsSet_basis_isCompact
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : CompleteSpace A
inst_11 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, spectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (spectrum ℝ≥0 (a i))
x : (↑t : Type u_1)
S : Set ℝ≥0
hS₃ : id S ⊆ s
hS₁ : S ∈ 𝓝ˢ (spectrum ℝ≥0 (a (↑x : X)))
hS₂ : IsCompact S
⊢ ∃ (S : Set ℝ≥0), IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), spectrum ℝ≥0 x' ⊆ S) ∧ S ⊆ s

Tactic:
⟨S, hS₂, ?_, hS₃⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : CompleteSpace A
inst_11 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, spectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (spectrum ℝ≥0 (a i))
x : (↑t : Type u_1)
S : Set ℝ≥0
hS₃ : id S ⊆ s
hS₁ : S ∈ 𝓝ˢ (spectrum ℝ≥0 (a (↑x : X)))
hS₂ : IsCompact S
refine : ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), spectrum ℝ≥0 x' ⊆ S
⊢ ∃ (S : Set ℝ≥0), IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), spectrum ℝ≥0 x' ⊆ S) ∧ S ⊆ s

Tactic:
refine ⟨S, hS₂, ?_, hS₃⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : CompleteSpace A
inst_11 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, spectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (spectrum ℝ≥0 (a i))
x : (↑t : Type u_1)
S : Set ℝ≥0
hS₃ : id S ⊆ s
hS₁ : S ∈ 𝓝ˢ (spectrum ℝ≥0 (a (↑x : X)))
hS₂ : IsCompact S
⊢ ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), spectrum ℝ≥0 x' ⊆ S

Tactic:
upperHemicontinuous_spectrum_nnreal A |>.upperHemicontinuousAt (a x) _ hS₁ |>.mono
      fun _ ↦ subset_of_mem_nhdsSet

Premises used: subset_of_mem_nhdsSet, Filter.Eventually.mono, upperHemicontinuous_spectrum_nnreal, UpperHemicontinuous.upperHemicontinuousAt, Subtype.val
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : CompleteSpace A
inst_11 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, spectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (spectrum ℝ≥0 (a i))
x : (↑t : Type u_1)
S : Set ℝ≥0
hS₃ : id S ⊆ s
hS₁ : S ∈ 𝓝ˢ (spectrum ℝ≥0 (a (↑x : X)))
hS₂ : IsCompact S
⊢ ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), spectrum ℝ≥0 x' ⊆ S

Tactic:
exact upperHemicontinuous_spectrum_nnreal A |>.upperHemicontinuousAt (a x) _ hS₁ |>.mono
      fun _ ↦ subset_of_mem_nhdsSet

Premises used: subset_of_mem_nhdsSet, Filter.Eventually.mono, upperHemicontinuous_spectrum_nnreal, UpperHemicontinuous.upperHemicontinuousAt, Subtype.val
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : CompleteSpace A
inst_11 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, spectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (spectrum ℝ≥0 (a i))
⊢ ∀ (x : (↑t : Type u_1)), ∃ (S : Set ℝ≥0), IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), spectrum ℝ≥0 x' ⊆ S) ∧ S ⊆ s

Tactic:
have (x : t) : ∃ S, IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a x), spectrum ℝ≥0 x' ⊆ S) ∧ S ⊆ s := by
    obtain ⟨S, ⟨hS₁, hS₂⟩, hS₃⟩ :=
      spectrum.isCompact_nnreal (a x) |>.nhdsSet_basis_isCompact.mem_iff.mp (hs' x x.2)
    refine ⟨S, hS₂, ?_, hS₃⟩
    exact upperHemicontinuous_spectrum_nnreal A |>.upperHemicontinuousAt (a x) _ hS₁ |>.mono
      fun _ ↦ subset_of_mem_nhdsSet
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
inst_10 : CompleteSpace A
inst_11 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, spectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (spectrum ℝ≥0 (a i))
this :
  ∀ (x : (↑t : Type u_1)), ∃ (S : Set ℝ≥0), IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), spectrum ℝ≥0 x' ⊆ S) ∧ S ⊆ s
choose :
  ∀ (S : (x : (↑t : Type u_1)) → Set ℝ≥0) (hS₁ : ∀ (x : (↑t : Type u_1)), IsCompact (S x))
    (hS₂ : ∀ (x : (↑t : Type u_1)), ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), spectrum ℝ≥0 x' ⊆ S x)
    (hS₃ : ∀ (x : (↑t : Type u_1)), S x ⊆ s),
    ContinuousOn.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfc (p := fun (x : A) ↦ 0 ≤ x) f (a x)) t
⊢ ContinuousOn.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfc (p := fun (x : A) ↦ 0 ≤ x) f (a x)) t

Tactic:
choose S hS₁ hS₂ hS₃ using this