awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : TopologicalSpace A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀
zero : Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) 0) b
smul :
  ∀ (r : 𝕜) (f : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀)
    (hf : Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b),
    Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) (r • f)) b
id :
  Commute
    ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A)
      (ContinuousMapZero.id (quasispectrum 𝕜 a) : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀))
    b
star_id :
  Commute
    ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A)
      (star (ContinuousMapZero.id (quasispectrum 𝕜 a)) : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀))
    b
add :
  ∀ (f g : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀)
    (hf : Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b)
    (hg : Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) g) b),
    Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) (f + g)) b
⊢ Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b
have mul : ∀ (f g : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀)
  (hf : Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b)
  (hg : Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) g) b),
  Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) (f * g)) b
Tactic: open scoped NonUnitalContinuousFunctionalCalculus in
  induction f using ContinuousMapZero.induction_on_of_compact with
  | zero => simp
  | smul r f hf => rw [map_smul]; exact hf.smul_left r
  | id => rwa [cfcₙHom_id ha]
  | star_id => rwa [map_star, cfcₙHom_id]
  | add f g hf hg => rw [map_add]; exact hf.add_left hg
  | mul f g hf hg => rw [map_mul]; exact mul_left hf hg
  | frequently f hf =>
    rw [commute_iff_eq, ← Set.mem_setOf (p := fun x => x * b = b * x),
      ← (isClosed_eq (by fun_prop) (by fun_prop)).closure_eq]
    apply mem_closure_of_frequently_of_tendsto hf
    exact cfcₙHom_continuous ha |>.tendsto _
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : TopologicalSpace A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀
zero : Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) 0) b
smul :
  ∀ (r : 𝕜) (f : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀)
    (hf : Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b),
    Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) (r • f)) b
id :
  Commute
    ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A)
      (ContinuousMapZero.id (quasispectrum 𝕜 a) : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀))
    b
star_id :
  Commute
    ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A)
      (star (ContinuousMapZero.id (quasispectrum 𝕜 a)) : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀))
    b
add :
  ∀ (f g : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀)
    (hf : Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b)
    (hg : Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) g) b),
    Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) (f + g)) b
mul :
  ∀ (f g : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀)
    (hf : Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b)
    (hg : Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) g) b),
    Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) (f * g)) b
⊢ Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b
have frequently : ∀ (f : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀)
  (hf :
    ∃ᶠ (g : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) in nhds f,
      Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) g) b),
  Commute ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f) b
Tactic: open scoped NonUnitalContinuousFunctionalCalculus in
  induction f using ContinuousMapZero.induction_on_of_compact with
  | zero => simp
  | smul r f hf => rw [map_smul]; exact hf.smul_left r
  | id => rwa [cfcₙHom_id ha]
  | star_id => rwa [map_star, cfcₙHom_id]
  | add f g hf hg => rw [map_add]; exact hf.add_left hg
  | mul f g hf hg => rw [map_mul]; exact mul_left hf hg
  | frequently f hf =>
    rw [commute_iff_eq, ← Set.mem_setOf (p := fun x => x * b = b * x),
      ← (isClosed_eq (by fun_prop) (by fun_prop)).closure_eq]
    apply mem_closure_of_frequently_of_tendsto hf
    exact cfcₙHom_continuous ha |>.tendsto _
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : IsTopologicalRing A
inst_8 : T2Space A
a b : A
hb : Commute a b
f : ℝ → ℝ
hf : ContinuousOn f (quasispectrum ℝ a)
hf0 :
  Eq (α := ℝ)
    (({ toFun := (quasispectrum ℝ a).restrict (π := fun (a : ℝ) ↦ ℝ) f, continuous_toFun := ⋯ :
            C((↑(quasispectrum ℝ a) : Type), ℝ) } :
          (a : (↑(quasispectrum ℝ a) : Type)) → ℝ)
        0 :
      ℝ)
    (0 : ℝ)
ha : IsSelfAdjoint a
⊢ (fun (x : A) ↦ Commute x b)
    ((cfcₙHom (p := IsSelfAdjoint) ha : (a : ContinuousMapZero (↑(quasispectrum ℝ a) : Type) ℝ) → A)
      { toFun := (quasispectrum ℝ a).restrict (π := fun (a : ℝ) ↦ ℝ) f, continuous_toFun := ⋯, map_zero' := hf0 :
        ContinuousMapZero (↑(quasispectrum ℝ a) : Type) ℝ })
have rw : (fun (x : A) ↦ Commute x b) (cfcₙ (p := IsSelfAdjoint) f a)
Tactic: rw [← cfcₙ_apply ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : IsTopologicalRing A
inst_8 : T2Space A
inst_9 : PartialOrder A
inst_10 : NonnegSpectrumClass ℝ A
inst_11 : StarOrderedRing A
a b : A
hb : Commute a b
f : ℝ≥0 → ℝ≥0
⊢ Commute (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a) b
have pos : ∀ (ha : 0 ≤ a), Commute (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a) b
Tactic: by_cases ha : 0 ≤ a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : IsTopologicalRing A
inst_8 : T2Space A
inst_9 : PartialOrder A
inst_10 : NonnegSpectrumClass ℝ A
inst_11 : StarOrderedRing A
a b : A
hb : Commute a b
f : ℝ≥0 → ℝ≥0
pos : ∀ (ha : 0 ≤ a), Commute (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a) b
⊢ Commute (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a) b
have neg : ∀ (ha : ¬0 ≤ a), Commute (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a) b
Tactic: by_cases ha : 0 ≤ a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : IsTopologicalRing A
inst_8 : T2Space A
inst_9 : PartialOrder A
inst_10 : NonnegSpectrumClass ℝ A
inst_11 : StarOrderedRing A
a b : A
hb : Commute a b
f : ℝ≥0 → ℝ≥0
ha : 0 ≤ a
⊢ Commute (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a) b
have pos : Commute (cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a) b
Tactic: rw [cfcₙ_nnreal_eq_real ..]
-- 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 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
⊢ Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))
have inl : ∀ (h_tendsto : TendstoUniformlyOn F f ⊥ (spectrum R a)) (hF : ∀ᶠ (x : X) in ⊥, ContinuousOn (F x) (spectrum R a)),
  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
-- 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 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
inl :
  ∀ (h_tendsto : TendstoUniformlyOn F f ⊥ (spectrum R a)) (hF : ∀ᶠ (x : X) in ⊥, ContinuousOn (F x) (spectrum R a)),
    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 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
⊢ Tendsto (fun (x : X) ↦ cfc (p := p) (F x) a) l (𝓝 (cfc (p := p) f a))
have hf : ContinuousOn f (spectrum R a)
Tactic: have hf := h_tendsto.continuousOn hF.frequently
-- 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 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
⊢ 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 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
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 (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 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (spectrum R a)}
⊢ 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 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (spectrum R a)}
| 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 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (spectrum R a)}
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 : ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_2), R)) → A)
    { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := sorry :
      C((↑(spectrum R a) : Type u_2), R) } :
  A)
Tactic: rw [Function.comp_apply, cfc_apply (hf := x.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 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (spectrum R a)}
| 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 }),
  ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_2), R)) → A)
      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := sorry :
        C((↑(spectrum R a) : Type u_2), R) } :
    A)
Tactic: enter [1, x]
      rw [Function.comp_apply, cfc_apply (hf := x.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 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (spectrum R a)}
⊢ 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 }) ↦
    (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_2), R)) → A)
      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := sorry :
        C((↑(spectrum R a) : Type u_2), R) })
  (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)]
-- 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 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (spectrum R a)}
⊢ Tendsto
    (fun (x : { x : X // x ∈ s }) ↦
      (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_2), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := ⋯ :
          C((↑(spectrum R a) : Type u_2), R) })
    (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 }) ↦
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_2), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := sorry :
          C((↑(spectrum R a) : Type u_2), R) } :
      A))
  (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l)
  (𝓝
      ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_2), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry :
          C((↑(spectrum R a) : Type u_2), R) }) :
    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 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (spectrum R a)}
⊢ Tendsto.{u_1, u_3} (β := A)
    (fun (x : { x : X // x ∈ s }) ↦
      ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_2), R)) → A)
          { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := ⋯ :
            C((↑(spectrum R a) : Type u_2), R) } :
        A))
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l)
    (𝓝
        ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_2), R)) → A)
          { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
            C((↑(spectrum R a) : Type u_2), R) }) :
      Filter A)
have pos : Tendsto
  (fun (x : { x : X // x ∈ s }) ↦
    { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := sorry })
  (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l)
  (𝓝
    { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry :
      C((↑(spectrum R a) : Type u_2), R) })
Tactic: apply cfcHom_continuous _ |>.tendsto _ |>.comp
-- 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 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (spectrum R a)}
⊢ Tendsto
    (fun (x : { x : X // x ∈ s }) ↦
      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := ⋯ })
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l)
    (𝓝
      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
        C((↑(spectrum R a) : Type u_2), R) })
have pos : TendstoUniformlyOn (fun (x : { x : X // x ∈ s }) ↦ F (↑x : X)) f (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l)
  (spectrum R a)
Tactic: rw [hf.tendsto_restrict_iff_tendstoUniformlyOn Subtype.property]