ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>r : R<GOAL>p ((algebraMap R A) r)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<GOAL>p 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>hfg : Set.EqOn f g (spectrum R a)<GOAL>cfc f a = cfc g a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>h : cfc f a = cfc g a<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<VAR>hg : ContinuousOn g (spectrum R a) := by cfc_cont_tac<VAR>ha : p a := by cfc_tac<GOAL>Set.EqOn f g (spectrum R a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>ha : p a := by cfc_tac<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<VAR>hg : ContinuousOn g (spectrum R a) := by cfc_cont_tac<GOAL>cfc f a = cfc g a ↔ Set.EqOn f g (spectrum R a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a := by cfc_tac<GOAL>cfc 1 a = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a := by cfc_tac<GOAL>cfc (fun x => 1) a = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>a : A<GOAL>cfc 0 a = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>a : A<GOAL>cfc (fun x => 0) a = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<VAR>hg : ContinuousOn g (spectrum R a) := by cfc_cont_tac<GOAL>cfc (fun x => f x * g x) a = cfc f a * cfc g a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>n : ℕ<VAR>a : A<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<VAR>ha : p a := by cfc_tac<GOAL>cfc (fun x => f x ^ n) a = cfc f a ^ n
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>a : A<VAR>f g : R → R<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<VAR>hg : ContinuousOn g (spectrum R a) := by cfc_cont_tac<GOAL>cfc (fun x => f x + g x) a = cfc f a + cfc g a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>r : R<VAR>f : R → R<VAR>a : A<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<VAR>ha : p a := by cfc_tac<GOAL>cfc (fun x => r + f x) a = (algebraMap R A) r + cfc f a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>r : R<VAR>f : R → R<VAR>a : A<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<VAR>ha : p a := by cfc_tac<GOAL>cfc (fun x => f x + r) a = cfc f a + (algebraMap R A) r
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>ι : Type u_3<VAR>f : ι → R → R<VAR>a : A<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a) := by cfc_cont_tac<GOAL>cfc (∑ i ∈ s, f i) a = ∑ i ∈ s, cfc (f i) a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>ι : Type u_3<VAR>Fintype ι<VAR>f : ι → R → R<VAR>a : A<VAR>hf : ∀ (i : ι), ContinuousOn (f i) (spectrum R a) := by cfc_cont_tac<GOAL>cfc (∑ i : ι, f i) a = ∑ i : ι, cfc (f i) a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>S : Type u_3<VAR>SMul S R<VAR>ContinuousConstSMul S R<VAR>SMulZeroClass S A<VAR>IsScalarTower S R A<VAR>IsScalarTower S R (R → R)<VAR>s : S<VAR>f : R → R<VAR>a : A<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<GOAL>cfc (fun x => s • f x) a = s • cfc f a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>r : R<VAR>f : R → R<VAR>a : A<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<GOAL>cfc (fun x => r * f x) a = r • cfc f a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<GOAL>cfc (fun x => star (f x)) a = star (cfc f a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>a : A<VAR>n : ℕ<VAR>ha : p a := by cfc_tac<GOAL>cfc (fun x => x ^ n) a = a ^ n
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>S : Type u_3<VAR>SMul S R<VAR>ContinuousConstSMul S R<VAR>SMulZeroClass S A<VAR>IsScalarTower S R A<VAR>IsScalarTower S R (R → R)<VAR>s : S<VAR>a : A<VAR>ha : p a := by cfc_tac<GOAL>cfc (fun x => s • x) a = s • a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>r : R<VAR>a : A<VAR>ha : p a := by cfc_tac<GOAL>cfc (fun x => r * x) a = r • a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a := by cfc_tac<GOAL>cfc (fun x => star x) a = star a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a := by cfc_tac<GOAL>cfc (fun a => Polynomial.eval a Polynomial.X) a = a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>r : R<VAR>a : A<VAR>ha : p a := by cfc_tac<GOAL>cfc (fun a => Polynomial.eval a (Polynomial.C r)) a = (algebraMap R A) r
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>q : Polynomial R<VAR>f : R → R<VAR>a : A<VAR>ha : p a := by cfc_tac<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<GOAL>cfc (fun x => Polynomial.eval (f x) q) a = (Polynomial.aeval (cfc f a)) q
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>q : Polynomial R<VAR>a : A<VAR>ha : p a := by cfc_tac<GOAL>cfc (fun a => Polynomial.eval a q) a = (Polynomial.aeval a) q
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>UniqueContinuousFunctionalCalculus R A<VAR>g f : R → R<VAR>a : A<VAR>ha : p a := by cfc_tac<VAR>hg : ContinuousOn g (f '' spectrum R a) := by cfc_cont_tac<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<GOAL>cfc (g ∘ f) a = cfc g (cfc f a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>UniqueContinuousFunctionalCalculus R A<VAR>g f : R → R<VAR>a : A<VAR>hg : ContinuousOn g (f '' spectrum R a) := by cfc_cont_tac<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<VAR>ha : p a := by cfc_tac<GOAL>cfc (fun x => g (f x)) a = cfc g (cfc f a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>UniqueContinuousFunctionalCalculus R A<VAR>f : R → R<VAR>n : ℕ<VAR>a : A<VAR>hf : ContinuousOn f ((fun x => x ^ n) '' spectrum R a) := by cfc_cont_tac<VAR>ha : p a := by cfc_tac<GOAL>cfc (fun x => f (x ^ n)) a = cfc f (a ^ n)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>UniqueContinuousFunctionalCalculus R A<VAR>S : Type u_3<VAR>SMul S R<VAR>ContinuousConstSMul S R<VAR>SMulZeroClass S A<VAR>IsScalarTower S R A<VAR>IsScalarTower S R (R → R)<VAR>s : S<VAR>f : R → R<VAR>a : A<VAR>hf : ContinuousOn f ((fun x => s • x) '' spectrum R a) := by cfc_cont_tac<VAR>ha : p a := by cfc_tac<GOAL>cfc (fun x => f (s • x)) a = cfc f (s • a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>UniqueContinuousFunctionalCalculus R A<VAR>r : R<VAR>f : R → R<VAR>a : A<VAR>hf : ContinuousOn f ((fun x => r * x) '' spectrum R a) := by cfc_cont_tac<VAR>ha : p a := by cfc_tac<GOAL>cfc (fun x => f (r * x)) a = cfc f (r • a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>UniqueContinuousFunctionalCalculus R A<VAR>f : R → R<VAR>a : A<VAR>hf : ContinuousOn f (star '' spectrum R a) := by cfc_cont_tac<VAR>ha : p a := by cfc_tac<GOAL>cfc (fun x => f (star x)) a = cfc f (star a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>UniqueContinuousFunctionalCalculus R A<VAR>q : Polynomial R<VAR>f : R → R<VAR>a : A<VAR>hf : ContinuousOn f ((fun a => Polynomial.eval a q) '' spectrum R a) := by cfc_cont_tac<VAR>ha : p a := by cfc_tac<GOAL>cfc (fun x => f (Polynomial.eval x q)) a = cfc f ((Polynomial.aeval a) q)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>a : A<VAR>r : R<VAR>h_spec : spectrum R a ⊆ {r}<VAR>ha : p a := by cfc_tac<GOAL>a = (algebraMap R A) r
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>a : A<VAR>h_spec : spectrum R a ⊆ {0}<VAR>ha : p a := by cfc_tac<GOAL>a = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>a : A<VAR>h_spec : spectrum R a ⊆ {1}<VAR>ha : p a := by cfc_tac<GOAL>a = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>r : R<GOAL>spectrum R ((algebraMap R A) r) ⊆ {r}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>Nontrivial A<VAR>r : R<GOAL>spectrum R ((algebraMap R A) r) = {r}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>Nontrivial A<GOAL>spectrum R 0 = {0}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>Nontrivial A<GOAL>spectrum R 1 = {1}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>r : R<VAR>f : R → R<GOAL>cfc f ((algebraMap R A) r) = (algebraMap R A) (f r)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f : R → R<GOAL>cfc f 0 = (algebraMap R A) (f 0)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f : R → R<GOAL>cfc f 1 = (algebraMap R A) (f 1)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>Semifield R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<VAR>ha : p a := by cfc_tac<GOAL>IsUnit (cfc f a) ↔ ∀ x ∈ spectrum R a, f x ≠ 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>Semifield R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>HasContinuousInv₀ R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>hf' : ∀ x ∈ spectrum R a, f x ≠ 0<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<VAR>ha : p a := by cfc_tac<GOAL>↑(cfcUnits f a hf' hf ha) = cfc f a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>Semifield R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>HasContinuousInv₀ R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>hf' : ∀ x ∈ spectrum R a, f x ≠ 0<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<VAR>ha : p a := by cfc_tac<GOAL>↑(cfcUnits f a hf' hf ha)⁻¹ = cfc (fun x => (f x)⁻¹) a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>Semifield R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>HasContinuousInv₀ R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>hf' : ∀ x ∈ spectrum R a, f x ≠ 0<VAR>n : ℕ<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<VAR>ha : p a := by cfc_tac<GOAL>cfcUnits f a hf' hf ha ^ n = cfcUnits (fun x => f x ^ n) a ⋯ ⋯ ha
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>Semifield R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>HasContinuousInv₀ R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>hf' : ∀ x ∈ spectrum R a, f x ≠ 0<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<VAR>ha : p a := by cfc_tac<GOAL>cfc (fun x => (f x)⁻¹) a = Ring.inverse (cfc f a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>Semifield R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>HasContinuousInv₀ R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>a : Aˣ<VAR>ha : p ↑a := by cfc_tac<GOAL>cfc (fun x => x⁻¹) ↑a = ↑a⁻¹
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>Semifield R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>HasContinuousInv₀ R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>hg' : ∀ x ∈ spectrum R a, g x ≠ 0<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<VAR>hg : ContinuousOn g (spectrum R a) := by cfc_cont_tac<VAR>ha : p a := by cfc_tac<GOAL>cfc (fun x => f x / g x) a = cfc f a * Ring.inverse (cfc g a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semifield R<VAR>MetricSpace R<VAR>HasContinuousInv₀ R<VAR>Ring A<VAR>Algebra R A<VAR>a : Aˣ<GOAL>ContinuousOn (fun x => x⁻¹) (spectrum R ↑a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semifield R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>HasContinuousInv₀ R<VAR>Ring A<VAR>Algebra R A<VAR>a : Aˣ<VAR>n : ℤ<GOAL>ContinuousOn (fun x => x ^ n) (spectrum R ↑a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>Semifield R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>HasContinuousInv₀ R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>UniqueContinuousFunctionalCalculus R A<VAR>f : R → R<VAR>a : Aˣ<VAR>hf : ContinuousOn f ((fun x => x⁻¹) '' spectrum R ↑a) := by cfc_cont_tac<VAR>ha : p ↑a := by cfc_tac<GOAL>cfc (fun x => f x⁻¹) ↑a = cfc f ↑a⁻¹
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>Semifield R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>HasContinuousInv₀ R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>hf' : ∀ x ∈ spectrum R a, f x ≠ 0<VAR>n : ℤ<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<VAR>ha : p a := by cfc_tac<GOAL>cfcUnits f a hf' hf ha ^ n = cfcUnits (f ^ n) a ⋯ ⋯ ha
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>Semifield R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>HasContinuousInv₀ R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>a : Aˣ<VAR>n : ℤ<VAR>ha : p ↑a := by cfc_tac<GOAL>cfc (fun x => x ^ n) ↑a = ↑(a ^ n)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>Semifield R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>HasContinuousInv₀ R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>UniqueContinuousFunctionalCalculus R A<VAR>f : R → R<VAR>n : ℤ<VAR>a : Aˣ<VAR>hf : ContinuousOn f ((fun x => x ^ n) '' spectrum R ↑a) := by cfc_cont_tac<VAR>ha : p ↑a := by cfc_tac<GOAL>cfc (fun x => f (x ^ n)) ↑a = cfc f ↑(a ^ n)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommRing R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalRing R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<VAR>hg : ContinuousOn g (spectrum R a) := by cfc_cont_tac<GOAL>cfc (fun x => f x - g x) a = cfc f a - cfc g a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommRing R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalRing R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<GOAL>cfc (fun x => -f x) a = -cfc f a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommRing R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalRing R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a := by cfc_tac<GOAL>cfc (fun x => -x) a = -a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>CommRing R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalRing R<VAR>ContinuousStar R<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>UniqueContinuousFunctionalCalculus R A<VAR>hf : ContinuousOn f ((fun x => -x) '' spectrum R a) := by cfc_cont_tac<VAR>ha : p a := by cfc_tac<GOAL>cfc (fun x => f (-x)) a = cfc f (-a)