awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
𝕜 : 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
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
hf0 : f 0 = 0
hs0 : 0 ∈ s
x : (↑{a : A | p a ∧ quasispectrum 𝕜 a ⊆ s} : Type u_3)
h :
  Eq.{u_3 + 1} (α := A)
    ((cfcₙHom (p := p) ⋯ : (a : ContinuousMapZero (↑(quasispectrum 𝕜 (↑x : A)) : Type u_2) 𝕜) → A)
        { toFun := (quasispectrum 𝕜 (↑x : A)).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯,
          map_zero' := hf0 } :
      A)
    ((cfcₙHom (p := p) ⋯ : (a : ContinuousMapZero (↑(quasispectrum 𝕜 (↑x : A)) : Type u_2) 𝕜) → A)
        (ContinuousMapZero.comp
          { toFun := s.restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯, map_zero' := hf0 }
          { toFun := Subtype.map (p := Membership.mem (quasispectrum 𝕜 (↑x : A))) (q := Membership.mem s) id ⋯,
            continuous_toFun := ⋯, map_zero' := ⋯ }) :
      A)
⊢ Eq (α := A)
    (Set.restrict (π := fun (a : A) ↦ A) {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s} (fun (x : A) ↦ cfcₙ (p := p) f x) x : A)
    (((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : ContinuousMapZero (↑s : Type u_2) 𝕜 →⋆ₙₐ[𝕜] A) :
          (a : ContinuousMapZero (↑s : Type u_2) 𝕜) → A)
        { toFun := s.restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯, map_zero' := hf0 } :
      A)

Tactic:
rw [cfcₙHomSuperset_apply, Set.restrict_apply, cfcₙ_apply _ _ (hf.mono x.2.2) hf0 x.2.1]

Premises used: Set.restrict_apply, And.right, And.left, ContinuousOn.mono, cfcₙHomSuperset_apply, cfcₙ_apply, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
𝕜 : 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
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
hf0 : f 0 = 0
hs0 : 0 ∈ s
x : (↑{a : A | p a ∧ quasispectrum 𝕜 a ⊆ s} : Type u_3)
⊢ Eq.{u_3 + 1} (α := A)
    ((cfcₙHom (p := p) ⋯ : (a : ContinuousMapZero (↑(quasispectrum 𝕜 (↑x : A)) : Type u_2) 𝕜) → A)
        { toFun := (quasispectrum 𝕜 (↑x : A)).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯,
          map_zero' := hf0 } :
      A)
    ((cfcₙHom (p := p) ⋯ : (a : ContinuousMapZero (↑(quasispectrum 𝕜 (↑x : A)) : Type u_2) 𝕜) → A)
        (ContinuousMapZero.comp
          { toFun := s.restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯, map_zero' := hf0 }
          { toFun := Subtype.map (p := Membership.mem (quasispectrum 𝕜 (↑x : A))) (q := Membership.mem s) id ⋯,
            continuous_toFun := ⋯, map_zero' := ⋯ }) :
      A)

Tactic:
congr!
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
𝕜 : 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
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
hf0 : f 0 = 0
hs0 : 0 ∉ s
⊢ ContinuousOn (Y := A) (fun (x : A) ↦ cfcₙ (p := p) f x) ∅

Tactic:
continuousOn_empty _

Premises used: continuousOn_empty
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
𝕜 : 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
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
hf0 : f 0 = 0
hs0 : 0 ∉ s
h : Eq.{u_3 + 1} (α := Set A) {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s} ∅
⊢ ContinuousOn (Y := A) (fun (x : A) ↦ cfcₙ (p := p) f x) {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s}

Tactic:
convert! continuousOn_empty _

Premises used: continuousOn_empty
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
𝕜 : 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
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
hf0 : f 0 = 0
hs0 : 0 ∉ s
h : ∀ (x : A), x ∉ {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s}
⊢ Eq.{u_3 + 1} (α := Set A) {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s} ∅

Tactic:
rw [Set.eq_empty_iff_forall_notMem]

Premises used: Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
𝕜 : 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
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
hf0 : f 0 = 0
hs0 : 0 ∉ s
⊢ ∀ (x : A), x ∉ {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s}

Tactic:
fun a ha ↦ hs0 <| ha.2 <| quasispectrum.zero_mem 𝕜 a

Premises used: quasispectrum.zero_mem, And.right, Not
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
𝕜 : 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
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
hf0 : f 0 = 0
hs0 : 0 ∉ s
⊢ ∀ (x : A), x ∉ {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s}

Tactic:
exact fun a ha ↦ hs0 <| ha.2 <| quasispectrum.zero_mem 𝕜 a
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
𝕜 : 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
s : Set 𝕜
hs : IsCompact s
⊢ ContinuousOn (Y := A)
    (fun (fa : Prod.{u_2, u_3} (𝕜 →ᵤ[{s}] 𝕜) A) ↦
      cfcₙ.{u_2, u_3} (R := 𝕜) (p := p) ((toFun {s} : (a : 𝕜 →ᵤ[{s}] 𝕜) → 𝕜 → 𝕜) fa.1) fa.2)
    (SProd.sprod (α := Set (𝕜 →ᵤ[{s}] 𝕜)) (β := Set A)
      {f : 𝕜 →ᵤ[{s}] 𝕜 | ContinuousOn (Y := 𝕜) ((toFun {s} : (a : 𝕜 →ᵤ[{s}] 𝕜) → 𝕜 → 𝕜) f) s ∧ f 0 = 0}
      {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s})

Tactic:
continuousOn_prod_of_continuousOn_lipschitzOnWith _ 1
    (fun f hf ↦ continuousOn_cfcₙ A hs ((toFun {s}) f) hf.1 hf.2)
    (fun a ⟨_, ha'⟩ ↦ lipschitzOnWith_cfcₙ_fun_of_subset a ha')

Premises used: cfcₙ, setOf, continuousOn_cfcₙ, _private.0.continuousOn_cfcₙ_setProd.match_1, continuousOn_prod_of_continuousOn_lipschitzOnWith, Prod.mk, UniformOnFun.toFun, Prod.fst, And, And.right, And.left, lipschitzOnWith_cfcₙ_fun_of_subset, LipschitzOnWith, ContinuousOn, Singleton.singleton, OfNat.ofNat, Eq, Prod.snd, DFunLike.coe
-- 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
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
a : X → A
a₀ : A
l : Filter X
ha_tendsto : Tendsto a l (𝓝 a₀)
ha : ∀ᶠ (x : X) in l, quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in l, p (a x)
ha₀ : quasispectrum 𝕜 a₀ ⊆ s
ha₀' : p a₀
hf : ContinuousOn f s
hf0 : f 0 = 0
apply : Tendsto a l (𝓝[{a : A | p a ∧ quasispectrum 𝕜 a ⊆ s}] a₀)
⊢ Tendsto (fun (x : X) ↦ cfcₙ (p := p) f (a x)) l (𝓝 (cfcₙ (p := p) f a₀))

Tactic:
apply continuousOn_cfcₙ A hs f |>.continuousWithinAt ⟨ha₀', ha₀⟩ |>.tendsto.comp

Premises used: continuousOn_cfcₙ, And.intro, Filter.Tendsto.comp, ContinuousWithinAt.tendsto, ContinuousOn.continuousWithinAt
-- 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
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
a : X → A
a₀ : A
l : Filter X
ha_tendsto : Tendsto a l (𝓝 a₀)
ha : ∀ᶠ (x : X) in l, quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in l, p (a x)
ha₀ : quasispectrum 𝕜 a₀ ⊆ s
ha₀' : p a₀
hf : ContinuousOn f s
hf0 : f 0 = 0
rw : Tendsto a l (𝓝 a₀) ∧ ∀ᶠ (n : X) in l, Membership.mem (γ := Set A) {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s} (a n)
⊢ Tendsto a l (𝓝[{a : A | p a ∧ quasispectrum 𝕜 a ⊆ s}] a₀)

Tactic:
rw [tendsto_nhdsWithin_iff]

Premises used: tendsto_nhdsWithin_iff
-- 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
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
a : X → A
a₀ : A
l : Filter X
ha_tendsto : Tendsto a l (𝓝 a₀)
ha : ∀ᶠ (x : X) in l, quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in l, p (a x)
ha₀ : quasispectrum 𝕜 a₀ ⊆ s
ha₀' : p a₀
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ Tendsto a l (𝓝 a₀) ∧ ∀ᶠ (n : X) in l, Membership.mem (γ := Set A) {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s} (a n)

Tactic:
⟨ha_tendsto, ha'.and ha⟩

Premises used: Filter.Eventually.and, And.intro
-- 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
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
a : X → A
a₀ : A
l : Filter X
ha_tendsto : Tendsto a l (𝓝 a₀)
ha : ∀ᶠ (x : X) in l, quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in l, p (a x)
ha₀ : quasispectrum 𝕜 a₀ ⊆ s
ha₀' : p a₀
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ Tendsto a l (𝓝 a₀) ∧ ∀ᶠ (n : X) in l, Membership.mem (γ := Set A) {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s} (a n)

Tactic:
exact ⟨ha_tendsto, ha'.and ha⟩
-- 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
f : 𝕜 → 𝕜
a : X → A
x₀ : X
ha_cont : ContinuousAt a x₀
ha : ∀ᶠ (x : X) in 𝓝 x₀, quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in 𝓝 x₀, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ ContinuousAt.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) f (a x)) x₀

Tactic:
ha_cont.tendsto.cfcₙ hs f ha ha' ha.self_of_nhds ha'.self_of_nhds

Premises used: Filter.Eventually.self_of_nhds, ContinuousAt, Filter.Tendsto.cfcₙ, ContinuousAt.tendsto
-- 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
f : 𝕜 → 𝕜
a : X → A
x₀ : X
t : Set X
hx₀ : x₀ ∈ t
ha_cont : ContinuousWithinAt a t x₀
ha : ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in 𝓝[t] x₀, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ ContinuousWithinAt.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) f (a x)) t x₀

Tactic:
ha_cont.tendsto.cfcₙ hs f ha ha' (ha.self_of_nhdsWithin hx₀) (ha'.self_of_nhdsWithin hx₀)

Premises used: Filter.Eventually.self_of_nhdsWithin, ContinuousWithinAt, Filter.Tendsto.cfcₙ, ContinuousWithinAt.tendsto
-- 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 : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ContinuousOn a t
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
⊢ ∀ x ∈ t, ContinuousWithinAt a t x

Tactic:
rw [ContinuousOn] at ha_cont ⊢

Premises used: ContinuousOn
-- 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 : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ContinuousOn a t
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
ha_cont₁ : ∀ x ∈ t, ContinuousWithinAt a t x
⊢ ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ s x₀

Tactic:
rw [ContinuousOn] at ha_cont ⊢

Premises used: ContinuousOn
-- 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 : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ContinuousOn a t
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
ha_cont₁ : ∀ x ∈ t, ContinuousWithinAt a t x
ha₁ : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
⊢ ∀ x ∈ t, p (a x)

Tactic:
rw [ContinuousOn] at ha_cont ⊢

Premises used: ContinuousOn
-- 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 : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ContinuousOn a t
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
ha_cont₁ : ∀ x ∈ t, ContinuousWithinAt a t x
ha₁ : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
ha'₁ : ∀ x ∈ t, p (a x)
⊢ ∀ x ∈ t, ContinuousOn f (s x)

Tactic:
rw [ContinuousOn] at ha_cont ⊢

Premises used: ContinuousOn
-- 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 : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ContinuousOn a t
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
ha_cont₁ : ∀ x ∈ t, ContinuousWithinAt a t x
ha₁ : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
ha'₁ : ∀ x ∈ t, p (a x)
hf₁ : ∀ x ∈ t, ContinuousOn f (s x)
⊢ f 0 = 0

Tactic:
rw [ContinuousOn] at ha_cont ⊢

Premises used: ContinuousOn
-- 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 : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
⊢ ∀ x ∈ t, ContinuousWithinAt.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) f (a x)) t x

Tactic:
fun x hx ↦ (ha_cont x hx).cfcₙ (hs x hx) f hx ?_ ?_ (hf x hx)

Premises used: ContinuousWithinAt.cfcₙ
-- 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 : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
refine_1 : ∀ (x : X) (hx : x ∈ t), ∀ᶠ (x_1 : X) in 𝓝[t] x, quasispectrum 𝕜 (a x_1) ⊆ s x
refine_2 : ∀ (x : X) (hx : x ∈ t), ∀ᶠ (x : X) in 𝓝[t] x, p (a x)
⊢ ∀ x ∈ t, ContinuousWithinAt.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) f (a x)) t x

Tactic:
refine fun x hx ↦ (ha_cont x hx).cfcₙ (hs x hx) f hx ?_ ?_ (hf x hx)

Premises used: ContinuousWithinAt.cfcₙ
-- 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 : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
x : X
hx : x ∈ t
h : ∀ (x_1 : X) (hx : quasispectrum 𝕜 (a x_1) ⊆ s x) (hxt : x_1 ∈ t), quasispectrum 𝕜 (a x_1) ⊆ s x
⊢ ∀ᶠ (x_1 : X) in 𝓝[t] x, quasispectrum 𝕜 (a x_1) ⊆ s x

Tactic:
filter_upwards [ha x hx, self_mem_nhdsWithin] with x hx hxt

Premises used: self_mem_nhdsWithin
-- 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 : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
x : X
hx : x ∈ t
h : ∀ (x_1 : X) (hx : quasispectrum 𝕜 (a x_1) ⊆ s x) (hxt : x_1 ∈ t), p (a x_1)
⊢ ∀ᶠ (x : X) in 𝓝[t] x, p (a x)

Tactic:
filter_upwards [ha x hx, self_mem_nhdsWithin] with x hx hxt

Premises used: self_mem_nhdsWithin
-- 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 : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
x_1 : X
hx_1 : x_1 ∈ t
x : X
hx : quasispectrum 𝕜 (a x) ⊆ s x_1
hxt : x ∈ t
⊢ quasispectrum 𝕜 (a x) ⊆ s x_1

Tactic:
hx
-- 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 : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
x_1 : X
hx_1 : x_1 ∈ t
x : X
hx : quasispectrum 𝕜 (a x) ⊆ s x_1
hxt : x ∈ t
⊢ p (a x)

Tactic:
ha' x hxt
-- 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 : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
x_1 : X
hx_1 : x_1 ∈ t
x : X
hx : quasispectrum 𝕜 (a x) ⊆ s x_1
hxt : x ∈ t
⊢ quasispectrum 𝕜 (a x) ⊆ s x_1

Tactic:
exacts [hx, ha' x hxt]
-- 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
f : 𝕜 → 𝕜
a : X → A
t : Set X
ha_cont : ContinuousOn a t
ha : ∀ x ∈ t, quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) f (a x)) t

Tactic:
ContinuousOn.cfcₙ _ (fun _ _ ↦ hs) ha_cont (fun _ _ ↦ ?_) ha'

Premises used: ContinuousOn.cfcₙ