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 : Set 𝕜
hs : IsCompact s
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (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_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      ((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A) g
frequently :
  ∀ (i : ℝ),
    0 < i →
      ∃ (F : X → A),
        Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
          ∀ (y : X),
            Membership.mem (α := A × A) (γ := Set (A × A)) {p : A × A | dist p.1 p.2 ≤ i}
              ((((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) :
                      (a : C((↑s : Type u_2), 𝕜)₀) → A)
                    f,
                  F y) :
                A × A)
⊢ ∀ u ∈ uniformity A,
    ∃ (F : X → A),
      Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
        ∀ (y : X),
          Membership.mem (α := A × A) u
            ((((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) :
                    (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 : 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
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (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_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      ((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A) g
ε : ℝ
hε : 0 < ε
frequently :
  ∃ (F : X → A),
    Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
      ∀ (y : X),
        ‖HSub.hSub (α := A)
              (((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) :
                    (a : C((↑s : Type u_2), 𝕜)₀) → A)
                  f :
                A)
              (F y)‖ ≤
          ε
⊢ ∃ (F : X → A),
    Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
      ∀ (y : X),
        Membership.mem (α := A × A) (γ := Set (A × A)) {p : A × A | dist p.1 p.2 ≤ ε}
          ((((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) :
                  (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 : 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
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (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_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      ((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (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_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
        ((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A)
          g),
    ∃ (F : X → A),
      Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
        ∀ (y : X),
          ‖HSub.hSub (α := A)
                (((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) :
                      (a : C((↑s : Type u_2), 𝕜)₀) → A)
                    f :
                  A)
                (F y)‖ ≤
            ε
⊢ ∃ (F : X → A),
    Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
      ∀ (y : X),
        ‖HSub.hSub (α := A)
              (((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) :
                    (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 : 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
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (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_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      ((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (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_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    ((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (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 : 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
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (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_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      ((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A) g
ε : ℝ
hε : 0 < ε
g : C((↑s : Type u_2), 𝕜)₀
g_cont :
  Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    ((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A) g
hg : ‖f - g‖ ≤ ε
⊢ ∃ (F : X → A),
    Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
      ∀ (y : X),
        ‖HSub.hSub (α := A)
              (((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) :
                    (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 : 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
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (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_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      ((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A) g
ε : ℝ
hε : 0 < ε
g : C((↑s : Type u_2), 𝕜)₀
g_cont :
  Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    ((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A) g
hg : ‖f - g‖ ≤ ε
frequently :
  ∀ (x : X),
    ‖HSub.hSub (α := A) (β := A)
          (((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) :
                (a : C((↑s : Type u_2), 𝕜)₀) → A)
              f :
            A)
          (((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) :
                (a : C((↑s : Type u_2), 𝕜)₀) → A)
              g :
            A)‖ ≤
      ε
⊢ ∃ (F : X → A),
    Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
      ∀ (y : X),
        ‖HSub.hSub (α := A)
              (((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) :
                    (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 : 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
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (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_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      ((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A) g
ε : ℝ
hε : 0 < ε
g : C((↑s : Type u_2), 𝕜)₀
g_cont :
  Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    ((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A) g
hg : ‖f - g‖ ≤ ε
x : X
frequently :
  norm.{u_3} (E := A)
      ((cfcₙHom (p := p) ⋯ : (a : C((↑(quasispectrum 𝕜 (a x)) : Type u_2), 𝕜)₀) → A)
          ((f - g).comp
            { toFun := Subtype.map (p := Membership.mem (quasispectrum 𝕜 (a x))) (q := Membership.mem s) id ⋯,
              continuous_toFun := ⋯, map_zero' := ⋯ : C((↑(quasispectrum 𝕜 (a x)) : Type u_2), (↑s : Type u_2))₀ }) :
        A) ≤
    ε
⊢ ‖HSub.hSub (α := A) (β := A)
        (((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A)
            f :
          A)
        (((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A)
            g :
          A)‖ ≤
    ε

Tactic:
rw [← map_sub, cfcₙHomSuperset_apply]

Premises used: map_sub, cfcₙHomSuperset_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 : 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
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (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_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      ((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A) g
ε : ℝ
hε : 0 < ε
g : C((↑s : Type u_2), 𝕜)₀
g_cont :
  Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    ((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A) g
hg : ‖f - g‖ ≤ ε
x : X
frequently :
  norm (E := C((↑(quasispectrum 𝕜 (a x)) : Type u_2), 𝕜)₀)
      ((f - g).comp
        { toFun := Subtype.map (p := Membership.mem (quasispectrum 𝕜 (a x))) (q := Membership.mem s) id ⋯,
          continuous_toFun := ⋯, map_zero' := ⋯ : C((↑(quasispectrum 𝕜 (a x)) : Type u_2), (↑s : Type u_2))₀ }) ≤
    ε
⊢ norm.{u_3} (E := A)
      ((cfcₙHom (p := p) ⋯ : (a : C((↑(quasispectrum 𝕜 (a x)) : Type u_2), 𝕜)₀) → A)
          ((f - g).comp
            { toFun := Subtype.map (p := Membership.mem (quasispectrum 𝕜 (a x))) (q := Membership.mem s) id ⋯,
              continuous_toFun := ⋯, map_zero' := ⋯ : C((↑(quasispectrum 𝕜 (a x)) : Type u_2), (↑s : Type u_2))₀ }) :
        A) ≤
    ε

Tactic:
rw [isometry_cfcₙHom (R := 𝕜) _ (ha' x) |>.norm_map_of_map_zero (map_zero (cfcₙHom (ha' x)))]

Premises used: isometry_cfcₙHom, map_zero, Isometry.norm_map_of_map_zero, cfcₙHom
-- 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
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (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_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      ((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A) g
ε : ℝ
hε : 0 < ε
g : C((↑s : Type u_2), 𝕜)₀
g_cont :
  Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    ((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A) g
hg : ‖f - g‖ ≤ ε
x : X
frequently :
  ∀
    (hg :
      ∀ (x : (↑s : Type u_2)),
        norm (E := 𝕜) (((↑(f - g) : C((↑s : Type u_2), 𝕜)) : (a : (↑s : Type u_2)) → 𝕜) x : 𝕜) ≤ ε)
    (x : X) (x_1 : (↑(quasispectrum 𝕜 (a x)) : Type u_2)),
    norm (E := 𝕜)
        (((↑((f - g).comp
                    { toFun := Subtype.map (p := Membership.mem (quasispectrum 𝕜 (a x))) (q := Membership.mem s) id ⋯,
                      continuous_toFun := ⋯, map_zero' := ⋯ :
                      C((↑(quasispectrum 𝕜 (a x)) : Type u_2), (↑s : Type u_2))₀ }) :
                C((↑(quasispectrum 𝕜 (a x)) : Type u_2), 𝕜)) :
              (a : (↑(quasispectrum 𝕜 (a x)) : Type u_2)) → 𝕜)
            x_1 :
          𝕜) ≤
      ε
⊢ norm (E := C((↑(quasispectrum 𝕜 (a x)) : Type u_2), 𝕜)₀)
      ((f - g).comp
        { toFun := Subtype.map (p := Membership.mem (quasispectrum 𝕜 (a x))) (q := Membership.mem s) id ⋯,
          continuous_toFun := ⋯, map_zero' := ⋯ : C((↑(quasispectrum 𝕜 (a x)) : Type u_2), (↑s : Type u_2))₀ }) ≤
    ε

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

Premises used: ContinuousMap.norm_le, LT.lt.le, ContinuousMapZero.norm_def
-- 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
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (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_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      ((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A) g
ε : ℝ
hε : 0 < ε
g : C((↑s : Type u_2), 𝕜)₀
g_cont :
  Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    ((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A) g
hg : ∀ (x : (↑s : Type u_2)), norm (E := 𝕜) (((↑(f - g) : C((↑s : Type u_2), 𝕜)) : (a : (↑s : Type u_2)) → 𝕜) x : 𝕜) ≤ ε
x : X
⊢ ∀ (x_1 : (↑(quasispectrum 𝕜 (a x)) : Type u_2)),
    norm (E := 𝕜)
        (((↑((f - g).comp
                    { toFun := Subtype.map (p := Membership.mem (quasispectrum 𝕜 (a x))) (q := Membership.mem s) id ⋯,
                      continuous_toFun := ⋯, map_zero' := ⋯ :
                      C((↑(quasispectrum 𝕜 (a x)) : Type u_2), (↑s : Type u_2))₀ }) :
                C((↑(quasispectrum 𝕜 (a x)) : Type u_2), 𝕜)) :
              (a : (↑(quasispectrum 𝕜 (a x)) : Type u_2)) → 𝕜)
            x_1 :
          𝕜) ≤
      ε

Tactic:
aesop
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
𝕜 : 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
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
hf0 : f 0 = 0
pos : ∀ (hs0 : 0 ∈ s), ContinuousOn (Y := A) (fun (x : A) ↦ cfcₙ (p := p) f x) {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s}
neg : ∀ (hs0 : 0 ∉ s), ContinuousOn (Y := A) (fun (x : A) ↦ cfcₙ (p := p) f x) {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s}
⊢ ContinuousOn (Y := A) (fun (x : A) ↦ cfcₙ (p := p) f x) {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s}

Tactic:
by_cases hs0 : 0 ∈ s
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
𝕜 : 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
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
hf0 : f 0 = 0
hs0 : 0 ∈ s
pos :
  Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (Set.restrict (π := fun (a : A) ↦ A) {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s} fun (x : A) ↦ cfcₙ (p := p) f x)
⊢ ContinuousOn (Y := A) (fun (x : A) ↦ cfcₙ (p := p) f x) {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s}

Tactic:
rw [continuousOn_iff_continuous_restrict]

Premises used: continuousOn_iff_continuous_restrict
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
𝕜 : 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
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
hf0 : f 0 = 0
hs0 : 0 ∈ s
⊢ Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (x : (↑{a : A | p a ∧ quasispectrum 𝕜 a ⊆ s} : Type u_3)) ↦
    ((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : ContinuousMapZero (↑s : Type u_2) 𝕜 →⋆ₙₐ[𝕜] A) :
        (a : ContinuousMapZero (↑s : Type u_2) 𝕜) → A)
      { toFun := s.restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯, map_zero' := hf0 }

Tactic:
continuous_cfcₙHomSuperset_left hs (hs0 := ⟨hs0⟩) ⟨⟨_, hf.restrict⟩, hf0⟩ (X :=
        {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s}) continuous_subtype_val (fun x ↦ x.2.2)

Premises used: continuous_cfcₙHomSuperset_left, continuous_subtype_val, ContinuousMap.mk, And.right, ContinuousOn.restrict, ContinuousMapZero.mk, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
𝕜 : 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
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
hf0 : f 0 = 0
hs0 : 0 ∈ s
h :
  ∀ (x : (↑{a : A | p a ∧ quasispectrum 𝕜 a ⊆ s} : Type u_3)),
    Eq (α := A)
      (Set.restrict (π := fun (a : A) ↦ A) {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s} (fun (x : A) ↦ cfcₙ (p := p) f x) x :
        A)
      (((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : ContinuousMapZero (↑s : Type u_2) 𝕜 →⋆ₙₐ[𝕜] A) :
            (a : ContinuousMapZero (↑s : Type u_2) 𝕜) → A)
          { toFun := s.restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯, map_zero' := hf0 } :
        A)
⊢ Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (Set.restrict (π := fun (a : A) ↦ A) {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s} fun (x : A) ↦ cfcₙ (p := p) f x)

Tactic:
convert!
      continuous_cfcₙHomSuperset_left hs (hs0 := ⟨hs0⟩) ⟨⟨_, hf.restrict⟩, hf0⟩ (X :=
        {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s}) continuous_subtype_val (fun x ↦ x.2.2) with
      x