awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
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 ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ 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 ℝ≥0 (a x_1) ⊆ s x
have h : ∀ (x_1 : X) (hx : quasispectrum ℝ≥0 (a x_1) ⊆ s x) (hxt : x_1 ∈ t), quasispectrum ℝ≥0 (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
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
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 ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
x : X
hx : x ∈ t
⊢ ∀ᶠ (x : X) in 𝓝[t] x, 0 ≤ a x
have h : ∀ (x_1 : X) (hx : quasispectrum ℝ≥0 (a x_1) ⊆ s x) (hxt : x_1 ∈ t), 0 ≤ 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
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : TopologicalSpace X
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
ha_cont : ContinuousOn a t
ha : ∀ x ∈ t, quasispectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ ContinuousOn.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (a x)) t
have refine : ∀ x ∈ t, ∀ᶠ (x : X) in 𝓝[t] x, quasispectrum ℝ≥0 (a x) ⊆ s
Tactic: refine ContinuousOn.cfcₙ_nnreal _ (fun _ _ ↦ hs) ha_cont (fun _ _ ↦ ?_) ha'
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (hypothesis)
Goal:
X : Type u_1
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : CompleteSpace A
inst_13 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, quasispectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, quasispectrum ℝ≥0 (a x))) s
⊢ ContinuousOn.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (a x)) t
have hs'₁ : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (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
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : CompleteSpace A
inst_13 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, quasispectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (a i))
x : (↑t : Type u_1)
⊢ ∃ (S : Set ℝ≥0), IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum ℝ≥0 x' ⊆ S) ∧ S ⊆ s
have obtain : ∀ (S : Set ℝ≥0) (hS₃ : id S ⊆ s) (hS₁ : S ∈ 𝓝ˢ (quasispectrum ℝ≥0 (a (↑x : X)))) (hS₂ : IsCompact S),
  ∃ (S : Set ℝ≥0), IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum ℝ≥0 x' ⊆ S) ∧ S ⊆ s
Tactic: obtain ⟨S, ⟨hS₁, hS₂⟩, hS₃⟩ :=
      quasispectrum.isCompact_nnreal (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
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : CompleteSpace A
inst_13 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, quasispectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (a i))
x : (↑t : Type u_1)
S : Set ℝ≥0
hS₃ : id S ⊆ s
hS₁ : S ∈ 𝓝ˢ (quasispectrum ℝ≥0 (a (↑x : X)))
hS₂ : IsCompact S
⊢ ∃ (S : Set ℝ≥0), IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum ℝ≥0 x' ⊆ S) ∧ S ⊆ s
have refine : ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum ℝ≥0 x' ⊆ S
Tactic: refine ⟨S, hS₂, ?_, hS₃⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (hypothesis)
Goal:
X : Type u_1
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : CompleteSpace A
inst_13 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, quasispectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (a i))
⊢ ContinuousOn.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (a x)) t
have this : ∀ (x : (↑t : Type u_1)),
  ∃ (S : Set ℝ≥0), IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum ℝ≥0 x' ⊆ S) ∧ S ⊆ s
Tactic: have (x : t) : ∃ S, IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a x), quasispectrum ℝ≥0 x' ⊆ S) ∧ S ⊆ s := by
    obtain ⟨S, ⟨hS₁, hS₂⟩, hS₃⟩ :=
      quasispectrum.isCompact_nnreal (a x) |>.nhdsSet_basis_isCompact.mem_iff.mp (hs' x x.2)
    refine ⟨S, hS₂, ?_, hS₃⟩
    exact upperHemicontinuous_quasispectrum_nnreal 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
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : CompleteSpace A
inst_13 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, quasispectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (a i))
this :
  ∀ (x : (↑t : Type u_1)),
    ∃ (S : Set ℝ≥0), IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum ℝ≥0 x' ⊆ S) ∧ S ⊆ s
⊢ ContinuousOn.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (a x)) t
have choose : ∀ (S : (x : (↑t : Type u_1)) → Set ℝ≥0) (hS₁ : ∀ (x : (↑t : Type u_1)), IsCompact (S x))
  (hS₂ : ∀ (x : (↑t : Type u_1)), ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum ℝ≥0 x' ⊆ S x)
  (hS₃ : ∀ (x : (↑t : Type u_1)), S x ⊆ s),
  ContinuousOn.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) 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
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : CompleteSpace A
inst_13 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, quasispectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (a i))
S : (x : (↑t : Type u_1)) → Set ℝ≥0
hS₁ : ∀ (x : (↑t : Type u_1)), IsCompact (S x)
hS₂ : ∀ (x : (↑t : Type u_1)), ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum ℝ≥0 x' ⊆ S x
hS₃ : ∀ (x : (↑t : Type u_1)), S x ⊆ s
⊢ ContinuousOn.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (a x)) t
have refine_1 : ∀ x₀ ∈ t,
  ∀ᶠ (x : X) in 𝓝[t] x₀,
    quasispectrum ℝ≥0 (a x) ⊆
      (fun (x : X) ↦ (if hx : x ∈ t then S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx) else ∅ : Set ℝ≥0)) x₀
Tactic: refine ha_cont.cfcₙ_nnreal (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
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : CompleteSpace A
inst_13 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, quasispectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (a i))
S : (x : (↑t : Type u_1)) → Set ℝ≥0
hS₁ : ∀ (x : (↑t : Type u_1)), IsCompact (S x)
hS₂ : ∀ (x : (↑t : Type u_1)), ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum ℝ≥0 x' ⊆ S x
hS₃ : ∀ (x : (↑t : Type u_1)), S x ⊆ s
refine_1 :
  ∀ x₀ ∈ t,
    ∀ᶠ (x : X) in 𝓝[t] x₀,
      quasispectrum ℝ≥0 (a x) ⊆
        (fun (x : X) ↦ (if hx : x ∈ t then S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx) else ∅ : Set ℝ≥0)) x₀
⊢ ContinuousOn.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) 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 ℝ≥0)) x)
Tactic: refine ha_cont.cfcₙ_nnreal (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
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : CompleteSpace A
inst_13 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, quasispectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (a i))
S : (x : (↑t : Type u_1)) → Set ℝ≥0
hS₁ : ∀ (x : (↑t : Type u_1)), IsCompact (S x)
hS₂ : ∀ (x : (↑t : Type u_1)), ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum ℝ≥0 x' ⊆ S x
hS₃ : ∀ (x : (↑t : Type u_1)), S x ⊆ s
⊢ ∀ x₀ ∈ t,
    ∀ᶠ (x : X) in 𝓝[t] x₀,
      quasispectrum ℝ≥0 (a x) ⊆
        (fun (x : X) ↦ (if hx : x ∈ t then S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx) else ∅ : Set ℝ≥0)) x₀
have refine_1 : ∀ (x₀ : X) (a_1 : x₀ ∈ t),
  ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum ℝ≥0 (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
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : CompleteSpace A
inst_13 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, quasispectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (a i))
S : (x : (↑t : Type u_1)) → Set ℝ≥0
hS₁ : ∀ (x : (↑t : Type u_1)), IsCompact (S x)
hS₂ : ∀ (x : (↑t : Type u_1)), ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum ℝ≥0 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 ℝ≥0)) 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
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : CompleteSpace A
inst_13 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, quasispectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (a i))
S : (x : (↑t : Type u_1)) → Set ℝ≥0
hS₁ : ∀ (x : (↑t : Type u_1)), IsCompact (S x)
hS₂ : ∀ (x : (↑t : Type u_1)), ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum ℝ≥0 x' ⊆ S x
hS₃ : ∀ (x : (↑t : Type u_1)), S x ⊆ s
⊢ ContinuousOn.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (a x)) t
have refine_1 : ∀ x₀ ∈ t,
  ∀ᶠ (x : X) in 𝓝[t] x₀,
    quasispectrum ℝ≥0 (a x) ⊆
      (fun (x : X) ↦ (if hx : x ∈ t then S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx) else ∅ : Set ℝ≥0)) x₀
Tactic: classical
  refine ha_cont.cfcₙ_nnreal (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
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : CompleteSpace A
inst_13 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, quasispectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (a i))
S : (x : (↑t : Type u_1)) → Set ℝ≥0
hS₁ : ∀ (x : (↑t : Type u_1)), IsCompact (S x)
hS₂ : ∀ (x : (↑t : Type u_1)), ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum ℝ≥0 x' ⊆ S x
hS₃ : ∀ (x : (↑t : Type u_1)), S x ⊆ s
refine_1 :
  ∀ x₀ ∈ t,
    ∀ᶠ (x : X) in 𝓝[t] x₀,
      quasispectrum ℝ≥0 (a x) ⊆
        (fun (x : X) ↦ (if hx : x ∈ t then S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx) else ∅ : Set ℝ≥0)) x₀
⊢ ContinuousOn.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) 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 ℝ≥0)) x)
Tactic: classical
  refine ha_cont.cfcₙ_nnreal (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
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : CompleteSpace A
inst_13 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, quasispectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (a i))
S : (x : (↑t : Type u_1)) → Set ℝ≥0
hS₁ : ∀ (x : (↑t : Type u_1)), IsCompact (S x)
hS₂ : ∀ (x : (↑t : Type u_1)), ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum ℝ≥0 x' ⊆ S x
hS₃ : ∀ (x : (↑t : Type u_1)), S x ⊆ s
refine_1 :
  ∀ x₀ ∈ t,
    ∀ᶠ (x : X) in 𝓝[t] x₀,
      quasispectrum ℝ≥0 (a x) ⊆
        (fun (x : X) ↦ (if hx : x ∈ t then S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx) else ∅ : Set ℝ≥0)) 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 ℝ≥0)) x)
⊢ ContinuousOn.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (a x)) t
have refine_1₁ : ∀ (x₀ : X) (a_1 : x₀ ∈ t),
  ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum ℝ≥0 (a x) ⊆ S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x₀ sorry)
Tactic: classical
  refine ha_cont.cfcₙ_nnreal (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
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : CompleteSpace A
inst_13 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, quasispectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (a i))
S : (x : (↑t : Type u_1)) → Set ℝ≥0
hS₁ : ∀ (x : (↑t : Type u_1)), IsCompact (S x)
hS₂ : ∀ (x : (↑t : Type u_1)), ∀ᶠ (x' : A) in 𝓝 (a (↑x : X)), quasispectrum ℝ≥0 x' ⊆ S x
hS₃ : ∀ (x : (↑t : Type u_1)), S x ⊆ s
refine_1 :
  ∀ x₀ ∈ t,
    ∀ᶠ (x : X) in 𝓝[t] x₀,
      quasispectrum ℝ≥0 (a x) ⊆
        (fun (x : X) ↦ (if hx : x ∈ t then S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx) else ∅ : Set ℝ≥0)) 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 ℝ≥0)) x)
refine_1₁ :
  ∀ (x₀ : X) (a_1 : x₀ ∈ t),
    ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum ℝ≥0 (a x) ⊆ S (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x₀ ⋯)
⊢ ContinuousOn.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) 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ₙ_nnreal (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
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
ha_cont : Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
hs : ∀ (x : X), IsCompact (s x)
ha : ∀ (x₀ : X), ∀ᶠ (x : X) in 𝓝 x₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
hf : ∀ (x : X), ContinuousOn f (s x)
hf0 : f 0 = 0
ha' : ∀ (x : X), 0 ≤ a x
⊢ Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (a x)
have rw : ∀ (ha_cont : ContinuousOn a Set.univ) (hs : ∀ (x : X), IsCompact (s x))
  (ha : ∀ (x₀ : X), ∀ᶠ (x : X) in 𝓝 x₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀) (hf : ∀ (x : X), ContinuousOn f (s x))
  (hf0 : f 0 = 0) (ha' : ∀ (x : X), 0 ≤ a x),
  ContinuousOn.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (a x)) Set.univ
Tactic: rw [← continuousOn_univ] at ha_cont ⊢
Cleared hypotheses: ha_cont, hs, ha, hf, hf0, ha'