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 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : ContinuousStar A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst_8 : TopologicalSpace X
s : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
ha_cont : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
hs : ∀ (x : X), IsCompact (s x)
ha : ∀ (x₀ : X), ∀ᶠ (x : X) in 𝓝 x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
hf : ∀ (x : X), ContinuousOn f (s x)
hf0 : f 0 = 0
ha' : ∀ (x : X), p (a x)
rw :
  ∀ (ha_cont : ContinuousOn a Set.univ) (hs : ∀ (x : X), IsCompact (s x))
    (ha : ∀ (x₀ : X), ∀ᶠ (x : X) in 𝓝 x₀, quasispectrum 𝕜 (a x) ⊆ s x₀) (hf : ∀ (x : X), ContinuousOn f (s x))
    (hf0 : f 0 = 0) (ha' : ∀ (x : X), p (a x)),
    ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) f (a x)) Set.univ
⊢ Continuous[inst_8, 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 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : ContinuousStar A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst_8 : TopologicalSpace X
s : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
ha_cont : ContinuousOn a Set.univ
hs : ∀ (x : X), IsCompact (s x)
ha : ∀ (x₀ : X), ∀ᶠ (x : X) in 𝓝 x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
hf : ∀ (x : X), ContinuousOn f (s x)
hf0 : f 0 = 0
ha' : ∀ (x : X), p (a x)
x : X
h : Membership.mem (γ := Set X) Set.univ x
⊢ ∀ᶠ (x_1 : X) in 𝓝[Set.univ] x, quasispectrum 𝕜 (a x_1) ⊆ s x

Tactic:
simpa using ha x
-- 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 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : ContinuousStar A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst_8 : TopologicalSpace X
s : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
ha_cont : ContinuousOn a Set.univ
hs : ∀ (x : X), IsCompact (s x)
ha : ∀ (x₀ : X), ∀ᶠ (x : X) in 𝓝 x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
hf : ∀ (x : X), ContinuousOn f (s x)
hf0 : f 0 = 0
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ₙ f (fun x _ ↦ hs x) (fun x _ ↦ by simpa using 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 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : ContinuousStar A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst_8 : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
a : X → A
ha_cont : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s
hf : ContinuousOn f s
hf0 : f 0 = 0
ha' : ∀ (x : X), p (a x)
rw :
  ∀ (ha_cont : ContinuousOn a Set.univ) (ha : ∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s) (hf : ContinuousOn f s)
    (hf0 : f 0 = 0) (ha' : ∀ (x : X), p (a x)),
    ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) f (a x)) Set.univ
⊢ Continuous[inst_8, 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 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : ContinuousStar A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst_8 : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
a : X → A
ha_cont : ContinuousOn a Set.univ
ha : ∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s
hf : ContinuousOn f s
hf0 : f 0 = 0
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:
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 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : ContinuousStar A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst_8 : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
a : X → A
ha_cont : ContinuousOn a Set.univ
ha : ∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s
hf : ContinuousOn f s
hf0 : f 0 = 0
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 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : ContinuousStar A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst_8 : CompleteSpace A
inst_9 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ (x : X), quasispectrum 𝕜 (a x))) s
ha_cont : Continuous[inst_9, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha' : ∀ (x : X), p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
rw :
  ∀ (ha_cont : ContinuousOn a Set.univ) (ha' : ∀ (x : X), p (a x)) (hf : ContinuousOn f s) (hf0 : f 0 = 0),
    ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) f (a x)) Set.univ
⊢ Continuous[inst_9, 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 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : ContinuousStar A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst_8 : CompleteSpace A
inst_9 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ (x : X), quasispectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a Set.univ
ha' : ∀ (x : X), p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ (x : X), ⋃ (_ : Membership.mem (γ := Set X) Set.univ x), quasispectrum 𝕜 (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 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : ContinuousStar A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst_8 : CompleteSpace A
inst_9 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ (x : X), quasispectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a Set.univ
ha' : ∀ (x : X), p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ ∀ (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 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : ContinuousStar A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst_8 : CompleteSpace A
inst_9 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ (x : X), quasispectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a Set.univ
ha' : ∀ (x : X), p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ 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 : 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
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ Set.EqOn (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f) (cfcₙ (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
    {a : A | 0 ≤ a ∧ quasispectrum ℝ≥0 a ⊆ s}

Tactic:
have : {a : A | 0 ≤ a ∧ quasispectrum ℝ≥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 : 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
hf : ContinuousOn f s
hf0 : 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 ∧ quasispectrum ℝ≥0 a ⊆ s}
⊢ ContinuousOn (Y := A) (fun (x : A) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f x) {a : A | 0 ≤ a ∧ quasispectrum ℝ≥0 a ⊆ s}

Tactic:
ContinuousOn.congr ?_ this

Premises used: ContinuousOn.congr
-- 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
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
hf0 : 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 ∧ quasispectrum ℝ≥0 a ⊆ s}
refine :
  ContinuousOn (cfcₙ (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) {a : A | 0 ≤ a ∧ quasispectrum ℝ≥0 a ⊆ s}
⊢ ContinuousOn (Y := A) (fun (x : A) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f x) {a : A | 0 ≤ a ∧ quasispectrum ℝ≥0 a ⊆ s}

Tactic:
refine ContinuousOn.congr ?_ this

Premises used: ContinuousOn.congr
-- 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
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
hf0 : 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 ∧ quasispectrum ℝ≥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 : 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
hf : ContinuousOn f s
hf0 : 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 ∧ quasispectrum ℝ≥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 : 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
hf : ContinuousOn f s
hf0 : 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 ∧ quasispectrum ℝ≥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 : 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
hf : ContinuousOn f s
hf0 : 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 ∧ quasispectrum ℝ≥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 : 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
hf0 : 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 ∧ quasispectrum ℝ≥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 ∧ quasispectrum ℝ≥0 a ⊆ s}

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

Premises used: NNReal.continuous_coe, continuousOn_cfcₙ, ContinuousOn.mono, IsCompact.image
-- 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
f : ℝ≥0 → ℝ≥0
hf0 : 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 ∧ quasispectrum ℝ≥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 ∧ quasispectrum ℝ≥0 a ⊆ s} a),
    Membership.mem (γ := Set A) {a : A | IsSelfAdjoint a ∧ quasispectrum ℝ a ⊆ NNReal.toReal '' s} a
⊢ ContinuousOn (cfcₙ (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) {a : A | 0 ≤ a ∧ quasispectrum ℝ≥0 a ⊆ s}

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

Premises used: NNReal.continuous_coe, continuousOn_cfcₙ, ContinuousOn.mono, IsCompact.image
-- 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
f : ℝ≥0 → ℝ≥0
hf0 : 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 ∧ quasispectrum ℝ≥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 ∧ quasispectrum ℝ≥0 a ⊆ s} a
⊢ (IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)) ∧
    quasispectrum ℝ≥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 : 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
hf0 : 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 ∧ quasispectrum ℝ≥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)) ∧
    quasispectrum ℝ≥0 a ⊆ s
⊢ IsSelfAdjoint a ∧ quasispectrum ℝ 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 : 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
hf0 : 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 ∧ quasispectrum ℝ≥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)) ∧
    quasispectrum ℝ≥0 a ⊆ s
refine : quasispectrum ℝ a ⊆ NNReal.toReal '' s
⊢ IsSelfAdjoint a ∧ quasispectrum ℝ a ⊆ NNReal.toReal '' s

Tactic:
refine ⟨ha.1.1, ?_⟩
-- 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
f : ℝ≥0 → ℝ≥0
hf0 : 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 ∧ quasispectrum ℝ≥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)) ∧
    quasispectrum ℝ≥0 a ⊆ s
rw : (⇑(algebraMap ℝ≥0 ℝ) : (a : ℝ≥0) → ℝ) '' quasispectrum ℝ≥0 a ⊆ NNReal.toReal '' s
⊢ quasispectrum ℝ a ⊆ NNReal.toReal '' s

Tactic:
rw [← ha.1.2.algebraMap_image]

Premises used: QuasispectrumRestricts.algebraMap_image, And.right, And.left
-- 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
f : ℝ≥0 → ℝ≥0
hf0 : 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 ∧ quasispectrum ℝ≥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)) ∧
    quasispectrum ℝ≥0 a ⊆ s
⊢ (⇑(algebraMap ℝ≥0 ℝ) : (a : ℝ≥0) → ℝ) '' quasispectrum ℝ≥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 : 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
hf0 : 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 ∧ quasispectrum ℝ≥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)) ∧
    quasispectrum ℝ≥0 a ⊆ s
⊢ (⇑(algebraMap ℝ≥0 ℝ) : (a : ℝ≥0) → ℝ) '' quasispectrum ℝ≥0 a ⊆ NNReal.toReal '' s

Tactic:
exact Set.image_mono ha.2

Premises used: Set.image_mono, And.right