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
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (spectrum R a)}
⊢ Set.range (ι := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) ∈ l

Tactic:
simpa
-- 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
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (spectrum R a)}
pos :
  Tendsto (α := { x : X // x ∈ s }) ((fun (x : X) ↦ cfc (p := p) (F x) a) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ s))
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l) (𝓝 (cfc (p := p) f a))
⊢ Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))

Tactic:
rw [← tendsto_comap'_iff (i := ((↑) : s → X)) (by simpa)]

Premises used: Filter.tendsto_comap'_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 : 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
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (spectrum R a)}
h : ∀ (x : { x : X // x ∈ s }), (((fun (x : X) ↦ cfc (p := p) (F x) a) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ s)) x : A)
| Tendsto (α := { x : X // x ∈ s }) ((fun (x : X) ↦ cfc (p := p) (F x) a) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ s))
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l) (𝓝 (cfc (p := p) f a))

Tactic:
enter [1, x]
-- 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
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (spectrum R a)}
x : { x : X // x ∈ s }
h :
  ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_2), R)) → A)
      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := ⋯ :
        C((↑(spectrum R a) : Type u_2), R) } :
    A)
| (((fun (x : X) ↦ cfc (p := p) (F x) a) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ s)) x : A)

Tactic:
rw [Function.comp_apply, cfc_apply (hf := x.2)]

Premises used: cfc_apply, Function.comp_apply, Subtype.property
-- 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
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (spectrum R a)}
h :
  ∀ (x : { x : X // x ∈ s }),
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_2), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := ⋯ :
          C((↑(spectrum R a) : Type u_2), R) } :
      A)
| Tendsto (α := { x : X // x ∈ s }) ((fun (x : X) ↦ cfc (p := p) (F x) a) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ s))
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l) (𝓝 (cfc (p := p) f a))

Tactic:
enter [1, x]
      rw [Function.comp_apply, cfc_apply (hf := x.2)]

Premises used: Function.comp_apply
-- 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
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (spectrum R a)}
pos :
  Tendsto
    (fun (x : { x : X // x ∈ s }) ↦
      (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_2), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := ⋯ :
          C((↑(spectrum R a) : Type u_2), R) })
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l) (𝓝 (cfc (p := p) f a))
⊢ Tendsto (α := { x : X // x ∈ s }) ((fun (x : X) ↦ cfc (p := p) (F x) a) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ s))
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l) (𝓝 (cfc (p := p) f a))

Tactic:
conv =>
      enter [1, x]
      rw [Function.comp_apply, cfc_apply (hf := x.2)]

Premises used: Function.comp_apply
-- 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
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (spectrum R a)}
pos :
  Tendsto.{u_1, u_3} (β := A)
    (fun (x : { x : X // x ∈ s }) ↦
      ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_2), R)) → A)
          { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := ⋯ :
            C((↑(spectrum R a) : Type u_2), R) } :
        A))
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l)
    (𝓝
        ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_2), R)) → A)
          { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
            C((↑(spectrum R a) : Type u_2), R) }) :
      Filter A)
⊢ Tendsto
    (fun (x : { x : X // x ∈ s }) ↦
      (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_2), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := ⋯ :
          C((↑(spectrum R a) : Type u_2), R) })
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l) (𝓝 (cfc (p := p) f a))

Tactic:
rw [cfc_apply ..]

Premises used: cfc_apply
-- 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
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (spectrum R a)}
pos :
  Tendsto
    (fun (x : { x : X // x ∈ s }) ↦
      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := ⋯ })
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l)
    (𝓝
      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
        C((↑(spectrum R a) : Type u_2), R) })
⊢ Tendsto.{u_1, u_3} (β := A)
    (fun (x : { x : X // x ∈ s }) ↦
      ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_2), R)) → A)
          { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := ⋯ :
            C((↑(spectrum R a) : Type u_2), R) } :
        A))
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l)
    (𝓝
        ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_2), R)) → A)
          { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
            C((↑(spectrum R a) : Type u_2), R) }) :
      Filter A)

Tactic:
apply cfcHom_continuous _ |>.tendsto _ |>.comp

Premises used: cfcHom_continuous, Continuous.tendsto, Filter.Tendsto.comp
-- 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
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (spectrum R a)}
pos :
  TendstoUniformlyOn (fun (x : { x : X // x ∈ s }) ↦ F (↑x : X)) f (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l)
    (spectrum R a)
⊢ Tendsto
    (fun (x : { x : X // x ∈ s }) ↦
      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := ⋯ })
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l)
    (𝓝
      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
        C((↑(spectrum R a) : Type u_2), R) })

Tactic:
rw [hf.tendsto_restrict_iff_tendstoUniformlyOn Subtype.property]
-- 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
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (spectrum R a)}
t : Set (R × R)
pos : t ∈ uniformity R → ∀ᶠ (b : X) in l, ∀ (a_2 : X) (b_1 : a_2 ∈ s), a_2 = b → ∀ x ∈ spectrum R a, (f x, F a_2 x) ∈ t
⊢ t ∈ uniformity R →
    ∀ᶠ (n : { x : X // x ∈ s }) in comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l,
      ∀ x ∈ spectrum R a, (f x, (fun (x : { x : X // x ∈ s }) ↦ F (↑x : X)) n x) ∈ t

Tactic:
simp only [eventually_comap, Subtype.forall]

Premises used: Subtype.forall, Filter.eventually_comap
-- 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
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (spectrum R a)}
t : Set (R × R)
pos :
  ∀ (ht : t ∈ uniformity R) (x : X) (this : ∀ x_1 ∈ spectrum R a, (f x_1, F x x_1) ∈ t) (a_1 : X) (b : a_1 ∈ s),
    a_1 = x → ∀ x ∈ spectrum R a, (f x, F a_1 x) ∈ t
⊢ t ∈ uniformity R → ∀ᶠ (b : X) in l, ∀ (a_2 : X) (b_1 : a_2 ∈ s), a_2 = b → ∀ x ∈ spectrum R a, (f x, F a_2 x) ∈ t

Tactic:
peel h_tendsto t with ht x _
-- 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
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (spectrum R a)}
t : Set (R × R)
ht : t ∈ uniformity R
x : X
this : ∀ x_1 ∈ spectrum R a, (f x_1, F x x_1) ∈ t
⊢ ∀ (a_1 : X) (b : a_1 ∈ s), a_1 = x → ∀ x ∈ spectrum R a, (f x, F a_1 x) ∈ t

Tactic:
simp_all
-- 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
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
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 : 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
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
inl :
  ∀ (h_tendsto : TendstoUniformlyOn F f ⊥ (spectrum R a)) (hF : ∀ᶠ (x : X) in ⊥, ContinuousOn (F x) (spectrum R a)),
    Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) ⊥ (𝓝 (cfc (p := p) f a))
inr inr₁ : ∀ (hl : l.NeBot), Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))
inr₂ :
  ∀ (hl : l.NeBot) (hf : ContinuousOn f (spectrum R a)),
    Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))
pos :
  ∀ (hl : l.NeBot) (hf : ContinuousOn f (spectrum R a)) (ha : p a),
    Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))
neg neg₁ :
  ∀ (hl : l.NeBot) (hf : ContinuousOn f (spectrum R a)) (ha : ¬p a),
    Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))
⊢ Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))

Tactic:
open scoped ContinuousFunctionalCalculus in
  obtain (rfl | hl) := l.eq_or_neBot
  · simp
  have hf := h_tendsto.continuousOn hF.frequently
  by_cases ha : p a
  · let s : Set X := {x | ContinuousOn (F x) (spectrum R a)}
    rw [← tendsto_comap'_iff (i := ((↑) : s → X)) (by simpa)]
    conv =>
      enter [1, x]
      rw [Function.comp_apply, cfc_apply (hf := x.2)]
    rw [cfc_apply ..]
    apply cfcHom_continuous _ |>.tendsto _ |>.comp
    rw [hf.tendsto_restrict_iff_tendstoUniformlyOn Subtype.property]
    intro t
    simp only [eventually_comap, Subtype.forall]
    peel h_tendsto t with ht x _
    simp_all
  · simpa [cfc_apply_of_not_predicate a ha] using tendsto_const_nhds

Premises used: cfcHom_continuous, tendsto_const_nhds, Subtype.forall, Continuous.tendsto, Filter.eq_or_neBot, cfc_apply, Function.comp_apply, Filter.eventually_comap, Filter.Tendsto.comp, rfl, ContinuousFunctionalCalculus
-- 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
x₀ : X
h_tendsto : TendstoUniformlyOn f (f x₀) (𝓝 x₀) (spectrum R a)
hf : ∀ᶠ (x : X) in 𝓝 x₀, ContinuousOn (f x) (spectrum R a)
⊢ ContinuousAt.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfc (p := p) (f x) a) x₀

Tactic:
tendsto_cfc_fun h_tendsto hf

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 : 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
x₀ : X
s : Set X
h_tendsto : TendstoUniformlyOn f (f x₀) (𝓝[s] x₀) (spectrum R a)
hf : ∀ᶠ (x : X) in 𝓝[s] x₀, ContinuousOn (f x) (spectrum R a)
⊢ 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

Premises used: tendsto_cfc_fun, ContinuousWithinAt
-- 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
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)) s
hf : ∀ x ∈ s, ContinuousOn (f x) (spectrum R a)
⊢ ∀ x ∈ s,
    ContinuousWithinAt.{u_1, u_2} (Y := R →ᵤ[{spectrum R a}] R)
      (fun (x : X) ↦ (ofFun {spectrum R a} : (a_2 : R → R) → R →ᵤ[{spectrum 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 : 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
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)) s
hf : ∀ x ∈ s, ContinuousOn (f x) (spectrum R a)
h_cont₁ :
  ∀ x ∈ s,
    ContinuousWithinAt.{u_1, u_2} (Y := R →ᵤ[{spectrum R a}] R)
      (fun (x : X) ↦ (ofFun {spectrum R a} : (a_2 : R → R) → R →ᵤ[{spectrum R a}] R) (f x)) s x
⊢ ∀ x ∈ s, ContinuousOn (f x) (spectrum 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 : 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
h_cont :
  ∀ x ∈ s,
    ContinuousWithinAt.{u_1, u_2} (Y := R →ᵤ[{spectrum R a}] R)
      (fun (x : X) ↦ (ofFun {spectrum R a} : (a_2 : R → R) → R →ᵤ[{spectrum R a}] R) (f x)) s x
hf : ∀ x ∈ s, ContinuousOn (f x) (spectrum R a)
⊢ ∀ x ∈ s, TendstoUniformlyOn (fun (x : X) ↦ f x) (f x) (𝓝[s] x) (spectrum 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 : 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 ∈ 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 : 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)
refine : ∀ (x : X) (hx : x ∈ s), ∀ᶠ (x : X) in 𝓝[s] x, ContinuousOn (f x) (spectrum R a)
⊢ ∀ 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 : 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 : X
hx : x ∈ s
h : ∀ (x : X) (hx : x ∈ s), ContinuousOn (f x) (spectrum R a)
⊢ ∀ᶠ (x : X) in 𝓝[s] x, ContinuousOn (f x) (spectrum R a)

Tactic:
filter_upwards [self_mem_nhdsWithin] with x hx

Premises used: self_mem_nhdsWithin