awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
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 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : TopologicalSpace X
f : X → R → R
a : A
s : Set X
hf : ∀ x ∈ s, ContinuousOn (f x) (spectrum R a)
h_cont : ∀ x ∈ s, TendstoUniformlyOn (fun (x : X) ↦ f x) (f x) (𝓝[s] x) (spectrum R a)
x_1 : X
hx_1 : x_1 ∈ s
x : X
hx : x ∈ s
⊢ ContinuousOn (f x) (spectrum R a)

Tactic:
hf x hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
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 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : TopologicalSpace X
f : X → R → R
a : A
s : Set X
hf : ∀ x ∈ s, ContinuousOn (f x) (spectrum R a)
h_cont : ∀ x ∈ s, TendstoUniformlyOn (fun (x : X) ↦ f x) (f x) (𝓝[s] x) (spectrum R a)
x_1 : X
hx_1 : x_1 ∈ s
x : X
hx : x ∈ s
⊢ ContinuousOn (f x) (spectrum R a)

Tactic:
exact hf x hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
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 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : TopologicalSpace X
f : X → R → R
a : A
h_cont :
  Continuous[inst_10, topologicalSpace R R {spectrum R a}] fun (x : X) ↦
    (ofFun {spectrum R a} : (a_1 : R → R) → R →ᵤ[{spectrum R a}] R) (f x)
hf : ∀ (x : X), ContinuousOn (f x) (spectrum R a)
rw :
  ∀
    (h_cont :
      ContinuousOn.{u_1, u_2} (Y := R →ᵤ[{spectrum R a}] R)
        (fun (x : X) ↦ (ofFun {spectrum R a} : (a_1 : R → R) → R →ᵤ[{spectrum R a}] R) (f x)) Set.univ)
    (hf : ∀ (x : X), ContinuousOn (f x) (spectrum R a)),
    ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfc (p := p) (f x) a) Set.univ
⊢ Continuous[inst_10, inst_7] fun (x : X) ↦ cfc (p := p) (f x) a

Tactic:
rw [← continuousOn_univ] at h_cont ⊢

Premises used: continuousOn_univ
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
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 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : TopologicalSpace X
f : X → R → R
a : A
h_cont :
  ContinuousOn.{u_1, u_2} (Y := R →ᵤ[{spectrum R a}] R)
    (fun (x : X) ↦ (ofFun {spectrum R a} : (a_1 : R → R) → R →ᵤ[{spectrum R a}] R) (f x)) Set.univ
hf : ∀ (x : X), ContinuousOn (f x) (spectrum R a)
⊢ ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfc (p := p) (f x) a) Set.univ

Tactic:
h_cont.cfc_fun (fun x _ ↦ hf x)

Premises used: ContinuousOn.cfc_fun
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
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 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : TopologicalSpace X
f : X → R → R
a : A
h_cont :
  ContinuousOn.{u_1, u_2} (Y := R →ᵤ[{spectrum R a}] R)
    (fun (x : X) ↦ (ofFun {spectrum R a} : (a_1 : R → R) → R →ᵤ[{spectrum R a}] R) (f x)) Set.univ
hf : ∀ (x : X), ContinuousOn (f x) (spectrum R a)
⊢ ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfc (p := p) (f x) a) Set.univ

Tactic:
exact h_cont.cfc_fun (fun x _ ↦ hf x)

Premises used: ContinuousOn.cfc_fun
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
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
pos :
  ∀ (ha : p a),
    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)}
neg :
  ∀ (ha : ¬p a),
    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 →ᵤ[{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)}

Tactic:
by_cases ha : p a
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
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
ha : p a
f : R →ᵤ[{spectrum R a}] R
hf :
  Membership.mem (γ := Set (R →ᵤ[{spectrum R a}] R))
    {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)}
    f
g : R →ᵤ[{spectrum R a}] R
hg :
  Membership.mem (γ := Set (R →ᵤ[{spectrum R a}] R))
    {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)}
    g
pos :
  edist (cfc.{u_2, u_3} (R := R) (p := p) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f) a)
      (cfc.{u_2, u_3} (R := R) (p := p) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) g) a) ≤
    (↑1 : ENNReal) * edist f g
⊢ edist.{u_3} (α := A)
      ((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)
      ((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)
        g) ≤
    (↑1 : ENNReal) * edist f g

Tactic:
simp only
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
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
ha : p a
f : R →ᵤ[{spectrum R a}] R
hf :
  Membership.mem (γ := Set (R →ᵤ[{spectrum R a}] R))
    {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)}
    f
g : R →ᵤ[{spectrum R a}] R
hg :
  Membership.mem (γ := Set (R →ᵤ[{spectrum R a}] R))
    {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)}
    g
pos :
  edist
      {
        toFun :=
          (spectrum R a).restrict (π := fun (a : R) ↦ R)
            ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f),
        continuous_toFun := ⋯ : C((↑(spectrum R a) : Type u_2), R) }
      {
        toFun :=
          (spectrum R a).restrict (π := fun (a : R) ↦ R)
            ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) g),
        continuous_toFun := ⋯ : C((↑(spectrum R a) : Type u_2), R) } ≤
    (↑1 : ENNReal) * edist f g
⊢ edist (cfc.{u_2, u_3} (R := R) (p := p) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f) a)
      (cfc.{u_2, u_3} (R := R) (p := p) ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) g) a) ≤
    (↑1 : ENNReal) * edist f g

Tactic:
rw [cfc_apply .., cfc_apply .., isometry_cfcHom (R := R) a ha |>.edist_eq]

Premises used: Isometry.edist_eq, cfc_apply, isometry_cfcHom
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
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
ha : p a
f : R →ᵤ[{spectrum R a}] R
hf :
  Membership.mem (γ := Set (R →ᵤ[{spectrum R a}] R))
    {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)}
    f
g : R →ᵤ[{spectrum R a}] R
hg :
  Membership.mem (γ := Set (R →ᵤ[{spectrum R a}] R))
    {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)}
    g
pos :
  edist
      {
        toFun :=
          (spectrum R a).restrict (π := fun (a : R) ↦ R)
            ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f),
        continuous_toFun := ⋯ : C((↑(spectrum R a) : Type u_2), R) }
      {
        toFun :=
          (spectrum R a).restrict (π := fun (a : R) ↦ R)
            ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) g),
        continuous_toFun := ⋯ : C((↑(spectrum R a) : Type u_2), R) } ≤
    edist f g
⊢ edist
      {
        toFun :=
          (spectrum R a).restrict (π := fun (a : R) ↦ R)
            ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f),
        continuous_toFun := ⋯ : C((↑(spectrum R a) : Type u_2), R) }
      {
        toFun :=
          (spectrum R a).restrict (π := fun (a : R) ↦ R)
            ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) g),
        continuous_toFun := ⋯ : C((↑(spectrum R a) : Type u_2), R) } ≤
    (↑1 : ENNReal) * edist f g

Tactic:
simp only [ENNReal.coe_one, one_mul]

Premises used: ENNReal.coe_one, one_mul
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
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
ha : p a
f : R →ᵤ[{spectrum R a}] R
hf :
  Membership.mem (γ := Set (R →ᵤ[{spectrum R a}] R))
    {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)}
    f
g : R →ᵤ[{spectrum R a}] R
hg :
  Membership.mem (γ := Set (R →ᵤ[{spectrum R a}] R))
    {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)}
    g
pos pos₁ : edist f g ≤ edist f g
⊢ edist
      {
        toFun :=
          (spectrum R a).restrict (π := fun (a : R) ↦ R)
            ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) f),
        continuous_toFun := ⋯ : C((↑(spectrum R a) : Type u_2), R) }
      {
        toFun :=
          (spectrum R a).restrict (π := fun (a : R) ↦ R)
            ((toFun {spectrum R a} : (a : R →ᵤ[{spectrum R a}] R) → R → R) g),
        continuous_toFun := ⋯ : C((↑(spectrum R a) : Type u_2), R) } ≤
    edist f g

Tactic:
rw [edist_continuousRestrict_of_singleton hf hg]

Premises used: UniformOnFun.edist_continuousRestrict_of_singleton
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
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
ha : ¬p a
⊢ 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)}

Tactic:
simpa [cfc_apply_of_not_predicate a ha] using LipschitzWith.const' 0 |>.lipschitzOnWith

Premises used: LipschitzWith.const', cfc_apply_of_not_predicate, LipschitzWith.lipschitzOnWith, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
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
⊢ 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)}

Tactic:
have h₁ := lipschitzOnWith_cfc_fun R a
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
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)}
⊢ Subset (α := Set R) (⋃₀ {spectrum R a}) (⋃₀ {s})

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
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)}
⊢ 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)
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
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 (α := 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)})
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
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))
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}
⊢ 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}

Tactic:
simpa using h₁.comp h₃ (fun f hf ↦ hf.mono hs)

Premises used: ContinuousOn.mono, LipschitzOnWith.comp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
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)
rwa rwa₁ rwa₂ 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)
⊢ CompactSpace.{u_2} (↑s : Type u_2)

Tactic:
rwa [isCompact_iff_compactSpace] at hs

Premises used: isCompact_iff_compactSpace
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
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:
have : CompactSpace s := by rwa [isCompact_iff_compactSpace] at hs
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
a : X → A
ha_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
r : 𝕜
⊢ 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
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
a : X → A
ha_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this_1 : CompactSpace.{u_2} (↑s : Type u_2)
r : 𝕜
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)
⊢ 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)

Tactic:
simpa only [this, AlgHomClass.commutes] using continuous_const

Premises used: continuous_const, AlgHomClass.commutes
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
a : X → A
ha_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
id : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦ a x
⊢ Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A)
      (ContinuousMap.restrict s (ContinuousMap.id 𝕜))

Tactic:
simp only [cfcHomSuperset_id]

Premises used: cfcHomSuperset_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
a : X → A
ha_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
⊢ Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦ a x

Tactic:
fun_prop