awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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
⊢ ∀ 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)
have 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) sorry (s := s) sorry : 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)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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 < ε
⊢ ∃ (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)
have frequently : ∃ (F : X → A),
  Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
    ∀ (y : X),
      ‖HSub.hSub (α := A)
            (((cfcₙHomSuperset (p := p) sorry (s := s) sorry : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) :
                  (a : C((↑s : Type u_2), 𝕜)₀) → A)
                f :
              A)
            (F y)‖ ≤
        ε
Tactic: simp only [Set.mem_setOf_eq, dist_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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 < ε
⊢ ∃ (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)‖ ≤
          ε
have 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) sorry (s := s) sorry : 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) sorry (s := s) sorry : 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ε)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (hypothesis)
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 : 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)‖ ≤
          ε
have hg₁ : ‖f - g‖ ≤ ε
Tactic: simp only [Metric.mem_closedBall, dist_comm g, dist_eq_norm] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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)‖ ≤
          ε
have frequently : ∀ (x : X),
  ‖HSub.hSub (α := A) (β := A)
        (((cfcₙHomSuperset (p := p) sorry (s := s) sorry : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A)
            f :
          A)
        (((cfcₙHomSuperset (p := p) sorry (s := s) sorry : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A)
            g :
          A)‖ ≤
    ε
Tactic: refine ⟨_, g_cont, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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
⊢ ‖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)‖ ≤
    ε
have frequently : norm.{u_3} (E := A)
    ((cfcₙHom (p := p) sorry : (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 sorry,
            continuous_toFun := sorry, map_zero' := sorry : C((↑(quasispectrum 𝕜 (a x)) : Type u_2), (↑s : Type u_2))₀ }) :
      A) ≤
  ε
Tactic: rw [← map_sub, cfcₙHomSuperset_apply]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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
⊢ 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) ≤
    ε
have 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 sorry,
        continuous_toFun := sorry, map_zero' := sorry : C((↑(quasispectrum 𝕜 (a x)) : Type u_2), (↑s : Type u_2))₀ }) ≤
  ε
Tactic: rw [isometry_cfcₙHom (R := 𝕜) _ (ha' x) |>.norm_map_of_map_zero (map_zero (cfcₙHom (ha' x)))]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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
⊢ 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))₀ }) ≤
    ε
have 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 sorry,
                    continuous_toFun := sorry, map_zero' := sorry :
                    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: rw [ContinuousMapZero.norm_def, ContinuousMap.norm_le _ hε.le] at hg ⊢
Cleared hypotheses: hg, x
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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)
f : C((↑s : Type u_2), 𝕜)₀
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)
⊢ 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) f
have zero : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
  ((cfcₙHomSuperset (p := p) sorry (s := s) sorry : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A) 0
Tactic: induction f using ContinuousMapZero.induction_on_of_compact with
  | zero => simpa [map_zero] using continuous_const
  | id => simpa only [cfcₙHomSuperset_id]
  | star_id => simp only [map_star, cfcₙHomSuperset_id]; fun_prop
  | add f g hf hg => simpa only [map_add] using hf.add hg
  | mul f g hf hg => simpa only [map_mul] using hf.mul hg
  | smul r f hf => simpa only [map_smul] using hf.const_smul r
  | frequently f hf =>
    apply continuous_of_uniform_approx_of_continuous
    rw [Metric.uniformity_basis_dist_le.forall_iff (by aesop)]
    intro ε hε
    simp only [Set.mem_setOf_eq, dist_eq_norm]
    obtain ⟨g, hg, g_cont⟩ := frequently_iff.mp hf (Metric.closedBall_mem_nhds f hε)
    simp only [Metric.mem_closedBall, dist_comm g, dist_eq_norm] at hg
    refine ⟨_, g_cont, fun x ↦ ?_⟩
    rw [← map_sub, cfcₙHomSuperset_apply]
    rw [isometry_cfcₙHom (R := 𝕜) _ (ha' x) |>.norm_map_of_map_zero (map_zero (cfcₙHom (ha' x)))]
    rw [ContinuousMapZero.norm_def, ContinuousMap.norm_le _ hε.le] at hg ⊢
    aesop
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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)
f : C((↑s : Type u_2), 𝕜)₀
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)
zero :
  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) 0
⊢ 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) f
have id : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
  ((cfcₙHomSuperset (p := p) sorry (s := s) sorry : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A)
    (ContinuousMapZero.id s)
Tactic: induction f using ContinuousMapZero.induction_on_of_compact with
  | zero => simpa [map_zero] using continuous_const
  | id => simpa only [cfcₙHomSuperset_id]
  | star_id => simp only [map_star, cfcₙHomSuperset_id]; fun_prop
  | add f g hf hg => simpa only [map_add] using hf.add hg
  | mul f g hf hg => simpa only [map_mul] using hf.mul hg
  | smul r f hf => simpa only [map_smul] using hf.const_smul r
  | frequently f hf =>
    apply continuous_of_uniform_approx_of_continuous
    rw [Metric.uniformity_basis_dist_le.forall_iff (by aesop)]
    intro ε hε
    simp only [Set.mem_setOf_eq, dist_eq_norm]
    obtain ⟨g, hg, g_cont⟩ := frequently_iff.mp hf (Metric.closedBall_mem_nhds f hε)
    simp only [Metric.mem_closedBall, dist_comm g, dist_eq_norm] at hg
    refine ⟨_, g_cont, fun x ↦ ?_⟩
    rw [← map_sub, cfcₙHomSuperset_apply]
    rw [isometry_cfcₙHom (R := 𝕜) _ (ha' x) |>.norm_map_of_map_zero (map_zero (cfcₙHom (ha' x)))]
    rw [ContinuousMapZero.norm_def, ContinuousMap.norm_le _ hε.le] at hg ⊢
    aesop
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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)
f : C((↑s : Type u_2), 𝕜)₀
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)
zero :
  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) 0
id :
  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)
      (ContinuousMapZero.id s)
⊢ 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) f
have star_id : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
  ((cfcₙHomSuperset (p := p) sorry (s := s) sorry : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A)
    (star (ContinuousMapZero.id s))
Tactic: induction f using ContinuousMapZero.induction_on_of_compact with
  | zero => simpa [map_zero] using continuous_const
  | id => simpa only [cfcₙHomSuperset_id]
  | star_id => simp only [map_star, cfcₙHomSuperset_id]; fun_prop
  | add f g hf hg => simpa only [map_add] using hf.add hg
  | mul f g hf hg => simpa only [map_mul] using hf.mul hg
  | smul r f hf => simpa only [map_smul] using hf.const_smul r
  | frequently f hf =>
    apply continuous_of_uniform_approx_of_continuous
    rw [Metric.uniformity_basis_dist_le.forall_iff (by aesop)]
    intro ε hε
    simp only [Set.mem_setOf_eq, dist_eq_norm]
    obtain ⟨g, hg, g_cont⟩ := frequently_iff.mp hf (Metric.closedBall_mem_nhds f hε)
    simp only [Metric.mem_closedBall, dist_comm g, dist_eq_norm] at hg
    refine ⟨_, g_cont, fun x ↦ ?_⟩
    rw [← map_sub, cfcₙHomSuperset_apply]
    rw [isometry_cfcₙHom (R := 𝕜) _ (ha' x) |>.norm_map_of_map_zero (map_zero (cfcₙHom (ha' x)))]
    rw [ContinuousMapZero.norm_def, ContinuousMap.norm_le _ hε.le] at hg ⊢
    aesop
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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
⊢ ContinuousOn (Y := A) (fun (x : A) ↦ cfcₙ (p := p) f x) {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s}
have pos : ∀ (hs0 : 0 ∈ 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