awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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 (↑(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
⊢ 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

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 : 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
pos₁ pos₂ : edist f g ≤ 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

Tactic:
rw [← ContinuousMapZero.isometry_toContinuousMap.edist_eq,
      edist_continuousRestrict_of_singleton hf hg]

Premises used: Isometry.edist_eq, ContinuousMapZero.isometry_toContinuousMap, 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 : 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
⊢ 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:
simpa [cfcₙ_apply_of_not_predicate a ha] using LipschitzWith.const' 0 |>.lipschitzOnWith

Premises used: cfcₙ_apply_of_not_predicate, LipschitzWith.const', 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 : 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
⊢ Subset (α := Set R) (⋃₀ {quasispectrum 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 : 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
⊢ 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)
-- 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 : 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 (α := 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})
-- 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 : 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))
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}
⊢ 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}

Tactic:
simpa using lipschitzOnWith_cfcₙ_fun R a |>.comp h₃ (fun f ↦ .imp_left fun hf ↦ hf.mono hs)

Premises used: And.imp_left, lipschitzOnWith_cfcₙ_fun, 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 : 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)
rwa rwa₁ rwa₂ 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)
⊢ 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 : 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)

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 : 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) 0

Tactic:
simpa [map_zero] using continuous_const

Premises used: continuous_const, map_zero
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : ContinuousStar A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst_8 : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
⊢ 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)

Tactic:
simpa only [cfcₙHomSuperset_id]

Premises used: cfcₙHomSuperset_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 : 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)
star_id : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦ star (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)
      (star (ContinuousMapZero.id s))

Tactic:
simp only [map_star, cfcₙHomSuperset_id]

Premises used: StarHomClass.map_star, cfcₙHomSuperset_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 : 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) ↦ star (a x)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : ContinuousStar A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst_8 : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
f g : C((↑s : Type u_2), 𝕜)₀
hf :
  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
hg :
  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 + g)

Tactic:
simpa only [map_add] using hf.add hg

Premises used: map_add, Continuous.add
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : ContinuousStar A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst_8 : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
f g : C((↑s : Type u_2), 𝕜)₀
hf :
  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
hg :
  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 * g)

Tactic:
simpa only [map_mul] using hf.mul hg

Premises used: Continuous.mul, map_mul
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : ContinuousStar A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst_8 : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
r : 𝕜
f : C((↑s : Type u_2), 𝕜)₀
hf :
  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
⊢ 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)
      (r • f)

Tactic:
simpa only [map_smul] using hf.const_smul r

Premises used: Continuous.const_smul, map_smul
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : ContinuousStar A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst_8 : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
f : C((↑s : Type u_2), 𝕜)₀
hf :
  ∃ᶠ (g : C((↑s : Type u_2), 𝕜)₀) in 𝓝 f,
    Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      ((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A) g
frequently :
  ∀ 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)
⊢ 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

Tactic:
apply continuous_of_uniform_approx_of_continuous

Premises used: continuous_of_uniform_approx_of_continuous
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : ContinuousStar A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst_8 : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
f : C((↑s : Type u_2), 𝕜)₀
hf :
  ∃ᶠ (g : C((↑s : Type u_2), 𝕜)₀) in 𝓝 f,
    Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      ((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A) g
⊢ ∀ ⦃s_1 t : Set (A × A)⦄,
    s_1 ⊆ t →
      (∃ (F : X → A),
          Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
            ∀ (y : X),
              Membership.mem (α := A × A) s_1
                ((((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) :
                        (a : C((↑s : Type u_2), 𝕜)₀) → A)
                      f,
                    F y) :
                  A × A)) →
        ∃ (F : X → A),
          Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
            ∀ (y : X),
              Membership.mem (α := A × A) t
                ((((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) :
                        (a : C((↑s : Type u_2), 𝕜)₀) → A)
                      f,
                    F y) :
                  A × A)

Tactic:
aesop