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 : 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
inst_10 : CompleteSpace A
inst_11 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ x ∈ t, spectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hs' : ∀ (i : X) (i_1 : i ∈ t), s ∈ 𝓝ˢ (spectrum ℝ≥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)), spectrum ℝ≥0 x' ⊆ S x
hS₃ : ∀ (x : (↑t : Type u_1)), S x ⊆ s
refine_1 :
  ∀ x₀ ∈ t,
    ∀ᶠ (x : X) in 𝓝[t] x₀,
      spectrum ℝ≥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₀, spectrum ℝ≥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 : 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
inst_10 : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
ha_cont : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
hs : ∀ (x : X), IsCompact (s x)
ha : ∀ (x₀ : X), ∀ᶠ (x : X) in 𝓝 x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
hf : ∀ (x : X), ContinuousOn f (s x)
ha' : ∀ (x : X), 0 ≤ a x
⊢ Continuous[inst_10, 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₀, spectrum ℝ≥0 (a x) ⊆ s x₀) (hf : ∀ (x : X), ContinuousOn f (s x))
  (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, ha'
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
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
inst_10 : TopologicalSpace X
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
ha_cont : Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum ℝ≥0 (a x) ⊆ s
hf : ContinuousOn f s
ha' : ∀ (x : X), 0 ≤ a x
⊢ Continuous[inst_10, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    cfc (p := fun (x : A) ↦ 0 ≤ x) f (a x)
have rw : ∀ (ha_cont : ContinuousOn a Set.univ) (ha : ∀ (x : X), spectrum ℝ≥0 (a x) ⊆ s) (hf : ContinuousOn f s)
  (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, ha, hf, ha'
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
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
inst_10 : CompleteSpace A
inst_11 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ (x : X), spectrum ℝ≥0 (a x))) s
ha_cont : Continuous[inst_11, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha' : ∀ (x : X), 0 ≤ a x
hf : ContinuousOn f s
⊢ Continuous[inst_11, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    cfc (p := fun (x : A) ↦ 0 ≤ x) f (a x)
have rw : ∀ (ha_cont : ContinuousOn a Set.univ) (ha' : ∀ (x : X), 0 ≤ a x) (hf : ContinuousOn f s),
  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, ha', hf
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (quasispectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (quasispectrum R a)
hF0 : ∀ᶠ (x : X) in l, F x 0 = 0
⊢ Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))
have inl : ∀ (h_tendsto : TendstoUniformlyOn F f ⊥ (quasispectrum R a))
  (hF : ∀ᶠ (x : X) in ⊥, ContinuousOn (F x) (quasispectrum R a)) (hF0 : ∀ᶠ (x : X) in ⊥, F x 0 = 0),
  Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) ⊥ (𝓝 (cfcₙ (p := p) f a))
Tactic: obtain (rfl | hl) := l.eq_or_neBot
Cleared hypotheses: l, h_tendsto, hF, hF0
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (quasispectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (quasispectrum R a)
hF0 : ∀ᶠ (x : X) in l, F x 0 = 0
inl :
  ∀ (h_tendsto : TendstoUniformlyOn F f ⊥ (quasispectrum R a))
    (hF : ∀ᶠ (x : X) in ⊥, ContinuousOn (F x) (quasispectrum R a)) (hF0 : ∀ᶠ (x : X) in ⊥, F x 0 = 0),
    Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) ⊥ (𝓝 (cfcₙ (p := p) f a))
⊢ Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))
have inr : ∀ (hl : l.NeBot), Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))
Tactic: obtain (rfl | hl) := l.eq_or_neBot
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (hypothesis)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (quasispectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (quasispectrum R a)
hF0 : ∀ᶠ (x : X) in l, F x 0 = 0
hl : l.NeBot
⊢ Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))
have hf : ContinuousOn f (quasispectrum R a)
Tactic: have hf := h_tendsto.continuousOn hF.frequently
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (hypothesis)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (quasispectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (quasispectrum R a)
hF0 : ∀ᶠ (x : X) in l, F x 0 = 0
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
⊢ Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))
have hf0 : f 0 = 0
Tactic: have hf0 : f 0 = 0 := Eq.symm <|
    tendsto_nhds_unique (tendsto_const_nhds.congr' <| .symm hF0) <|
    h_tendsto.tendsto_at (quasispectrum.zero_mem R a)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (quasispectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (quasispectrum R a)
hF0 : ∀ᶠ (x : X) in l, F x 0 = 0
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
hf0 : f 0 = 0
⊢ Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))
have pos : ∀ (ha : p a), Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))
Tactic: by_cases ha : p a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (quasispectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (quasispectrum R a)
hF0 : ∀ᶠ (x : X) in l, F x 0 = 0
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
hf0 : f 0 = 0
pos : ∀ (ha : p a), Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))
⊢ Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))
have neg : ∀ (ha : ¬p a), Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))
Tactic: by_cases ha : p a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (hypothesis)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (quasispectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (quasispectrum R a)
hF0 : ∀ᶠ (x : X) in l, F x 0 = 0
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
hf0 : f 0 = 0
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (quasispectrum R a) ∧ F x 0 = 0}
⊢ Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))
have hs : s ∈ l
Tactic: have hs : s ∈ l := hF.and hF0
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (quasispectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (quasispectrum R a)
hF0 : ∀ᶠ (x : X) in l, F x 0 = 0
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
hf0 : f 0 = 0
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (quasispectrum R a) ∧ F x 0 = 0}
hs : s ∈ l
⊢ Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))
have pos : Tendsto (α := { x : X // x ∈ s }) ((fun (x : X) ↦ cfcₙ (p := p) (F x) a) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ s))
  (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l) (𝓝 (cfcₙ (p := p) f a))
Tactic: rw [← tendsto_comap'_iff (i := ((↑) : s → X)) (by simpa)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (quasispectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (quasispectrum R a)
hF0 : ∀ᶠ (x : X) in l, F x 0 = 0
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
hf0 : f 0 = 0
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (quasispectrum R a) ∧ F x 0 = 0}
hs : s ∈ l
| Tendsto (α := { x : X // x ∈ s }) ((fun (x : X) ↦ cfcₙ (p := p) (F x) a) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ s))
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l) (𝓝 (cfcₙ (p := p) f a))
have h : ∀ (x : { x : X // x ∈ s }), (((fun (x : X) ↦ cfcₙ (p := p) (F x) a) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ s)) x : A)
Tactic: enter [1, x]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (quasispectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (quasispectrum R a)
hF0 : ∀ᶠ (x : X) in l, F x 0 = 0
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
hf0 : f 0 = 0
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (quasispectrum R a) ∧ F x 0 = 0}
hs : s ∈ l
x : { x : X // x ∈ s }
| (((fun (x : X) ↦ cfcₙ (p := p) (F x) a) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ s)) x : A)
have h : ((cfcₙHom (p := p) ha : (a : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R) → A)
    { toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := sorry,
      map_zero' := sorry } :
  A)
Tactic: rw [Function.comp_apply, cfcₙ_apply (hf := x.2.1) (hf0 := x.2.2)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (quasispectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (quasispectrum R a)
hF0 : ∀ᶠ (x : X) in l, F x 0 = 0
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
hf0 : f 0 = 0
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (quasispectrum R a) ∧ F x 0 = 0}
hs : s ∈ l
| Tendsto (α := { x : X // x ∈ s }) ((fun (x : X) ↦ cfcₙ (p := p) (F x) a) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ s))
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l) (𝓝 (cfcₙ (p := p) f a))
have h : ∀ (x : { x : X // x ∈ s }),
  ((cfcₙHom (p := p) ha : (a : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R) → A)
      { toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := sorry,
        map_zero' := sorry } :
    A)
Tactic: enter [1, x]
      rw [Function.comp_apply, cfcₙ_apply (hf := x.2.1) (hf0 := x.2.2)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (quasispectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (quasispectrum R a)
hF0 : ∀ᶠ (x : X) in l, F x 0 = 0
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
hf0 : f 0 = 0
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (quasispectrum R a) ∧ F x 0 = 0}
hs : s ∈ l
⊢ Tendsto (α := { x : X // x ∈ s }) ((fun (x : X) ↦ cfcₙ (p := p) (F x) a) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ s))
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l) (𝓝 (cfcₙ (p := p) f a))
have pos : Tendsto
  (fun (x : { x : X // x ∈ s }) ↦
    (cfcₙHom (p := p) ha : (a : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R) → A)
      { toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := sorry,
        map_zero' := sorry })
  (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l) (𝓝 (cfcₙ (p := p) f a))
Tactic: conv =>
      enter [1, x]
      rw [Function.comp_apply, cfcₙ_apply (hf := x.2.1) (hf0 := x.2.2)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (quasispectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (quasispectrum R a)
hF0 : ∀ᶠ (x : X) in l, F x 0 = 0
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
hf0 : f 0 = 0
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (quasispectrum R a) ∧ F x 0 = 0}
hs : s ∈ l
⊢ Tendsto
    (fun (x : { x : X // x ∈ s }) ↦
      (cfcₙHom (p := p) ha : (a : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R) → A)
        { toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := ⋯,
          map_zero' := ⋯ })
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l) (𝓝 (cfcₙ (p := p) f a))
have pos : Tendsto.{u_1, u_3} (β := A)
  (fun (x : { x : X // x ∈ s }) ↦
    ((cfcₙHom (p := p) ha : (a : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R) → A)
        { toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := sorry,
          map_zero' := sorry } :
      A))
  (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l)
  (𝓝
      ((cfcₙHom (p := p) ha : (a : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R) → A)
        { toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry, map_zero' := sorry }) :
    Filter A)
Tactic: rw [cfcₙ_apply ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (quasispectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (quasispectrum R a)
hF0 : ∀ᶠ (x : X) in l, F x 0 = 0
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
hf0 : f 0 = 0
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (quasispectrum R a) ∧ F x 0 = 0}
hs : s ∈ l
⊢ Tendsto.{u_1, u_3} (β := A)
    (fun (x : { x : X // x ∈ s }) ↦
      ((cfcₙHom (p := p) ha : (a : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R) → A)
          { toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := ⋯,
            map_zero' := ⋯ } :
        A))
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l)
    (𝓝
        ((cfcₙHom (p := p) ha : (a : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R) → A)
          { toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ }) :
      Filter A)
have pos : Tendsto (β := ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R)
  (fun (x : { x : X // x ∈ s }) ↦
    { toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := sorry,
      map_zero' := sorry })
  (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l)
  (𝓝 { toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry, map_zero' := sorry })
Tactic: apply cfcₙHom_continuous _ |>.tendsto _ |>.comp