awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
⊢ ContinuousOn (Y := A)
    (fun (fa : (ℝ≥0 →ᵤ[{s}] ℝ≥0) × A) ↦
      cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) ((toFun {s} : (a : ℝ≥0 →ᵤ[{s}] ℝ≥0) → ℝ≥0 → ℝ≥0) fa.1) fa.2)
    (SProd.sprod (α := Set (ℝ≥0 →ᵤ[{s}] ℝ≥0)) (β := Set A)
      {f : ℝ≥0 →ᵤ[{s}] ℝ≥0 | ContinuousOn (Y := ℝ≥0) ((toFun {s} : (a : ℝ≥0 →ᵤ[{s}] ℝ≥0) → ℝ≥0 → ℝ≥0) f) s ∧ f 0 = 0}
      {a : A | 0 ≤ a ∧ quasispectrum ℝ≥0 a ⊆ s})

Tactic:
continuousOn_prod_of_continuousOn_lipschitzOnWith _ 1
    (fun f hf ↦ continuousOn_cfcₙ_nnreal A hs ((toFun {s}) f) hf.1 hf.2)
    (fun a ⟨_, ha'⟩ ↦ lipschitzOnWith_cfcₙ_fun_of_subset a ha')

Premises used: cfcₙ, _private.0.continuousOn_cfcₙ_nnreal_setProd.match_1, setOf, continuousOn_prod_of_continuousOn_lipschitzOnWith, Prod.mk, UniformOnFun.toFun, Prod.fst, And, And.right, And.left, lipschitzOnWith_cfcₙ_fun_of_subset, LipschitzOnWith, continuousOn_cfcₙ_nnreal, ContinuousOn, Singleton.singleton, OfNat.ofNat, Eq, Prod.snd, DFunLike.coe
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
a₀ : A
l : Filter X
ha_tendsto : Tendsto a l (𝓝 a₀)
ha : ∀ᶠ (x : X) in l, quasispectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in l, 0 ≤ a x
ha₀ : quasispectrum ℝ≥0 a₀ ⊆ s
ha₀' : 0 ≤ a₀
hf : ContinuousOn f s
hf0 : f 0 = 0
apply : Tendsto a l (𝓝[{a : A | 0 ≤ a ∧ quasispectrum ℝ≥0 a ⊆ s}] a₀)
⊢ Tendsto (fun (x : X) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (a x)) l (𝓝 (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a₀))

Tactic:
apply continuousOn_cfcₙ_nnreal A hs f |>.continuousWithinAt ⟨ha₀', ha₀⟩ |>.tendsto.comp

Premises used: And.intro, continuousOn_cfcₙ_nnreal, Filter.Tendsto.comp, ContinuousWithinAt.tendsto, ContinuousOn.continuousWithinAt
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
a₀ : A
l : Filter X
ha_tendsto : Tendsto a l (𝓝 a₀)
ha : ∀ᶠ (x : X) in l, quasispectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in l, 0 ≤ a x
ha₀ : quasispectrum ℝ≥0 a₀ ⊆ s
ha₀' : 0 ≤ a₀
hf : ContinuousOn f s
hf0 : f 0 = 0
rw : Tendsto a l (𝓝 a₀) ∧ ∀ᶠ (n : X) in l, Membership.mem (γ := Set A) {a : A | 0 ≤ a ∧ quasispectrum ℝ≥0 a ⊆ s} (a n)
⊢ Tendsto a l (𝓝[{a : A | 0 ≤ a ∧ quasispectrum ℝ≥0 a ⊆ s}] a₀)

Tactic:
rw [tendsto_nhdsWithin_iff]

Premises used: tendsto_nhdsWithin_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
a₀ : A
l : Filter X
ha_tendsto : Tendsto a l (𝓝 a₀)
ha : ∀ᶠ (x : X) in l, quasispectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in l, 0 ≤ a x
ha₀ : quasispectrum ℝ≥0 a₀ ⊆ s
ha₀' : 0 ≤ a₀
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ Tendsto a l (𝓝 a₀) ∧ ∀ᶠ (n : X) in l, Membership.mem (γ := Set A) {a : A | 0 ≤ a ∧ quasispectrum ℝ≥0 a ⊆ s} (a n)

Tactic:
⟨ha_tendsto, ha'.and ha⟩

Premises used: Filter.Eventually.and, And.intro
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
a₀ : A
l : Filter X
ha_tendsto : Tendsto a l (𝓝 a₀)
ha : ∀ᶠ (x : X) in l, quasispectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in l, 0 ≤ a x
ha₀ : quasispectrum ℝ≥0 a₀ ⊆ s
ha₀' : 0 ≤ a₀
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ Tendsto a l (𝓝 a₀) ∧ ∀ᶠ (n : X) in l, Membership.mem (γ := Set A) {a : A | 0 ≤ a ∧ quasispectrum ℝ≥0 a ⊆ s} (a n)

Tactic:
exact ⟨ha_tendsto, ha'.and ha⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : TopologicalSpace X
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
x₀ : X
ha_cont : ContinuousAt a x₀
ha : ∀ᶠ (x : X) in 𝓝 x₀, quasispectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in 𝓝 x₀, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ ContinuousAt.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (a x)) x₀

Tactic:
ha_cont.tendsto.cfcₙ_nnreal hs f ha ha' ha.self_of_nhds ha'.self_of_nhds

Premises used: Filter.Eventually.self_of_nhds, ContinuousAt, Filter.Tendsto.cfcₙ_nnreal, ContinuousAt.tendsto
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : 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₀, quasispectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in 𝓝[t] x₀, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ 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 : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : 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₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
⊢ ∀ 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 : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : 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₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
ha_cont₁ : ∀ x ∈ t, ContinuousWithinAt a t x
⊢ ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum ℝ≥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 : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : 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₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
ha_cont₁ : ∀ x ∈ t, ContinuousWithinAt a t x
ha₁ : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum ℝ≥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 : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : 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₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
ha_cont₁ : ∀ x ∈ t, ContinuousWithinAt a t x
ha₁ : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum ℝ≥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 : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : 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₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
ha_cont₁ : ∀ x ∈ t, ContinuousWithinAt a t x
ha₁ : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
ha'₁ : ∀ x ∈ t, 0 ≤ a x
hf₁ : ∀ x ∈ t, ContinuousOn f (s x)
⊢ f 0 = 0

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 : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : 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₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
⊢ ∀ 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 : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : 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₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
refine_1 : ∀ (x : X) (hx : x ∈ t), ∀ᶠ (x_1 : X) in 𝓝[t] x, quasispectrum ℝ≥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 : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : 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₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
x : X
hx : x ∈ t
h : ∀ (x_1 : X) (hx : quasispectrum ℝ≥0 (a x_1) ⊆ s x) (hxt : x_1 ∈ t), quasispectrum ℝ≥0 (a x_1) ⊆ s x
⊢ ∀ᶠ (x_1 : X) in 𝓝[t] x, quasispectrum ℝ≥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 : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : 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₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
x : X
hx : x ∈ t
h : ∀ (x_1 : X) (hx : quasispectrum ℝ≥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 : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : 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₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
x_1 : X
hx_1 : x_1 ∈ t
x : X
hx : quasispectrum ℝ≥0 (a x) ⊆ s x_1
hxt : x ∈ t
⊢ quasispectrum ℝ≥0 (a x) ⊆ s x_1

Tactic:
hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : 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₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
x_1 : X
hx_1 : x_1 ∈ t
x : X
hx : quasispectrum ℝ≥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 : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : 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₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
x_1 : X
hx_1 : x_1 ∈ t
x : X
hx : quasispectrum ℝ≥0 (a x) ⊆ s x_1
hxt : x ∈ t
⊢ quasispectrum ℝ≥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 : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : 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, quasispectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ 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 : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : 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, quasispectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
refine : ∀ x ∈ t, ∀ᶠ (x : X) in 𝓝[t] x, quasispectrum ℝ≥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 : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : 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, quasispectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
x : X
h_1 : x ∈ t
h : ∀ (x : X) (hx : x ∈ t), quasispectrum ℝ≥0 (a x) ⊆ s
⊢ ∀ᶠ (x : X) in 𝓝[t] x, quasispectrum ℝ≥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 : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : 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, quasispectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
x_1 : X
h : x_1 ∈ t
x : X
hx : x ∈ t
⊢ quasispectrum ℝ≥0 (a x) ⊆ s

Tactic:
ha x hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : 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, quasispectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
x_1 : X
h : x_1 ∈ t
x : X
hx : x ∈ t
⊢ quasispectrum ℝ≥0 (a x) ⊆ s

Tactic:
exact ha x hx