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 : 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
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (quasispectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (quasispectrum R a)
hF0 : ∀ᶠ (x : X) in l, F x 0 = 0
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
hf0 : f 0 = 0
ha : ¬p a
⊢ Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))

Tactic:
simpa [cfcₙ_apply_of_not_predicate a ha] using tendsto_const_nhds

Premises used: tendsto_const_nhds, cfcₙ_apply_of_not_predicate
-- 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 : 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
x₀ : X
h_tendsto : TendstoUniformlyOn f (f x₀) (𝓝 x₀) (quasispectrum R a)
hf : ∀ᶠ (x : X) in 𝓝 x₀, ContinuousOn (f x) (quasispectrum R a)
hf0 : ∀ᶠ (x : X) in 𝓝 x₀, f x 0 = 0
⊢ ContinuousAt.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) (f x) a) x₀

Tactic:
tendsto_cfcₙ_fun h_tendsto hf hf0

Premises used: tendsto_cfcₙ_fun, ContinuousAt
-- 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 : 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
x₀ : X
s : Set X
h_tendsto : TendstoUniformlyOn f (f x₀) (𝓝[s] x₀) (quasispectrum R a)
hf : ∀ᶠ (x : X) in 𝓝[s] x₀, ContinuousOn (f x) (quasispectrum R a)
hf0 : ∀ᶠ (x : X) in 𝓝[s] x₀, f x 0 = 0
⊢ ContinuousWithinAt.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) (f x) a) s x₀

Tactic:
tendsto_cfcₙ_fun h_tendsto hf hf0

Premises used: ContinuousWithinAt, tendsto_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 : 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 :
  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)) s
hf : ∀ x ∈ s, ContinuousOn (f x) (quasispectrum R a)
hf0 : ∀ x ∈ s, f x 0 = 0
⊢ ∀ 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

Tactic:
rw [ContinuousOn] at h_cont ⊢

Premises used: ContinuousOn
-- 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 : 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 :
  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)) s
hf : ∀ x ∈ s, ContinuousOn (f x) (quasispectrum R a)
hf0 : ∀ x ∈ s, f x 0 = 0
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
⊢ ∀ x ∈ s, ContinuousOn (f x) (quasispectrum R a)

Tactic:
rw [ContinuousOn] at h_cont ⊢

Premises used: ContinuousOn
-- 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 : 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 :
  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)) s
hf : ∀ x ∈ s, ContinuousOn (f x) (quasispectrum R a)
hf0 : ∀ x ∈ s, f x 0 = 0
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)
⊢ ∀ x ∈ s, f x 0 = 0

Tactic:
rw [ContinuousOn] at h_cont ⊢

Premises used: ContinuousOn
-- 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 : 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, 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

Premises used: ContinuousWithinAt, UniformOnFun.toFun_ofFun, UniformOnFun.tendsto_iff_tendstoUniformlyOn, forall_eq, Function.comp_def, Set.mem_singleton_iff
-- 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 : 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

Tactic:
fun x hx ↦ continuousWithinAt_cfcₙ_fun (h_cont x hx) ?_ ?_

Premises used: continuousWithinAt_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 : 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)
refine_2 : ∀ (x : X) (hx : x ∈ s), ∀ᶠ (x : X) in 𝓝[s] x, f x 0 = 0
⊢ ∀ x ∈ s, ContinuousWithinAt.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) (f x) a) s x

Tactic:
refine fun x hx ↦ continuousWithinAt_cfcₙ_fun (h_cont x hx) ?_ ?_

Premises used: continuousWithinAt_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 : 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 : X
hx : x ∈ s
h : ∀ (x : X) (hx : x ∈ s), ContinuousOn (f x) (quasispectrum R a)
⊢ ∀ᶠ (x : X) in 𝓝[s] x, ContinuousOn (f x) (quasispectrum R a)

Tactic:
filter_upwards [self_mem_nhdsWithin] with x hx

Premises used: self_mem_nhdsWithin
-- 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 : 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 : X
hx : x ∈ s
h : ∀ (x : X) (hx : x ∈ s), f x 0 = 0
⊢ ∀ᶠ (x : X) in 𝓝[s] x, f x 0 = 0

Tactic:
filter_upwards [self_mem_nhdsWithin] with x hx

Premises used: self_mem_nhdsWithin
-- 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 : 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_1 : X
hx_1 : x_1 ∈ s
x : X
hx : x ∈ s
⊢ ContinuousOn (f x) (quasispectrum 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 : 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_1 : X
hx_1 : x_1 ∈ s
x : X
hx : x ∈ s
⊢ f x 0 = 0

Tactic:
hf0 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 : 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_1 : X
hx_1 : x_1 ∈ s
x : X
hx : x ∈ s
⊢ ContinuousOn (f x) (quasispectrum R a)

Tactic:
exacts [hf x hx, hf0 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 : 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
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
⊢ Continuous[inst_13, inst_8] 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 : 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 :
  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:
h_cont.cfcₙ_fun (fun x _ ↦ hf x) (fun x _ ↦ hf0 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 : 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 :
  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:
exact h_cont.cfcₙ_fun (fun x _ ↦ hf x) (fun x _ ↦ hf0 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 : 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}
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}
⊢ 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
-- 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
      (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
⊢ edist.{u_3} (α := A)
      ((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)
      ((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)
        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 : 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 } ≤
    (↑1 : ENNReal) * edist f g
⊢ 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

Tactic:
rw [cfcₙ_apply .., cfcₙ_apply .., isometry_cfcₙHom (R := R) a ha |>.edist_eq]

Premises used: Isometry.edist_eq, isometry_cfcₙHom, cfcₙ_apply