awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (hypothesis)
Goal:
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : MetricSpace A
inst_8 : Algebra R A
inst_9 : IsometricContinuousFunctionalCalculus R A p
a : A
s : Set R
hs : spectrum R a ⊆ s
h₁ :
  LipschitzOnWith.{u_2, u_3} (β := A) 1
    (fun (f : R →ᵤ[{spectrum R a}] R) ↦
      cfc.{u_2, u_3} (R := R) (p := p) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f) a)
    {f : R →ᵤ[{spectrum R a}] R |
      ContinuousOn (Y := R) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f) (spectrum R a)}
⊢ LipschitzOnWith.{u_2, u_3} (β := A) 1
    (fun (f : R →ᵤ[{s}] R) ↦ cfc.{u_2, u_3} (R := R) (p := p) ((toFun {s} : (a : R →ᵤ[{s}] R) → R → R) f) a)
    {f : R →ᵤ[{s}] R | ContinuousOn (Y := R) ((toFun {s} : (a : R →ᵤ[{s}] R) → R → R) f) s}
have h₂ : LipschitzWith (α := R →ᵤ[{s}] R) (β := R →ᵤ[{spectrum R a}] R) 1
  (Function.comp (β := R → R) (⇑(ofFun {spectrum R a}) : (a_1 : R → R) → R →ᵤ[{spectrum R a}] R)
    (⇑(toFun {s}) : (a : R →ᵤ[{s}] R) → R → R))
Tactic: have h₂ := lipschitzWith_one_ofFun_toFun' (𝔖 := {spectrum R a}) (𝔗 := {s}) (β := R) (by simpa)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (hypothesis)
Goal:
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : MetricSpace A
inst_8 : Algebra R A
inst_9 : IsometricContinuousFunctionalCalculus R A p
a : A
s : Set R
hs : spectrum R a ⊆ s
h₁ :
  LipschitzOnWith.{u_2, u_3} (β := A) 1
    (fun (f : R →ᵤ[{spectrum R a}] R) ↦
      cfc.{u_2, u_3} (R := R) (p := p) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f) a)
    {f : R →ᵤ[{spectrum R a}] R |
      ContinuousOn (Y := R) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f) (spectrum R a)}
h₂ :
  LipschitzWith (α := R →ᵤ[{s}] R) (β := R →ᵤ[{spectrum R a}] R) 1
    (Function.comp (β := R → R) (⇑(ofFun {spectrum R a}) : (a_1 : R → R) → R →ᵤ[{spectrum R a}] R)
      (⇑(toFun {s}) : (a : R →ᵤ[{s}] R) → R → R))
⊢ LipschitzOnWith.{u_2, u_3} (β := A) 1
    (fun (f : R →ᵤ[{s}] R) ↦ cfc.{u_2, u_3} (R := R) (p := p) ((toFun {s} : (a : R →ᵤ[{s}] R) → R → R) f) a)
    {f : R →ᵤ[{s}] R | ContinuousOn (Y := R) ((toFun {s} : (a : R →ᵤ[{s}] R) → R → R) f) s}
have h₃ : LipschitzOnWith (α := R →ᵤ[{s}] R) (β := R →ᵤ[{spectrum R a}] R) 1
  (Function.comp (β := R → R) (⇑(ofFun {spectrum R a}) : (a_1 : R → R) → R →ᵤ[{spectrum R a}] R)
    (⇑(toFun {s}) : (a : R →ᵤ[{s}] R) → R → R))
  {f : R →ᵤ[{s}] R | ContinuousOn (Y := R) ((toFun {s} : (a : R →ᵤ[{s}] R) → R → R) f) s}
Tactic: have h₃ := h₂.lipschitzOnWith (s := {f | ContinuousOn (toFun {s} f) (s)})
-- 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 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
f : C((↑s : Type u_2), 𝕜)
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)
⊢ CompactSpace.{u_2} (↑s : Type u_2)
have rwa : ∀ (hs : CompactSpace.{u_2} (↑s : Type u_2)) (f : C((↑s : Type u_2), 𝕜)) (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)), CompactSpace.{u_2} (↑s : Type u_2)
Tactic: rwa [isCompact_iff_compactSpace] at hs
Cleared hypotheses: hs, f, a, ha_cont, ha, ha'
-- 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 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
f : C((↑s : Type u_2), 𝕜)
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)
⊢ Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) f
have this : CompactSpace.{u_2} (↑s : Type u_2)
Tactic: have : CompactSpace s := by rwa [isCompact_iff_compactSpace] at hs
-- 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 : 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)
r : 𝕜
⊢ Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) (ContinuousMap.const (↑s : Type u_2) r)
have this₁ : Eq (α := C((↑s : Type u_2), 𝕜)) (ContinuousMap.const (↑s : Type u_2) r)
  ((algebraMap 𝕜 C((↑s : Type u_2), 𝕜) : (a : 𝕜) → C((↑s : Type u_2), 𝕜)) r)
Tactic: have : ContinuousMap.const s r = algebraMap 𝕜 C(s, 𝕜) r := rfl
-- 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 : 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) ↦
    (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A)
      (star (ContinuousMap.restrict s (ContinuousMap.id 𝕜)))
have star_id : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦ star (a x)
Tactic: simp only [map_star, cfcHomSuperset_id]
-- 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 : 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
⊢ Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) f
have frequently : ∀ u ∈ uniformity A,
  ∃ (F : X → A),
    Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
      ∀ (y : X),
        Membership.mem (α := A × A) u
          (((cfcHomSuperset (p := p) sorry (s := s) sorry : (a : C((↑s : Type u_2), 𝕜)) → A) f, F y) : A × A)
Tactic: apply continuous_of_uniform_approx_of_continuous
-- 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 : 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
⊢ ∀ 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)
have 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) sorry (s := s) sorry : (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 : 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 < ε
⊢ ∃ (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)
have frequently : ∃ (F : X → A),
  Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
    ∀ (y : X),
      ‖HSub.hSub (α := A) ((cfcHomSuperset (p := p) sorry (s := s) sorry : (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 : 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 < ε
⊢ ∃ (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)‖ ≤ ε
have 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) sorry (s := s) sorry : (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) sorry (s := s) sorry : (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 : 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 : 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)‖ ≤ ε
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 : 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)‖ ≤ ε
have frequently : ∀ (x : X),
  ‖HSub.hSub (α := A) (β := A) ((cfcHomSuperset (p := p) sorry (s := s) sorry : (a : C((↑s : Type u_2), 𝕜)) → A) f : A)
        ((cfcHomSuperset (p := p) sorry (s := s) sorry : (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 : 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
⊢ ‖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)‖ ≤
    ε
have frequently : norm.{u_3} (E := A)
    ((cfcHom (p := p) sorry : (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 sorry,
            continuous_toFun := sorry : C((↑(spectrum 𝕜 (a x)) : Type u_2), (↑s : Type u_2)) }) :
      A) ≤
  ε
Tactic: rw [← map_sub, cfcHomSuperset_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 : 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
⊢ 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) ≤
    ε
have frequently : ‖(f - g).comp
      { toFun := Subtype.map (p := Membership.mem (spectrum 𝕜 (a x))) (q := Membership.mem s) id sorry,
        continuous_toFun := sorry : C((↑(spectrum 𝕜 (a x)) : Type u_2), (↑s : Type u_2)) }‖ ≤
  ε
Tactic: rw [isometry_cfcHom (R := 𝕜) _ (ha' x) |>.norm_map_of_map_zero (map_zero (cfcHom (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 : 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
⊢ ‖(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)) }‖ ≤
    ε
have 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 sorry,
                continuous_toFun := sorry : C((↑(spectrum 𝕜 (a x)) : Type u_2), (↑s : Type u_2)) } :
            (a : (↑(spectrum 𝕜 (a x)) : Type u_2)) → 𝕜)
          x_1 :
        𝕜) ≤
    ε
Tactic: rw [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 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
f : C((↑s : Type u_2), 𝕜)
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) ↦
    (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) f
have const : ∀ (r : 𝕜),
  Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    (cfcHomSuperset (p := p) sorry (s := s) sorry : (a : C((↑s : Type u_2), 𝕜)) → A) (ContinuousMap.const (↑s : Type u_2) r)
Tactic: induction f using ContinuousMap.induction_on_of_compact with
  | const r =>
    have : ContinuousMap.const s r = algebraMap 𝕜 C(s, 𝕜) r := rfl
    simpa only [this, AlgHomClass.commutes] using continuous_const
  | id =>
    simp only [cfcHomSuperset_id]
    fun_prop
  | star_id =>
    simp only [map_star, cfcHomSuperset_id]
    fun_prop
  | add f g hf hg => simpa using hf.add hg
  | mul f g hf hg => simpa using hf.mul hg
  | 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, cfcHomSuperset_apply]
    rw [isometry_cfcHom (R := 𝕜) _ (ha' x) |>.norm_map_of_map_zero (map_zero (cfcHom (ha' x)))]
    rw [ContinuousMap.norm_le _ hε.le] at hg ⊢
    aesop
Cleared hypotheses: f