awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (hypothesis)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
inst_13 : TopologicalSpace X
f : X → R → R
a : A
s : Set X
h_cont :
  ∀ x ∈ s,
    ContinuousWithinAt.{u_1, u_2} (Y := R →ᵤ[{quasispectrum R a}] R)
      (fun (x : X) ↦ (ofFun {quasispectrum R a} : (a_2 : R → R) → R →ᵤ[{quasispectrum R a}] R) (f x)) s x
hf : ∀ x ∈ s, ContinuousOn (f x) (quasispectrum R a)
hf0 : ∀ x ∈ s, f x 0 = 0
⊢ ∀ x ∈ s, ContinuousWithinAt.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) (f x) a) s x
have h_cont₁ : ∀ x ∈ s, TendstoUniformlyOn (fun (x : X) ↦ f x) (f x) (𝓝[s] x) (quasispectrum R a)
Tactic: simp only [ContinuousWithinAt, UniformOnFun.tendsto_iff_tendstoUniformlyOn, Set.mem_singleton_iff,
    Function.comp_def, toFun_ofFun, forall_eq] at h_cont
Cleared hypotheses: h_cont
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
inst_13 : TopologicalSpace X
f : X → R → R
a : A
s : Set X
hf : ∀ x ∈ s, ContinuousOn (f x) (quasispectrum R a)
hf0 : ∀ x ∈ s, f x 0 = 0
h_cont : ∀ x ∈ s, TendstoUniformlyOn (fun (x : X) ↦ f x) (f x) (𝓝[s] x) (quasispectrum R a)
⊢ ∀ x ∈ s, ContinuousWithinAt.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) (f x) a) s x
have refine_1 : ∀ (x : X) (hx : x ∈ s), ∀ᶠ (x : X) in 𝓝[s] x, ContinuousOn (f x) (quasispectrum R a)
Tactic: refine fun x hx ↦ continuousWithinAt_cfcₙ_fun (h_cont x hx) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
inst_13 : TopologicalSpace X
f : X → R → R
a : A
s : Set X
hf : ∀ x ∈ s, ContinuousOn (f x) (quasispectrum R a)
hf0 : ∀ x ∈ s, f x 0 = 0
h_cont : ∀ x ∈ s, TendstoUniformlyOn (fun (x : X) ↦ f x) (f x) (𝓝[s] x) (quasispectrum R a)
refine_1 : ∀ (x : X) (hx : x ∈ s), ∀ᶠ (x : X) in 𝓝[s] x, ContinuousOn (f x) (quasispectrum R a)
⊢ ∀ x ∈ s, ContinuousWithinAt.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) (f x) a) s x
have refine_2 : ∀ (x : X) (hx : x ∈ s), ∀ᶠ (x : X) in 𝓝[s] x, f x 0 = 0
Tactic: refine fun x hx ↦ continuousWithinAt_cfcₙ_fun (h_cont x hx) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
inst_13 : TopologicalSpace X
f : X → R → R
a : A
h_cont :
  Continuous[inst_13, topologicalSpace R R {quasispectrum R a}] fun (x : X) ↦
    (ofFun {quasispectrum R a} : (a_1 : R → R) → R →ᵤ[{quasispectrum R a}] R) (f x)
hf : ∀ (x : X), ContinuousOn (f x) (quasispectrum R a)
hf0 : ∀ (x : X), f x 0 = 0
⊢ Continuous[inst_13, inst_8] fun (x : X) ↦ cfcₙ (p := p) (f x) a
have rw : ∀
  (h_cont :
    ContinuousOn.{u_1, u_2} (Y := R →ᵤ[{quasispectrum R a}] R)
      (fun (x : X) ↦ (ofFun {quasispectrum R a} : (a_1 : R → R) → R →ᵤ[{quasispectrum R a}] R) (f x)) Set.univ)
  (hf : ∀ (x : X), ContinuousOn (f x) (quasispectrum R a)) (hf0 : ∀ (x : X), f x 0 = 0),
  ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) (f x) a) Set.univ
Tactic: rw [← continuousOn_univ] at h_cont ⊢
Cleared hypotheses: h_cont, hf, hf0
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : MetricSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalIsometricContinuousFunctionalCalculus R A p
a : A
⊢ LipschitzOnWith.{u_2, u_3} (β := A) 1
    (fun (f : R →ᵤ[{quasispectrum R a}] R) ↦
      cfcₙ.{u_2, u_3} (R := R) (p := p) ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) f) a)
    {f : R →ᵤ[{quasispectrum R a}] R |
      ContinuousOn (Y := R) ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) f)
          (quasispectrum R a) ∧
        f 0 = 0}
have pos : ∀ (ha : p a),
  LipschitzOnWith.{u_2, u_3} (β := A) 1
    (fun (f : R →ᵤ[{quasispectrum R a}] R) ↦
      cfcₙ.{u_2, u_3} (R := R) (p := p) ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) f) a)
    {f : R →ᵤ[{quasispectrum R a}] R |
      ContinuousOn (Y := R) ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) f)
          (quasispectrum R a) ∧
        f 0 = 0}
Tactic: by_cases ha : p a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : MetricSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalIsometricContinuousFunctionalCalculus R A p
a : A
pos :
  ∀ (ha : p a),
    LipschitzOnWith.{u_2, u_3} (β := A) 1
      (fun (f : R →ᵤ[{quasispectrum R a}] R) ↦
        cfcₙ.{u_2, u_3} (R := R) (p := p) ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) f) a)
      {f : R →ᵤ[{quasispectrum R a}] R |
        ContinuousOn (Y := R) ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) f)
            (quasispectrum R a) ∧
          f 0 = 0}
⊢ LipschitzOnWith.{u_2, u_3} (β := A) 1
    (fun (f : R →ᵤ[{quasispectrum R a}] R) ↦
      cfcₙ.{u_2, u_3} (R := R) (p := p) ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) f) a)
    {f : R →ᵤ[{quasispectrum R a}] R |
      ContinuousOn (Y := R) ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) f)
          (quasispectrum R a) ∧
        f 0 = 0}
have neg : ∀ (ha : ¬p a),
  LipschitzOnWith.{u_2, u_3} (β := A) 1
    (fun (f : R →ᵤ[{quasispectrum R a}] R) ↦
      cfcₙ.{u_2, u_3} (R := R) (p := p) ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) f) a)
    {f : R →ᵤ[{quasispectrum R a}] R |
      ContinuousOn (Y := R) ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) f)
          (quasispectrum R a) ∧
        f 0 = 0}
Tactic: by_cases ha : p a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : MetricSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalIsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
f : R →ᵤ[{quasispectrum R a}] R
hf :
  ContinuousOn (Y := R) ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) f) (quasispectrum R a)
hf0 : f 0 = 0
g : R →ᵤ[{quasispectrum R a}] R
hg :
  ContinuousOn (Y := R) ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) g) (quasispectrum R a)
hg0 : g 0 = 0
⊢ edist
      (cfcₙ.{u_2, u_3} (R := R) (p := p) ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) f) a)
      (cfcₙ.{u_2, u_3} (R := R) (p := p) ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) g)
        a) ≤
    (↑1 : ENNReal) * edist f g
have pos : edist (α := ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R)
    {
      toFun :=
        (quasispectrum R a).restrict (π := fun (a : R) ↦ R)
          ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) f),
      continuous_toFun := sorry, map_zero' := hf0 : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R }
    {
      toFun :=
        (quasispectrum R a).restrict (π := fun (a : R) ↦ R)
          ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) g),
      continuous_toFun := sorry, map_zero' := hg0 : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R } ≤
  (↑1 : ENNReal) * edist f g
Tactic: rw [cfcₙ_apply .., cfcₙ_apply .., isometry_cfcₙHom (R := R) a ha |>.edist_eq]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : MetricSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalIsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
f : R →ᵤ[{quasispectrum R a}] R
hf :
  ContinuousOn (Y := R) ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) f) (quasispectrum R a)
hf0 : f 0 = 0
g : R →ᵤ[{quasispectrum R a}] R
hg :
  ContinuousOn (Y := R) ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) g) (quasispectrum R a)
hg0 : g 0 = 0
⊢ edist (α := ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R)
      {
        toFun :=
          (quasispectrum R a).restrict (π := fun (a : R) ↦ R)
            ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) f),
        continuous_toFun := ⋯, map_zero' := hf0 : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R }
      {
        toFun :=
          (quasispectrum R a).restrict (π := fun (a : R) ↦ R)
            ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) g),
        continuous_toFun := ⋯, map_zero' := hg0 : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R } ≤
    (↑1 : ENNReal) * edist f g
have pos : edist (α := ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R)
    {
      toFun :=
        (quasispectrum R a).restrict (π := fun (a : R) ↦ R)
          ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) f),
      continuous_toFun := sorry, map_zero' := hf0 : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R }
    {
      toFun :=
        (quasispectrum R a).restrict (π := fun (a : R) ↦ R)
          ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) g),
      continuous_toFun := sorry, map_zero' := hg0 : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R } ≤
  edist f g
Tactic: simp only [ENNReal.coe_one, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : MetricSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalIsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
f : R →ᵤ[{quasispectrum R a}] R
hf :
  ContinuousOn (Y := R) ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) f) (quasispectrum R a)
hf0 : f 0 = 0
g : R →ᵤ[{quasispectrum R a}] R
hg :
  ContinuousOn (Y := R) ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) g) (quasispectrum R a)
hg0 : g 0 = 0
⊢ edist (α := ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R)
      {
        toFun :=
          (quasispectrum R a).restrict (π := fun (a : R) ↦ R)
            ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) f),
        continuous_toFun := ⋯, map_zero' := hf0 : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R }
      {
        toFun :=
          (quasispectrum R a).restrict (π := fun (a : R) ↦ R)
            ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) g),
        continuous_toFun := ⋯, map_zero' := hg0 : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R } ≤
    edist f g
have pos : edist
    (ContinuousMapZero.toContinuousMap
      {
        toFun :=
          (quasispectrum R a).restrict (π := fun (a : R) ↦ R)
            ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) f),
        continuous_toFun := sorry, map_zero' := hf0 : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R })
    (ContinuousMapZero.toContinuousMap
      {
        toFun :=
          (quasispectrum R a).restrict (π := fun (a : R) ↦ R)
            ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) g),
        continuous_toFun := sorry, map_zero' := hg0 : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R }) ≤
  edist f g
Tactic: rw [← ContinuousMapZero.isometry_toContinuousMap.edist_eq,
      edist_continuousRestrict_of_singleton hf hg]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : MetricSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalIsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
f : R →ᵤ[{quasispectrum R a}] R
hf :
  ContinuousOn (Y := R) ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) f) (quasispectrum R a)
hf0 : f 0 = 0
g : R →ᵤ[{quasispectrum R a}] R
hg :
  ContinuousOn (Y := R) ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) g) (quasispectrum R a)
hg0 : g 0 = 0
pos :
  edist
      (ContinuousMapZero.toContinuousMap
        {
          toFun :=
            (quasispectrum R a).restrict (π := fun (a : R) ↦ R)
              ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) f),
          continuous_toFun := ⋯, map_zero' := hf0 : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R })
      (ContinuousMapZero.toContinuousMap
        {
          toFun :=
            (quasispectrum R a).restrict (π := fun (a : R) ↦ R)
              ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) g),
          continuous_toFun := ⋯, map_zero' := hg0 : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R }) ≤
    edist f g
⊢ edist (α := ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R)
      {
        toFun :=
          (quasispectrum R a).restrict (π := fun (a : R) ↦ R)
            ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) f),
        continuous_toFun := ⋯, map_zero' := hf0 : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R }
      {
        toFun :=
          (quasispectrum R a).restrict (π := fun (a : R) ↦ R)
            ((toFun {quasispectrum R a} : (a : R →ᵤ[{quasispectrum R a}] R) → R → R) g),
        continuous_toFun := ⋯, map_zero' := hg0 : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R } ≤
    edist f g
have pos₁ : edist f g ≤ edist f g
Tactic: rw [← ContinuousMapZero.isometry_toContinuousMap.edist_eq,
      edist_continuousRestrict_of_singleton hf hg]
-- 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 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : MetricSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalIsometricContinuousFunctionalCalculus R A p
a : A
s : Set R
hs : quasispectrum R a ⊆ s
⊢ 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 ∧ f 0 = 0}
have h₂ : LipschitzWith (α := R →ᵤ[{s}] R) (β := R →ᵤ[{quasispectrum R a}] R) 1
  (Function.comp (β := R → R) (⇑(ofFun {quasispectrum R a}) : (a_1 : R → R) → R →ᵤ[{quasispectrum R a}] R)
    (⇑(toFun {s}) : (a : R →ᵤ[{s}] R) → R → R))
Tactic: have h₂ := lipschitzWith_one_ofFun_toFun' (𝔖 := {quasispectrum 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 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : MetricSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalIsometricContinuousFunctionalCalculus R A p
a : A
s : Set R
hs : quasispectrum R a ⊆ s
h₂ :
  LipschitzWith (α := R →ᵤ[{s}] R) (β := R →ᵤ[{quasispectrum R a}] R) 1
    (Function.comp (β := R → R) (⇑(ofFun {quasispectrum R a}) : (a_1 : R → R) → R →ᵤ[{quasispectrum 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 ∧ f 0 = 0}
have h₃ : LipschitzOnWith (α := R →ᵤ[{s}] R) (β := R →ᵤ[{quasispectrum R a}] R) 1
  (Function.comp (β := R → R) (⇑(ofFun {quasispectrum R a}) : (a_1 : R → R) → R →ᵤ[{quasispectrum 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 ∧ f 0 = 0}
Tactic: have h₃ := h₂.lipschitzOnWith (s := {f | ContinuousOn (toFun {s} f) (s) ∧ f 0 = 0})
-- 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)
⊢ CompactSpace.{u_2} (↑s : Type u_2)
have rwa : ∀ (hs : CompactSpace.{u_2} (↑s : Type u_2)) [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)), CompactSpace.{u_2} (↑s : Type u_2)
Tactic: rwa [isCompact_iff_compactSpace] at hs
Cleared hypotheses: hs, hs0, 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 : 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)
⊢ 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 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 (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)
⊢ 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)
      (star (ContinuousMapZero.id s))
have star_id : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦ star (a x)
Tactic: simp only [map_star, cfcₙHomSuperset_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 : 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
⊢ 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 frequently : ∀ u ∈ uniformity A,
  ∃ (F : X → A),
    Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
      ∀ (y : X),
        Membership.mem (α := A × A) u
          ((((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: apply continuous_of_uniform_approx_of_continuous