awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
a : X → A
ha_cont : ContinuousOn a Set.univ
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
hf : ContinuousOn f s
ha' : ∀ (x : X), p (a x)
⊢ ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfc (p := p) f (a x)) Set.univ

Tactic:
exact ha_cont.cfc' hs f (fun x _ ↦ ha x) (fun x _ ↦ ha' x)

Premises used: ContinuousOn.cfc'
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : CompleteSpace A
inst_7 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ (x : X), spectrum 𝕜 (a x))) s
ha_cont : Continuous[inst_7, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha' : ∀ (x : X), p (a x)
hf : ContinuousOn f s
rw :
  ∀ (ha_cont : ContinuousOn a Set.univ) (ha' : ∀ (x : X), p (a x)) (hf : ContinuousOn f s),
    ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfc (p := p) f (a x)) Set.univ
⊢ Continuous[inst_7, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦ cfc (p := p) f (a x)

Tactic:
rw [← continuousOn_univ] at ha_cont ⊢

Premises used: continuousOn_univ
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : CompleteSpace A
inst_7 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ (x : X), spectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a Set.univ
ha' : ∀ (x : X), p (a x)
hf : ContinuousOn f s
⊢ Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ (x : X), ⋃ (_ : Membership.mem (γ := Set X) Set.univ x), spectrum 𝕜 (a x))) s

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : CompleteSpace A
inst_7 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ (x : X), spectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a Set.univ
ha' : ∀ (x : X), p (a x)
hf : ContinuousOn f s
⊢ ∀ (x : X), Membership.mem (γ := Set X) Set.univ x → p (a x)

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : CompleteSpace A
inst_7 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ (x : X), spectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a Set.univ
ha' : ∀ (x : X), p (a x)
hf : ContinuousOn f s
⊢ ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfc (p := p) f (a x)) Set.univ

Tactic:
exact ha_cont.cfc_of_mem_nhdsSet f (by simpa) (by simpa)

Premises used: ContinuousOn.cfc_of_mem_nhdsSet
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
⊢ Set.EqOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
    {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}

Tactic:
have : {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}.EqOn (cfc f) (cfc (fun x : ℝ ↦ f x.toNNReal)) :=
    fun a ha ↦ cfc_nnreal_eq_real _ _ ha.1
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
this :
  Set.EqOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
    {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
⊢ ContinuousOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}

Tactic:
ContinuousOn.congr ?_ this

Premises used: ContinuousOn.congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
this :
  Set.EqOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
    {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
refine :
  ContinuousOn (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
⊢ ContinuousOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}

Tactic:
refine ContinuousOn.congr ?_ this

Premises used: ContinuousOn.congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
this :
  Set.EqOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
    {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
apply : Set.MapsTo Real.toNNReal (NNReal.toReal '' s) s
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (NNReal.toReal '' s)

Tactic:
apply hf.ofReal_map_toNNReal

Premises used: ContinuousOn.ofReal_map_toNNReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
this :
  Set.EqOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
    {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
rw : Set.MapsTo (Real.toNNReal ∘ NNReal.toReal) s s
⊢ Set.MapsTo Real.toNNReal (NNReal.toReal '' s) s

Tactic:
rw [Set.mapsTo_image_iff]

Premises used: Set.mapsTo_image_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
this :
  Set.EqOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
    {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
x : ℝ≥0
hx : x ∈ s
⊢ (Real.toNNReal ∘ NNReal.toReal) x ∈ s

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
this :
  Set.EqOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
    {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (NNReal.toReal '' s)

Tactic:
replace hf : ContinuousOn (fun x ↦ f x.toNNReal : ℝ → ℝ) (NNReal.toReal '' s) := by
    apply hf.ofReal_map_toNNReal
    rw [Set.mapsTo_image_iff]
    intro x hx
    simpa
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
this :
  Set.EqOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
    {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
hf : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (NNReal.toReal '' s)
⊢ ContinuousOn (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}

Tactic:
continuousOn_cfc A (hs.image NNReal.continuous_coe) _ hf |>.mono fun a ha ↦ ?_

Premises used: NNReal.continuous_coe, ContinuousOn.mono, continuousOn_cfc, IsCompact.image
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
this :
  Set.EqOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
    {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
hf : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (NNReal.toReal '' s)
refine :
  ∀ (a : A) (ha : Membership.mem (γ := Set A) {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s} a),
    Membership.mem (γ := Set A) {a : A | IsSelfAdjoint a ∧ spectrum ℝ a ⊆ NNReal.toReal '' s} a
⊢ ContinuousOn (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}

Tactic:
refine continuousOn_cfc A (hs.image NNReal.continuous_coe) _ hf |>.mono fun a ha ↦ ?_

Premises used: NNReal.continuous_coe, ContinuousOn.mono, continuousOn_cfc, IsCompact.image
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
this :
  Set.EqOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
    {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
hf : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (NNReal.toReal '' s)
a : A
ha : Membership.mem (γ := Set A) {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s} a
⊢ (IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)) ∧
    spectrum ℝ≥0 a ⊆ s

Tactic:
simp only [Set.mem_setOf_eq, nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts] at ha ⊢

Premises used: Set.mem_setOf_eq, nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
this :
  Set.EqOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
    {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
hf : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (NNReal.toReal '' s)
a : A
ha :
  (IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)) ∧
    spectrum ℝ≥0 a ⊆ s
⊢ (IsSelfAdjoint a ∧ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)) ∧
    spectrum ℝ≥0 a ⊆ s

Tactic:
rw [← SpectrumRestricts] at ha

Premises used: SpectrumRestricts
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
this :
  Set.EqOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
    {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
hf : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (NNReal.toReal '' s)
a : A
ha :
  (IsSelfAdjoint a ∧ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)) ∧
    spectrum ℝ≥0 a ⊆ s
⊢ IsSelfAdjoint a ∧ spectrum ℝ a ⊆ NNReal.toReal '' s

Tactic:
⟨ha.1.1, ?_⟩

Premises used: And.left, And.intro
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
this :
  Set.EqOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
    {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
hf : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (NNReal.toReal '' s)
a : A
ha :
  (IsSelfAdjoint a ∧ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)) ∧
    spectrum ℝ≥0 a ⊆ s
refine : spectrum ℝ a ⊆ NNReal.toReal '' s
⊢ IsSelfAdjoint a ∧ spectrum ℝ a ⊆ NNReal.toReal '' s

Tactic:
refine ⟨ha.1.1, ?_⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
this :
  Set.EqOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
    {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
hf : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (NNReal.toReal '' s)
a : A
ha :
  (IsSelfAdjoint a ∧ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)) ∧
    spectrum ℝ≥0 a ⊆ s
rw : (⇑(algebraMap ℝ≥0 ℝ) : (a : ℝ≥0) → ℝ) '' spectrum ℝ≥0 a ⊆ NNReal.toReal '' s
⊢ spectrum ℝ a ⊆ NNReal.toReal '' s

Tactic:
rw [← ha.1.2.algebraMap_image]

Premises used: SpectrumRestricts.algebraMap_image, And.right, And.left
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
this :
  Set.EqOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
    {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
hf : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (NNReal.toReal '' s)
a : A
ha :
  (IsSelfAdjoint a ∧ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)) ∧
    spectrum ℝ≥0 a ⊆ s
⊢ (⇑(algebraMap ℝ≥0 ℝ) : (a : ℝ≥0) → ℝ) '' spectrum ℝ≥0 a ⊆ NNReal.toReal '' s

Tactic:
Set.image_mono ha.2

Premises used: Set.image_mono, NNReal, And.right, NNReal.toReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
this :
  Set.EqOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
    {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
hf : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (NNReal.toReal '' s)
a : A
ha :
  (IsSelfAdjoint a ∧ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)) ∧
    spectrum ℝ≥0 a ⊆ s
⊢ (⇑(algebraMap ℝ≥0 ℝ) : (a : ℝ≥0) → ℝ) '' spectrum ℝ≥0 a ⊆ NNReal.toReal '' s

Tactic:
exact Set.image_mono ha.2

Premises used: Set.image_mono, And.right
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
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
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}
      {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s})

Tactic:
continuousOn_prod_of_continuousOn_lipschitzOnWith _ 1
    (fun f hf ↦ continuousOn_cfc_nnreal A hs ((toFun {s}) f) hf)
    (fun a ⟨_, ha'⟩ ↦ lipschitzOnWith_cfc_fun_of_subset a ha')

Premises used: cfc, setOf, lipschitzOnWith_cfc_fun_of_subset, _private.0.continuousOn_cfc_nnreal_setProd.match_1, continuousOn_cfc_nnreal, continuousOn_prod_of_continuousOn_lipschitzOnWith, Prod.mk, UniformOnFun.toFun, Prod.fst, LipschitzOnWith, ContinuousOn, Singleton.singleton, OfNat.ofNat, Prod.snd, DFunLike.coe
-- 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
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, spectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in l, 0 ≤ a x
ha₀ : spectrum ℝ≥0 a₀ ⊆ s
ha₀' : 0 ≤ a₀
hf : ContinuousOn f s
apply : Tendsto a l (𝓝[{a : A | 0 ≤ a ∧ spectrum ℝ≥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: continuousOn_cfc_nnreal, And.intro, Filter.Tendsto.comp, ContinuousWithinAt.tendsto, ContinuousOn.continuousWithinAt
-- 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
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, spectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in l, 0 ≤ a x
ha₀ : spectrum ℝ≥0 a₀ ⊆ s
ha₀' : 0 ≤ a₀
hf : ContinuousOn f s
rw : Tendsto a l (𝓝 a₀) ∧ ∀ᶠ (n : X) in l, Membership.mem (γ := Set A) {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s} (a n)
⊢ Tendsto a l (𝓝[{a : A | 0 ≤ a ∧ spectrum ℝ≥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 : 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
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, spectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in l, 0 ≤ a x
ha₀ : spectrum ℝ≥0 a₀ ⊆ s
ha₀' : 0 ≤ a₀
hf : ContinuousOn f s
⊢ Tendsto a l (𝓝 a₀) ∧ ∀ᶠ (n : X) in l, Membership.mem (γ := Set A) {a : A | 0 ≤ a ∧ spectrum ℝ≥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 : 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
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, spectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in l, 0 ≤ a x
ha₀ : spectrum ℝ≥0 a₀ ⊆ s
ha₀' : 0 ≤ a₀
hf : ContinuousOn f s
⊢ Tendsto a l (𝓝 a₀) ∧ ∀ᶠ (n : X) in l, Membership.mem (γ := Set A) {a : A | 0 ≤ a ∧ spectrum ℝ≥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 : 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
ha_cont : ContinuousAt a x₀
ha : ∀ᶠ (x : X) in 𝓝 x₀, spectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in 𝓝 x₀, 0 ≤ a x
hf : ContinuousOn f s
⊢ 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, ContinuousAt.tendsto, Filter.Tendsto.cfc_nnreal