awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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
pos : ∀ (hs0 : 0 ∈ s), ContinuousOn (Y := A) (fun (x : A) ↦ cfcₙ (p := p) f x) {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}
have neg : ∀ (hs0 : 0 ∉ s), ContinuousOn (Y := A) (fun (x : A) ↦ cfcₙ (p := p) f x) {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s}
Tactic: by_cases hs0 : 0 ∈ s
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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) {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s}
have pos : Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  (Set.restrict (π := fun (a : A) ↦ A) {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s} fun (x : A) ↦ cfcₙ (p := p) f x)
Tactic: rw [continuousOn_iff_continuous_restrict]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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
⊢ Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (Set.restrict (π := fun (a : A) ↦ A) {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s} fun (x : A) ↦ cfcₙ (p := p) f x)
have h : ∀ (x : (↑{a : A | p a ∧ quasispectrum 𝕜 a ⊆ s} : Type u_3)),
  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) sorry (s := s) sorry : ContinuousMapZero (↑s : Type u_2) 𝕜 →⋆ₙₐ[𝕜] A) :
          (a : ContinuousMapZero (↑s : Type u_2) 𝕜) → A)
        { toFun := s.restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := sorry, map_zero' := hf0 } :
      A)
Tactic: convert!
      continuous_cfcₙHomSuperset_left hs (hs0 := ⟨hs0⟩) ⟨⟨_, hf.restrict⟩, hf0⟩ (X :=
        {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s}) continuous_subtype_val (fun x ↦ x.2.2) with
      x
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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 (α := 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)
have h : Eq.{u_3 + 1} (α := A)
  ((cfcₙHom (p := p) sorry : (a : ContinuousMapZero (↑(quasispectrum 𝕜 (↑x : A)) : Type u_2) 𝕜) → A)
      { toFun := (quasispectrum 𝕜 (↑x : A)).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := sorry,
        map_zero' := hf0 } :
    A)
  ((cfcₙHom (p := p) sorry : (a : ContinuousMapZero (↑(quasispectrum 𝕜 (↑x : A)) : Type u_2) 𝕜) → A)
      (ContinuousMapZero.comp { toFun := s.restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := sorry, map_zero' := hf0 }
        { toFun := Subtype.map (p := Membership.mem (quasispectrum 𝕜 (↑x : A))) (q := Membership.mem s) id sorry,
          continuous_toFun := sorry, map_zero' := sorry }) :
    A)
Tactic: rw [cfcₙHomSuperset_apply, Set.restrict_apply, cfcₙ_apply _ _ (hf.mono x.2.2) hf0 x.2.1]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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) {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s}
have h : Eq.{u_3 + 1} (α := Set A) {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s} ∅
Tactic: convert! continuousOn_empty _
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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
⊢ Eq.{u_3 + 1} (α := Set A) {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s} ∅
have h : ∀ (x : A), x ∉ {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s}
Tactic: rw [Set.eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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 (fun (x : X) ↦ cfcₙ (p := p) f (a x)) l (𝓝 (cfcₙ (p := p) f a₀))
have apply : Tendsto a l (𝓝[{a : A | p a ∧ quasispectrum 𝕜 a ⊆ s}] a₀)
Tactic: apply continuousOn_cfcₙ A hs f |>.continuousWithinAt ⟨ha₀', ha₀⟩ |>.tendsto.comp
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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 : A | p a ∧ quasispectrum 𝕜 a ⊆ s}] a₀)
have rw : Tendsto a l (𝓝 a₀) ∧ ∀ᶠ (n : X) in l, Membership.mem (γ := Set A) {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s} (a n)
Tactic: rw [tendsto_nhdsWithin_iff]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (hypothesis)
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
⊢ ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) f (a x)) t
have ha_cont₁ : ∀ x ∈ t, ContinuousWithinAt a t x
Tactic: rw [ContinuousOn] at ha_cont ⊢
Cleared hypotheses: ha_cont, ha, ha', hf, hf0
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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
⊢ ∀ x ∈ t, ContinuousWithinAt.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) f (a x)) t x
have refine_2 : ∀ (x : X) (hx : x ∈ t), ∀ᶠ (x : X) in 𝓝[t] x, p (a x)
Tactic: refine fun x hx ↦ (ha_cont x hx).cfcₙ (hs x hx) f hx ?_ ?_ (hf x hx)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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
⊢ ∀ᶠ (x_1 : X) in 𝓝[t] x, quasispectrum 𝕜 (a x_1) ⊆ s x
have h : ∀ (x_1 : X) (hx : quasispectrum 𝕜 (a x_1) ⊆ s x) (hxt : x_1 ∈ t), quasispectrum 𝕜 (a x_1) ⊆ s x
Tactic: filter_upwards [ha x hx, self_mem_nhdsWithin] with x hx hxt
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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
⊢ ∀ᶠ (x : X) in 𝓝[t] x, p (a x)
have h : ∀ (x_1 : X) (hx : quasispectrum 𝕜 (a x_1) ⊆ s x) (hxt : x_1 ∈ t), p (a x_1)
Tactic: filter_upwards [ha x hx, self_mem_nhdsWithin] with x hx hxt
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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
have refine : ∀ x ∈ t, ∀ᶠ (x : X) in 𝓝[t] x, quasispectrum 𝕜 (a x) ⊆ s
Tactic: refine ContinuousOn.cfcₙ _ (fun _ _ ↦ hs) ha_cont (fun _ _ ↦ ?_) ha'
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (hypothesis)
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
⊢ ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) f (a x)) t
have hs'₁ : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum 𝕜 (a i))
Tactic: simp only [nhdsSet_iUnion, mem_iSup] at hs'
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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
have 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
Tactic: obtain ⟨S, ⟨hS₁, hS₂⟩, hS₃⟩ :=
      quasispectrum.isCompact (𝕜 := 𝕜) (a x) |>.nhdsSet_basis_isCompact.mem_iff.mp (hs' x x.2)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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
have refine : ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum 𝕜 x' ⊆ S
Tactic: refine ⟨S, hS₂, ?_, hS₃⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (hypothesis)
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))
⊢ ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) f (a x)) t
have this : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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
⊢ ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) f (a x)) t
have 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
Tactic: choose S hS₁ hS₂ hS₃ using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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
⊢ ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) f (a x)) t
have 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₀
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' ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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₀
⊢ ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) f (a x)) t
have 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)
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' ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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,
    ∀ᶠ (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₀
have 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₀ sorry)
Tactic: simp +contextual only [↓reduceDIte]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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,
    ContinuousOn f
      ((fun (x : X) ↦ (if hx : x ∈ t then S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx) else ∅ : Set 𝕜)) x)
have refine_2 : ∀ (x : X) (a : x ∈ t), ContinuousOn f (S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x sorry))
Tactic: simp +contextual only [↓reduceDIte]