awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
refine : ∀ x ∈ t, ∀ᶠ (x : X) in 𝓝[t] x, quasispectrum 𝕜 (a x) ⊆ s
⊢ ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) f (a x)) t

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

Premises used: ContinuousOn.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 : 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
x : X
h_1 : x ∈ t
h : ∀ (x : X) (hx : x ∈ t), quasispectrum 𝕜 (a x) ⊆ s
⊢ ∀ᶠ (x : X) in 𝓝[t] x, quasispectrum 𝕜 (a x) ⊆ s

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
𝕜 : 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
x_1 : X
h : x_1 ∈ t
x : X
hx : x ∈ t
⊢ quasispectrum 𝕜 (a x) ⊆ s

Tactic:
ha x 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 : 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
x_1 : X
h : x_1 ∈ t
x : X
hx : x ∈ t
⊢ quasispectrum 𝕜 (a x) ⊆ s

Tactic:
exact ha x 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 : CompleteSpace A
inst_9 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))) s

Tactic:
have hs' := 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 : CompleteSpace A
inst_9 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))) s
⊢ ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum 𝕜 (a i))

Tactic:
simp only [nhdsSet_iUnion, mem_iSup] at hs'

Premises used: nhdsSet_iUnion, Filter.mem_iSup
-- 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 : CompleteSpace A
inst_9 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum 𝕜 (a i))
x : (↑t : Type u_1)
obtain :
  ∀ (S : Set 𝕜) (hS₃ : id S ⊆ s) (hS₁ : S ∈ 𝓝ˢ (quasispectrum 𝕜 (a (↑x : X)))) (hS₂ : IsCompact S),
    ∃ (S : Set 𝕜), IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum 𝕜 x' ⊆ S) ∧ S ⊆ s
⊢ ∃ (S : Set 𝕜), IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum 𝕜 x' ⊆ S) ∧ S ⊆ s

Tactic:
obtain ⟨S, ⟨hS₁, hS₂⟩, hS₃⟩ :=
      quasispectrum.isCompact (𝕜 := 𝕜) (a x) |>.nhdsSet_basis_isCompact.mem_iff.mp (hs' x x.2)

Premises used: Filter.HasBasis.mem_iff, quasispectrum.isCompact, Iff.mp, Subtype.val, Subtype.property, IsCompact.nhdsSet_basis_isCompact
-- 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 : CompleteSpace A
inst_9 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum 𝕜 (a i))
x : (↑t : Type u_1)
S : Set 𝕜
hS₃ : id S ⊆ s
hS₁ : S ∈ 𝓝ˢ (quasispectrum 𝕜 (a (↑x : X)))
hS₂ : IsCompact S
⊢ ∃ (S : Set 𝕜), IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum 𝕜 x' ⊆ S) ∧ S ⊆ s

Tactic:
⟨S, hS₂, ?_, hS₃⟩

Premises used: And.intro, Exists.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
inst_8 : CompleteSpace A
inst_9 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum 𝕜 (a i))
x : (↑t : Type u_1)
S : Set 𝕜
hS₃ : id S ⊆ s
hS₁ : S ∈ 𝓝ˢ (quasispectrum 𝕜 (a (↑x : X)))
hS₂ : IsCompact S
refine : ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum 𝕜 x' ⊆ S
⊢ ∃ (S : Set 𝕜), IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum 𝕜 x' ⊆ S) ∧ S ⊆ s

Tactic:
refine ⟨S, hS₂, ?_, 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 : CompleteSpace A
inst_9 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum 𝕜 (a i))
x : (↑t : Type u_1)
S : Set 𝕜
hS₃ : id S ⊆ s
hS₁ : S ∈ 𝓝ˢ (quasispectrum 𝕜 (a (↑x : X)))
hS₂ : IsCompact S
⊢ ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum 𝕜 x' ⊆ S

Tactic:
upperHemicontinuous_quasispectrum 𝕜 A |>.upperHemicontinuousAt (a x) _ hS₁ |>.mono
      fun _ ↦ subset_of_mem_nhdsSet

Premises used: subset_of_mem_nhdsSet, upperHemicontinuous_quasispectrum, Filter.Eventually.mono, UpperHemicontinuous.upperHemicontinuousAt, Subtype.val
-- 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 : CompleteSpace A
inst_9 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum 𝕜 (a i))
x : (↑t : Type u_1)
S : Set 𝕜
hS₃ : id S ⊆ s
hS₁ : S ∈ 𝓝ˢ (quasispectrum 𝕜 (a (↑x : X)))
hS₂ : IsCompact S
⊢ ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum 𝕜 x' ⊆ S

Tactic:
exact upperHemicontinuous_quasispectrum 𝕜 A |>.upperHemicontinuousAt (a x) _ hS₁ |>.mono
      fun _ ↦ subset_of_mem_nhdsSet

Premises used: subset_of_mem_nhdsSet, upperHemicontinuous_quasispectrum, Filter.Eventually.mono, UpperHemicontinuous.upperHemicontinuousAt, Subtype.val
-- 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 : CompleteSpace A
inst_9 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum 𝕜 (a i))
⊢ ∀ (x : (↑t : Type u_1)), ∃ (S : Set 𝕜), IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum 𝕜 x' ⊆ S) ∧ S ⊆ s

Tactic:
have (x : t) : ∃ S, IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a x), quasispectrum 𝕜 x' ⊆ S) ∧ S ⊆ s := by
    obtain ⟨S, ⟨hS₁, hS₂⟩, hS₃⟩ :=
      quasispectrum.isCompact (𝕜 := 𝕜) (a x) |>.nhdsSet_basis_isCompact.mem_iff.mp (hs' x x.2)
    refine ⟨S, hS₂, ?_, hS₃⟩
    exact upperHemicontinuous_quasispectrum 𝕜 A |>.upperHemicontinuousAt (a x) _ hS₁ |>.mono
      fun _ ↦ subset_of_mem_nhdsSet
-- 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 : CompleteSpace A
inst_9 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum 𝕜 (a i))
this :
  ∀ (x : (↑t : Type u_1)), ∃ (S : Set 𝕜), IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum 𝕜 x' ⊆ S) ∧ S ⊆ s
choose :
  ∀ (S : (x : (↑t : Type u_1)) → Set 𝕜) (hS₁ : ∀ (x : (↑t : Type u_1)), IsCompact (S x))
    (hS₂ : ∀ (x : (↑t : Type u_1)), ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum 𝕜 x' ⊆ S x)
    (hS₃ : ∀ (x : (↑t : Type u_1)), S x ⊆ s), ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) f (a x)) t
⊢ ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) f (a x)) t

Tactic:
choose S hS₁ hS₂ hS₃ using this
-- 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 : CompleteSpace A
inst_9 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum 𝕜 (a i))
S : (x : (↑t : Type u_1)) → Set 𝕜
hS₁ : ∀ (x : (↑t : Type u_1)), IsCompact (S x)
hS₂ : ∀ (x : (↑t : Type u_1)), ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum 𝕜 x' ⊆ S x
hS₃ : ∀ (x : (↑t : Type u_1)), S x ⊆ s
⊢ ∀ x ∈ t,
    IsCompact.{u_2} (X := 𝕜)
      ((fun (x : X) ↦ (if hx : x ∈ t then S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx) else ∅ : Set 𝕜)) x)

Tactic:
simpa +contextual using 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 : CompleteSpace A
inst_9 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum 𝕜 (a i))
S : (x : (↑t : Type u_1)) → Set 𝕜
hS₁ : ∀ (x : (↑t : Type u_1)), IsCompact (S x)
hS₂ : ∀ (x : (↑t : Type u_1)), ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum 𝕜 x' ⊆ S x
hS₃ : ∀ (x : (↑t : Type u_1)), S x ⊆ s
refine_1 :
  ∀ x₀ ∈ t,
    ∀ᶠ (x : X) in 𝓝[t] x₀,
      quasispectrum 𝕜 (a x) ⊆
        (fun (x : X) ↦ (if hx : x ∈ t then S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx) else ∅ : Set 𝕜)) x₀
refine_2 :
  ∀ x ∈ t,
    ContinuousOn f
      ((fun (x : X) ↦ (if hx : x ∈ t then S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx) else ∅ : Set 𝕜)) x)
⊢ ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) f (a x)) t

Tactic:
refine ha_cont.cfcₙ (s := fun x : X ↦ if hx : x ∈ t then S ⟨x, hx⟩ else ∅) f
    (by simpa +contextual using hS₁) ?_ ha' ?_

Premises used: ContinuousOn.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 : CompleteSpace A
inst_9 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum 𝕜 (a i))
S : (x : (↑t : Type u_1)) → Set 𝕜
hS₁ : ∀ (x : (↑t : Type u_1)), IsCompact (S x)
hS₂ : ∀ (x : (↑t : Type u_1)), ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum 𝕜 x' ⊆ S x
hS₃ : ∀ (x : (↑t : Type u_1)), S x ⊆ s
refine_1 :
  ∀ (x₀ : X) (a_1 : x₀ ∈ t),
    ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x₀ ⋯)
⊢ ∀ x₀ ∈ t,
    ∀ᶠ (x : X) in 𝓝[t] x₀,
      quasispectrum 𝕜 (a x) ⊆
        (fun (x : X) ↦ (if hx : x ∈ t then S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx) else ∅ : Set 𝕜)) x₀

Tactic:
simp +contextual only [↓reduceDIte]

Premises used: reduceDIte
-- 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 : CompleteSpace A
inst_9 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum 𝕜 (a i))
S : (x : (↑t : Type u_1)) → Set 𝕜
hS₁ : ∀ (x : (↑t : Type u_1)), IsCompact (S x)
hS₂ : ∀ (x : (↑t : Type u_1)), ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum 𝕜 x' ⊆ S x
hS₃ : ∀ (x : (↑t : Type u_1)), S x ⊆ s
refine_2 : ∀ (x : X) (a : x ∈ t), ContinuousOn f (S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x ⋯))
⊢ ∀ x ∈ t,
    ContinuousOn f
      ((fun (x : X) ↦ (if hx : x ∈ t then S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx) else ∅ : Set 𝕜)) x)

Tactic:
simp +contextual only [↓reduceDIte]

Premises used: reduceDIte
-- 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 : CompleteSpace A
inst_9 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum 𝕜 (a i))
S : (x : (↑t : Type u_1)) → Set 𝕜
hS₁ : ∀ (x : (↑t : Type u_1)), IsCompact (S x)
hS₂ : ∀ (x : (↑t : Type u_1)), ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum 𝕜 x' ⊆ S x
hS₃ : ∀ (x : (↑t : Type u_1)), S x ⊆ s
⊢ ∀ (x₀ : X) (a_1 : x₀ ∈ t),
    ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x₀ ⋯)

Tactic:
fun x₀ hx₀ ↦ ha_cont.continuousWithinAt hx₀ |>.eventually <| hS₂ ⟨x₀, hx₀⟩

Premises used: Subtype.mk, Filter.Tendsto.eventually, 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
inst_8 : CompleteSpace A
inst_9 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum 𝕜 (a i))
S : (x : (↑t : Type u_1)) → Set 𝕜
hS₁ : ∀ (x : (↑t : Type u_1)), IsCompact (S x)
hS₂ : ∀ (x : (↑t : Type u_1)), ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum 𝕜 x' ⊆ S x
hS₃ : ∀ (x : (↑t : Type u_1)), S x ⊆ s
⊢ ∀ (x₀ : X) (a_1 : x₀ ∈ t),
    ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x₀ ⋯)

Tactic:
exact fun x₀ hx₀ ↦ ha_cont.continuousWithinAt hx₀ |>.eventually <| hS₂ ⟨x₀, hx₀⟩

Premises used: Subtype.mk, Filter.Tendsto.eventually, 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
inst_8 : CompleteSpace A
inst_9 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum 𝕜 (a i))
S : (x : (↑t : Type u_1)) → Set 𝕜
hS₁ : ∀ (x : (↑t : Type u_1)), IsCompact (S x)
hS₂ : ∀ (x : (↑t : Type u_1)), ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum 𝕜 x' ⊆ S x
hS₃ : ∀ (x : (↑t : Type u_1)), S x ⊆ s
⊢ ∀ (x : X) (a : x ∈ t), ContinuousOn f (S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x ⋯))

Tactic:
fun x hx ↦ hf.mono <| hS₃ ⟨x, hx⟩

Premises used: Subtype.mk, ContinuousOn.mono
-- 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 : CompleteSpace A
inst_9 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum 𝕜 (a i))
S : (x : (↑t : Type u_1)) → Set 𝕜
hS₁ : ∀ (x : (↑t : Type u_1)), IsCompact (S x)
hS₂ : ∀ (x : (↑t : Type u_1)), ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum 𝕜 x' ⊆ S x
hS₃ : ∀ (x : (↑t : Type u_1)), S x ⊆ s
⊢ ∀ (x : X) (a : x ∈ t), ContinuousOn f (S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x ⋯))

Tactic:
exact fun x hx ↦ hf.mono <| hS₃ ⟨x, hx⟩

Premises used: Subtype.mk, ContinuousOn.mono
-- 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 : CompleteSpace A
inst_9 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum 𝕜 (a i))
S : (x : (↑t : Type u_1)) → Set 𝕜
hS₁ : ∀ (x : (↑t : Type u_1)), IsCompact (S x)
hS₂ : ∀ (x : (↑t : Type u_1)), ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum 𝕜 x' ⊆ S x
hS₃ : ∀ (x : (↑t : Type u_1)), S x ⊆ s
refine_1 :
  ∀ x₀ ∈ t,
    ∀ᶠ (x : X) in 𝓝[t] x₀,
      quasispectrum 𝕜 (a x) ⊆
        (fun (x : X) ↦ (if hx : x ∈ t then S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx) else ∅ : Set 𝕜)) x₀
refine_2 :
  ∀ x ∈ t,
    ContinuousOn f
      ((fun (x : X) ↦ (if hx : x ∈ t then S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx) else ∅ : Set 𝕜)) x)
refine_1₁ :
  ∀ (x₀ : X) (a_1 : x₀ ∈ t),
    ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x₀ ⋯)
refine_2₁ refine_2₂ : ∀ (x : X) (a : x ∈ t), ContinuousOn f (S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x ⋯))
⊢ ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) f (a x)) t

Tactic:
classical
  refine ha_cont.cfcₙ (s := fun x : X ↦ if hx : x ∈ t then S ⟨x, hx⟩ else ∅) f
    (by simpa +contextual using hS₁) ?_ ha' ?_
  all_goals simp +contextual only [↓reduceDIte]
  · exact fun x₀ hx₀ ↦ ha_cont.continuousWithinAt hx₀ |>.eventually <| hS₂ ⟨x₀, hx₀⟩
  · exact fun x hx ↦ hf.mono <| hS₃ ⟨x, hx⟩

Premises used: reduceDIte, Subtype.mk, Filter.Tendsto.eventually, ContinuousOn.mono, ContinuousOn.continuousWithinAt