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
a : X → A
ha_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
star_id : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦ star (a x)
⊢ Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A)
      (star (ContinuousMap.restrict s (ContinuousMap.id 𝕜)))

Tactic:
simp only [map_star, cfcHomSuperset_id]

Premises used: StarHomClass.map_star, cfcHomSuperset_id
-- 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
a : X → A
ha_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
⊢ Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦ star (a x)

Tactic:
fun_prop
-- 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
a : X → A
ha_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
f g : C((↑s : Type u_2), 𝕜)
hf :
  Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) f
hg :
  Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g
⊢ Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) (f + g)

Tactic:
simpa using hf.add hg

Premises used: Continuous.add
-- 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
a : X → A
ha_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
f g : C((↑s : Type u_2), 𝕜)
hf :
  Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) f
hg :
  Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g
⊢ Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) (f * g)

Tactic:
simpa using hf.mul hg

Premises used: Continuous.mul
-- 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
a : X → A
ha_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
f : C((↑s : Type u_2), 𝕜)
hf :
  ∃ᶠ (g : C((↑s : Type u_2), 𝕜)) in 𝓝 f,
    Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g
frequently :
  ∀ u ∈ uniformity A,
    ∃ (F : X → A),
      Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
        ∀ (y : X),
          Membership.mem (α := A × A) u
            (((cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) f, F y) : A × A)
⊢ Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) f

Tactic:
apply continuous_of_uniform_approx_of_continuous

Premises used: continuous_of_uniform_approx_of_continuous
-- 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
a : X → A
ha_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
f : C((↑s : Type u_2), 𝕜)
hf :
  ∃ᶠ (g : C((↑s : Type u_2), 𝕜)) in 𝓝 f,
    Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g
⊢ ∀ ⦃s_1 t : Set (A × A)⦄,
    s_1 ⊆ t →
      (∃ (F : X → A),
          Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
            ∀ (y : X),
              Membership.mem (α := A × A) s_1
                (((cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) f, F y) : A × A)) →
        ∃ (F : X → A),
          Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
            ∀ (y : X),
              Membership.mem (α := A × A) t
                (((cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) f, F y) : A × A)

Tactic:
aesop
-- 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
a : X → A
ha_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
f : C((↑s : Type u_2), 𝕜)
hf :
  ∃ᶠ (g : C((↑s : Type u_2), 𝕜)) in 𝓝 f,
    Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g
frequently :
  ∀ (i : ℝ),
    0 < i →
      ∃ (F : X → A),
        Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
          ∀ (y : X),
            Membership.mem (α := A × A) (γ := Set (A × A)) {p : A × A | dist p.1 p.2 ≤ i}
              (((cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) f, F y) : A × A)
⊢ ∀ u ∈ uniformity A,
    ∃ (F : X → A),
      Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
        ∀ (y : X),
          Membership.mem (α := A × A) u
            (((cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) f, F y) : A × A)

Tactic:
rw [Metric.uniformity_basis_dist_le.forall_iff (by aesop)]

Premises used: Metric.uniformity_basis_dist_le, Filter.HasBasis.forall_iff
-- 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
a : X → A
ha_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
f : C((↑s : Type u_2), 𝕜)
hf :
  ∃ᶠ (g : C((↑s : Type u_2), 𝕜)) in 𝓝 f,
    Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g
ε : ℝ
hε : 0 < ε
frequently :
  ∃ (F : X → A),
    Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
      ∀ (y : X),
        ‖HSub.hSub (α := A) ((cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) f : A) (F y)‖ ≤ ε
⊢ ∃ (F : X → A),
    Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
      ∀ (y : X),
        Membership.mem (α := A × A) (γ := Set (A × A)) {p : A × A | dist p.1 p.2 ≤ ε}
          (((cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) f, F y) : A × A)

Tactic:
simp only [Set.mem_setOf_eq, dist_eq_norm]

Premises used: dist_eq_norm, Set.mem_setOf_eq
-- 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
a : X → A
ha_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
f : C((↑s : Type u_2), 𝕜)
hf :
  ∃ᶠ (g : C((↑s : Type u_2), 𝕜)) in 𝓝 f,
    Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g
ε : ℝ
hε : 0 < ε
frequently :
  ∀ (g : C((↑s : Type u_2), 𝕜)) (hg : g ∈ Metric.closedBall f ε)
    (g_cont :
      Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
        (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g),
    ∃ (F : X → A),
      Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
        ∀ (y : X),
          ‖HSub.hSub (α := A) ((cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) f : A) (F y)‖ ≤
            ε
⊢ ∃ (F : X → A),
    Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
      ∀ (y : X),
        ‖HSub.hSub (α := A) ((cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) f : A) (F y)‖ ≤ ε

Tactic:
obtain ⟨g, hg, g_cont⟩ := frequently_iff.mp hf (Metric.closedBall_mem_nhds f hε)

Premises used: Filter.frequently_iff, Metric.closedBall_mem_nhds, Iff.mp
-- 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
a : X → A
ha_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
f : C((↑s : Type u_2), 𝕜)
hf :
  ∃ᶠ (g : C((↑s : Type u_2), 𝕜)) in 𝓝 f,
    Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g
ε : ℝ
hε : 0 < ε
g : C((↑s : Type u_2), 𝕜)
hg : g ∈ Metric.closedBall f ε
g_cont :
  Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g
⊢ ‖f - g‖ ≤ ε

Tactic:
simp only [Metric.mem_closedBall, dist_comm g, dist_eq_norm] at hg

Premises used: dist_eq_norm, dist_comm, Metric.mem_closedBall
-- 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
a : X → A
ha_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
f : C((↑s : Type u_2), 𝕜)
hf :
  ∃ᶠ (g : C((↑s : Type u_2), 𝕜)) in 𝓝 f,
    Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g
ε : ℝ
hε : 0 < ε
g : C((↑s : Type u_2), 𝕜)
g_cont :
  Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g
hg : ‖f - g‖ ≤ ε
⊢ ∃ (F : X → A),
    Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
      ∀ (y : X),
        ‖HSub.hSub (α := A) ((cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) f : A) (F y)‖ ≤ ε

Tactic:
⟨_, g_cont, fun x ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- 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
a : X → A
ha_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
f : C((↑s : Type u_2), 𝕜)
hf :
  ∃ᶠ (g : C((↑s : Type u_2), 𝕜)) in 𝓝 f,
    Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g
ε : ℝ
hε : 0 < ε
g : C((↑s : Type u_2), 𝕜)
g_cont :
  Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g
hg : ‖f - g‖ ≤ ε
frequently :
  ∀ (x : X),
    ‖HSub.hSub (α := A) (β := A) ((cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) f : A)
          ((cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g : A)‖ ≤
      ε
⊢ ∃ (F : X → A),
    Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
      ∀ (y : X),
        ‖HSub.hSub (α := A) ((cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) f : A) (F y)‖ ≤ ε

Tactic:
refine ⟨_, g_cont, fun 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 : 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
a : X → A
ha_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
f : C((↑s : Type u_2), 𝕜)
hf :
  ∃ᶠ (g : C((↑s : Type u_2), 𝕜)) in 𝓝 f,
    Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g
ε : ℝ
hε : 0 < ε
g : C((↑s : Type u_2), 𝕜)
g_cont :
  Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g
hg : ‖f - g‖ ≤ ε
x : X
frequently :
  norm.{u_3} (E := A)
      ((cfcHom (p := p) ⋯ : (a : C((↑(spectrum 𝕜 (a x)) : Type u_2), 𝕜)) → A)
          ((f - g).comp
            { toFun := Subtype.map (p := Membership.mem (spectrum 𝕜 (a x))) (q := Membership.mem s) id ⋯,
              continuous_toFun := ⋯ : C((↑(spectrum 𝕜 (a x)) : Type u_2), (↑s : Type u_2)) }) :
        A) ≤
    ε
⊢ ‖HSub.hSub (α := A) (β := A) ((cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) f : A)
        ((cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g : A)‖ ≤
    ε

Tactic:
rw [← map_sub, cfcHomSuperset_apply]

Premises used: map_sub, cfcHomSuperset_apply
-- 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
a : X → A
ha_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
f : C((↑s : Type u_2), 𝕜)
hf :
  ∃ᶠ (g : C((↑s : Type u_2), 𝕜)) in 𝓝 f,
    Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g
ε : ℝ
hε : 0 < ε
g : C((↑s : Type u_2), 𝕜)
g_cont :
  Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g
hg : ‖f - g‖ ≤ ε
x : X
frequently :
  ‖(f - g).comp
        { toFun := Subtype.map (p := Membership.mem (spectrum 𝕜 (a x))) (q := Membership.mem s) id ⋯,
          continuous_toFun := ⋯ : C((↑(spectrum 𝕜 (a x)) : Type u_2), (↑s : Type u_2)) }‖ ≤
    ε
⊢ norm.{u_3} (E := A)
      ((cfcHom (p := p) ⋯ : (a : C((↑(spectrum 𝕜 (a x)) : Type u_2), 𝕜)) → A)
          ((f - g).comp
            { toFun := Subtype.map (p := Membership.mem (spectrum 𝕜 (a x))) (q := Membership.mem s) id ⋯,
              continuous_toFun := ⋯ : C((↑(spectrum 𝕜 (a x)) : Type u_2), (↑s : Type u_2)) }) :
        A) ≤
    ε

Tactic:
rw [isometry_cfcHom (R := 𝕜) _ (ha' x) |>.norm_map_of_map_zero (map_zero (cfcHom (ha' x)))]

Premises used: cfcHom, map_zero, Isometry.norm_map_of_map_zero
-- 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
a : X → A
ha_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
f : C((↑s : Type u_2), 𝕜)
hf :
  ∃ᶠ (g : C((↑s : Type u_2), 𝕜)) in 𝓝 f,
    Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g
ε : ℝ
hε : 0 < ε
g : C((↑s : Type u_2), 𝕜)
g_cont :
  Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g
hg : ‖f - g‖ ≤ ε
x : X
frequently :
  ∀ (hg : ∀ (x : (↑s : Type u_2)), norm (E := 𝕜) ((f - g : (a : (↑s : Type u_2)) → 𝕜) x : 𝕜) ≤ ε) (x : X)
    (x_1 : (↑(spectrum 𝕜 (a x)) : Type u_2)),
    norm (E := 𝕜)
        (((f - g).comp
                { toFun := Subtype.map (p := Membership.mem (spectrum 𝕜 (a x))) (q := Membership.mem s) id ⋯,
                  continuous_toFun := ⋯ : C((↑(spectrum 𝕜 (a x)) : Type u_2), (↑s : Type u_2)) } :
              (a : (↑(spectrum 𝕜 (a x)) : Type u_2)) → 𝕜)
            x_1 :
          𝕜) ≤
      ε
⊢ ‖(f - g).comp
        { toFun := Subtype.map (p := Membership.mem (spectrum 𝕜 (a x))) (q := Membership.mem s) id ⋯,
          continuous_toFun := ⋯ : C((↑(spectrum 𝕜 (a x)) : Type u_2), (↑s : Type u_2)) }‖ ≤
    ε

Tactic:
rw [ContinuousMap.norm_le _ hε.le] at hg ⊢

Premises used: ContinuousMap.norm_le, LT.lt.le
-- 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
a : X → A
ha_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
f : C((↑s : Type u_2), 𝕜)
hf :
  ∃ᶠ (g : C((↑s : Type u_2), 𝕜)) in 𝓝 f,
    Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g
ε : ℝ
hε : 0 < ε
g : C((↑s : Type u_2), 𝕜)
g_cont :
  Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g
hg : ∀ (x : (↑s : Type u_2)), norm (E := 𝕜) ((f - g : (a : (↑s : Type u_2)) → 𝕜) x : 𝕜) ≤ ε
x : X
⊢ ∀ (x_1 : (↑(spectrum 𝕜 (a x)) : Type u_2)),
    norm (E := 𝕜)
        (((f - g).comp
                { toFun := Subtype.map (p := Membership.mem (spectrum 𝕜 (a x))) (q := Membership.mem s) id ⋯,
                  continuous_toFun := ⋯ : C((↑(spectrum 𝕜 (a x)) : Type u_2), (↑s : Type u_2)) } :
              (a : (↑(spectrum 𝕜 (a x)) : Type u_2)) → 𝕜)
            x_1 :
          𝕜) ≤
      ε

Tactic:
aesop