awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : CompleteSpace A
inst_7 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, spectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (spectrum 𝕜 (a i))
this : ∀ (x : (↑t : Type u_1)), ∃ (S : Set 𝕜), IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), spectrum 𝕜 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)), spectrum 𝕜 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 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : CompleteSpace A
inst_7 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, spectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (spectrum 𝕜 (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)), spectrum 𝕜 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₀,
    spectrum 𝕜 (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 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : CompleteSpace A
inst_7 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, spectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (spectrum 𝕜 (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)), spectrum 𝕜 x' ⊆ S x
hS₃ : ∀ (x : (↑t : Type u_1)), S x ⊆ s
refine_1 :
  ∀ x₀ ∈ t,
    ∀ᶠ (x : X) in 𝓝[t] x₀,
      spectrum 𝕜 (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 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : CompleteSpace A
inst_7 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, spectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (spectrum 𝕜 (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)), spectrum 𝕜 x' ⊆ S x
hS₃ : ∀ (x : (↑t : Type u_1)), S x ⊆ s
⊢ ∀ x₀ ∈ t,
    ∀ᶠ (x : X) in 𝓝[t] x₀,
      spectrum 𝕜 (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₀, spectrum 𝕜 (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 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : CompleteSpace A
inst_7 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, spectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (spectrum 𝕜 (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)), spectrum 𝕜 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]
-- 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 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : CompleteSpace A
inst_7 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, spectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (spectrum 𝕜 (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)), spectrum 𝕜 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₀,
    spectrum 𝕜 (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: 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⟩
-- 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 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : CompleteSpace A
inst_7 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, spectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (spectrum 𝕜 (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)), spectrum 𝕜 x' ⊆ S x
hS₃ : ∀ (x : (↑t : Type u_1)), S x ⊆ s
refine_1 :
  ∀ x₀ ∈ t,
    ∀ᶠ (x : X) in 𝓝[t] x₀,
      spectrum 𝕜 (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: 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⟩
-- 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 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : CompleteSpace A
inst_7 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, spectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (spectrum 𝕜 (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)), spectrum 𝕜 x' ⊆ S x
hS₃ : ∀ (x : (↑t : Type u_1)), S x ⊆ s
refine_1 :
  ∀ x₀ ∈ t,
    ∀ᶠ (x : X) in 𝓝[t] x₀,
      spectrum 𝕜 (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
have refine_1₁ : ∀ (x₀ : X) (a_1 : x₀ ∈ t), ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum 𝕜 (a x) ⊆ S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x₀ sorry)
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⟩
-- 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 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : CompleteSpace A
inst_7 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ x ∈ t, spectrum 𝕜 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (spectrum 𝕜 (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)), spectrum 𝕜 x' ⊆ S x
hS₃ : ∀ (x : (↑t : Type u_1)), S x ⊆ s
refine_1 :
  ∀ x₀ ∈ t,
    ∀ᶠ (x : X) in 𝓝[t] x₀,
      spectrum 𝕜 (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₀, spectrum 𝕜 (a x) ⊆ 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
have refine_2₁ : ∀ (x : X) (a : x ∈ t), ContinuousOn f (S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x sorry))
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⟩
-- 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 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : TopologicalSpace X
s : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
ha_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
hs : ∀ (x : X), IsCompact (s x)
ha : ∀ (x₀ : X), ∀ᶠ (x : X) in 𝓝 x₀, spectrum 𝕜 (a x) ⊆ s x₀
hf : ∀ (x : X), ContinuousOn f (s x)
ha' : ∀ (x : X), p (a x)
⊢ Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦ cfc (p := p) f (a x)
have rw : ∀ (ha_cont : ContinuousOn a Set.univ) (hs : ∀ (x : X), IsCompact (s x))
  (ha : ∀ (x₀ : X), ∀ᶠ (x : X) in 𝓝 x₀, spectrum 𝕜 (a x) ⊆ s x₀) (hf : ∀ (x : X), ContinuousOn f (s x))
  (ha' : ∀ (x : X), p (a x)), ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfc (p := p) f (a x)) Set.univ
Tactic: rw [← continuousOn_univ] at ha_cont ⊢
Cleared hypotheses: ha_cont, hs, ha, hf, 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 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
a : X → A
ha_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
hf : ContinuousOn f s
ha' : ∀ (x : X), p (a x)
⊢ Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦ cfc (p := p) f (a x)
have rw : ∀ (ha_cont : ContinuousOn a Set.univ) (ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s) (hf : ContinuousOn f s)
  (ha' : ∀ (x : X), p (a x)), ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfc (p := p) f (a x)) Set.univ
Tactic: rw [← continuousOn_univ] at ha_cont ⊢
Cleared hypotheses: ha_cont, ha, hf, 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 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : CompleteSpace A
inst_7 : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
hs : Membership.mem (γ := Filter 𝕜) (𝓝ˢ (⋃ (x : X), spectrum 𝕜 (a x))) s
ha_cont : Continuous[inst_7, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha' : ∀ (x : X), p (a x)
hf : ContinuousOn f s
⊢ Continuous[inst_7, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦ cfc (p := p) f (a x)
have rw : ∀ (ha_cont : ContinuousOn a Set.univ) (ha' : ∀ (x : X), p (a x)) (hf : ContinuousOn f s),
  ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfc (p := p) f (a x)) Set.univ
Tactic: rw [← continuousOn_univ] at ha_cont ⊢
Cleared hypotheses: ha_cont, ha', hf
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (hypothesis)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
⊢ ContinuousOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
have this : Set.EqOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
  {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
Tactic: have : {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}.EqOn (cfc f) (cfc (fun x : ℝ ↦ f x.toNNReal)) :=
    fun a ha ↦ cfc_nnreal_eq_real _ _ ha.1
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
this :
  Set.EqOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
    {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
⊢ ContinuousOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
have refine : ContinuousOn (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
Tactic: refine ContinuousOn.congr ?_ this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
this :
  Set.EqOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
    {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (NNReal.toReal '' s)
have apply : Set.MapsTo Real.toNNReal (NNReal.toReal '' s) s
Tactic: apply hf.ofReal_map_toNNReal
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
this :
  Set.EqOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
    {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
⊢ Set.MapsTo Real.toNNReal (NNReal.toReal '' s) s
have rw : Set.MapsTo (Real.toNNReal ∘ NNReal.toReal) s s
Tactic: rw [Set.mapsTo_image_iff]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (hypothesis)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
this :
  Set.EqOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
    {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
⊢ ContinuousOn (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
have hf₁ : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (NNReal.toReal '' s)
Tactic: replace hf : ContinuousOn (fun x ↦ f x.toNNReal : ℝ → ℝ) (NNReal.toReal '' s) := by
    apply hf.ofReal_map_toNNReal
    rw [Set.mapsTo_image_iff]
    intro x hx
    simpa
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
this :
  Set.EqOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
    {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
hf : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (NNReal.toReal '' s)
⊢ ContinuousOn (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
have refine : ∀ (a : A) (ha : Membership.mem (γ := Set A) {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s} a),
  Membership.mem (γ := Set A) {a : A | IsSelfAdjoint a ∧ spectrum ℝ a ⊆ NNReal.toReal '' s} a
Tactic: refine continuousOn_cfc A (hs.image NNReal.continuous_coe) _ hf |>.mono fun a ha ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (hypothesis)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
this :
  Set.EqOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
    {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
hf : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (NNReal.toReal '' s)
a : A
ha : Membership.mem (γ := Set A) {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s} a
⊢ Membership.mem (γ := Set A) {a : A | IsSelfAdjoint a ∧ spectrum ℝ a ⊆ NNReal.toReal '' s} a
have ha₁ : (IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)) ∧
  spectrum ℝ≥0 a ⊆ s
Tactic: simp only [Set.mem_setOf_eq, nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts] at ha ⊢
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (hypothesis)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
this :
  Set.EqOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
    {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
hf : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (NNReal.toReal '' s)
a : A
ha :
  (IsSelfAdjoint a ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)) ∧
    spectrum ℝ≥0 a ⊆ s
⊢ IsSelfAdjoint a ∧ spectrum ℝ a ⊆ NNReal.toReal '' s
have ha₁ : (IsSelfAdjoint a ∧ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)) ∧
  spectrum ℝ≥0 a ⊆ s
Tactic: rw [← SpectrumRestricts] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_4 : ContinuousStar A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : T2Space A
inst_9 : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
this :
  Set.EqOn (cfc (p := fun (x : A) ↦ 0 ≤ x) f) (cfc (p := IsSelfAdjoint) fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ))
    {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
hf : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (NNReal.toReal '' s)
a : A
ha :
  (IsSelfAdjoint a ∧ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)) ∧
    spectrum ℝ≥0 a ⊆ s
⊢ IsSelfAdjoint a ∧ spectrum ℝ a ⊆ NNReal.toReal '' s
have refine : spectrum ℝ a ⊆ NNReal.toReal '' s
Tactic: refine ⟨ha.1.1, ?_⟩