chore: backports for leanprover/lean4#4814 (part 38) (#15618)

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean

@@ -99,7 +99,7 @@ section Main
 variable {R A : Type*} {p : A → Prop} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R]
 variable [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A]
 variable [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A]
-variable [NonUnitalContinuousFunctionalCalculus R p]
+variable [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p]
 
 lemma NonUnitalStarAlgHom.ext_continuousMap [UniqueNonUnitalContinuousFunctionalCalculus R A]
     (a : A) (φ ψ : C(σₙ R a, R)₀ →⋆ₙₐ[R] A) (hφ : Continuous φ) (hψ : Continuous ψ)
@@ -383,6 +383,8 @@ lemma cfcₙ_const_mul_id (r : R) (a : A) (ha : p a := by cfc_tac) : cfcₙ (r *
 lemma cfcₙ_star_id : cfcₙ (star · : R → R) a = star a := by
   rw [cfcₙ_star _ a, cfcₙ_id' R a]
 
+section Comp
+
 variable [UniqueNonUnitalContinuousFunctionalCalculus R A]
 
 lemma cfcₙ_comp (g f : R → R) (a : A)
@@ -429,6 +431,8 @@ lemma cfcₙ_comp_star (hf : ContinuousOn f (star '' (σₙ R a)) := by cfc_cont
     cfcₙ (f <| star ·) a = cfcₙ f (star a) := by
   rw [cfcₙ_comp' f star a, cfcₙ_star_id a]
 
+end Comp
+
 lemma CFC.eq_zero_of_quasispectrum_eq_zero (h_spec : σₙ R a ⊆ {0}) (ha : p a := by cfc_tac) :
     a = 0 := by
   simpa [cfcₙ_id R a] using cfcₙ_congr (a := a) (f := id) (g := fun _ : R ↦ 0) fun x ↦ by simp_all
@@ -505,17 +509,17 @@ section Order
 section Semiring
 
 variable {R A : Type*} {p : A → Prop} [OrderedCommSemiring R] [Nontrivial R]
-variable [StarRing R] [StarOrderedRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R]
+variable [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R]
 variable [∀ (α) [Zero α] [TopologicalSpace α], StarOrderedRing C(α, R)₀]
 variable [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [PartialOrder A] [StarOrderedRing A]
-variable [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A]
-variable [NonUnitalContinuousFunctionalCalculus R p] [NonnegSpectrumClass R A]
+variable [Module R A] [IsScalarTower R A A] [SMulCommClass R A A]
+variable [NonUnitalContinuousFunctionalCalculus R p]
 
 lemma cfcₙHom_mono {a : A} (ha : p a) {f g : C(σₙ R a, R)₀} (hfg : f ≤ g) :
     cfcₙHom ha f ≤ cfcₙHom ha g :=
   OrderHomClass.mono (cfcₙHom ha) hfg
 
-lemma cfcₙHom_nonneg_iff {a : A} (ha : p a) {f : C(σₙ R a, R)₀} :
+lemma cfcₙHom_nonneg_iff [NonnegSpectrumClass R A] {a : A} (ha : p a) {f : C(σₙ R a, R)₀} :
     0 ≤ cfcₙHom ha f ↔ 0 ≤ f := by
   constructor
   · exact fun hf x ↦
@@ -533,15 +537,16 @@ lemma cfcₙ_mono {f g : R → R} {a : A} (h : ∀ x ∈ σₙ R a, f x ≤ g x)
     exact cfcₙHom_mono ha fun x ↦ h x.1 x.2
   · simp only [cfcₙ_apply_of_not_predicate _ ha, le_rfl]
 
-lemma cfcₙ_nonneg_iff (f : R → R) (a : A) (hf : ContinuousOn f (σₙ R a) := by cfc_cont_tac)
+lemma cfcₙ_nonneg_iff [NonnegSpectrumClass R A] (f : R → R) (a : A)
+    (hf : ContinuousOn f (σₙ R a) := by cfc_cont_tac)
     (h0 : f 0 = 0 := by cfc_zero_tac) (ha : p a := by cfc_tac) :
     0 ≤ cfcₙ f a ↔ ∀ x ∈ σₙ R a, 0 ≤ f x := by
   rw [cfcₙ_apply .., cfcₙHom_nonneg_iff, ContinuousMapZero.le_def]
   simp only [ContinuousMapZero.coe_mk, ContinuousMap.coe_mk, Set.restrict_apply, Subtype.forall]
   congr!
 
-lemma StarOrderedRing.nonneg_iff_quasispectrum_nonneg (a : A) (ha : p a := by cfc_tac) :
-    0 ≤ a ↔ ∀ x ∈ quasispectrum R a, 0 ≤ x := by
+lemma StarOrderedRing.nonneg_iff_quasispectrum_nonneg [NonnegSpectrumClass R A] (a : A)
+    (ha : p a := by cfc_tac) : 0 ≤ a ↔ ∀ x ∈ quasispectrum R a, 0 ≤ x := by
   have := cfcₙ_nonneg_iff (id : R → R) a (by fun_prop)
   simpa [cfcₙ_id _ a ha] using this
 
@@ -570,10 +575,10 @@ end Semiring
 section Ring
 
 variable {R A : Type*} {p : A → Prop} [OrderedCommRing R] [Nontrivial R]
-variable [StarRing R] [StarOrderedRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R]
+variable [StarRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R]
 variable [∀ (α) [Zero α] [TopologicalSpace α], StarOrderedRing C(α, R)₀]
 variable [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [PartialOrder A] [StarOrderedRing A]
-variable [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A]
+variable [Module R A] [IsScalarTower R A A] [SMulCommClass R A A]
 variable [NonUnitalContinuousFunctionalCalculus R p] [NonnegSpectrumClass R A]
 
 lemma cfcₙHom_le_iff {a : A} (ha : p a) {f g : C(σₙ R a, R)₀} :
@@ -603,10 +608,9 @@ section UnitalToNonUnital
 
 open ContinuousMapZero Set Uniformity ContinuousMap
 
-variable {R A : Type*} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [CompleteSpace R]
+variable {R A : Type*} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R]
 variable [TopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A]
 variable [Algebra R A] [ContinuousFunctionalCalculus R p]
-variable [h_cpct : ∀ a : A, CompactSpace (spectrum R a)]
 
 variable (R) in
 /-- The non-unital continuous functional calculus obtained by restricting a unital calculus
@@ -621,6 +625,30 @@ noncomputable def cfcₙHom_of_cfcHom {a : A} (ha : p a) : C(σₙ R a, R)₀ 
   (cfcHom ha (R := R) : C(spectrum R a, R) →⋆ₙₐ[R] A).comp <|
     (ψ : C(σₙ R a, R) →⋆ₙₐ[R] C(spectrum R a, R)).comp e
 
+lemma cfcₙHom_of_cfcHom_map_quasispectrum {a : A} (ha : p a) :
+    ∀ f : C(σₙ R a, R)₀, σₙ R (cfcₙHom_of_cfcHom R ha f) = range f := by
+  intro f
+  simp only [cfcₙHom_of_cfcHom]
+  rw [quasispectrum_eq_spectrum_union_zero]
+  simp only [NonUnitalStarAlgHom.comp_assoc, NonUnitalStarAlgHom.comp_apply,
+    NonUnitalStarAlgHom.coe_coe]
+  rw [cfcHom_map_spectrum ha]
+  ext x
+  constructor
+  · rintro (⟨x, rfl⟩ | rfl)
+    · exact ⟨⟨x.1, spectrum_subset_quasispectrum R a x.2⟩, rfl⟩
+    · exact ⟨0, map_zero f⟩
+  · rintro ⟨x, rfl⟩
+    have hx := x.2
+    simp_rw [quasispectrum_eq_spectrum_union_zero R a] at hx
+    obtain (hx | hx) := hx
+    · exact Or.inl ⟨⟨x.1, hx⟩, rfl⟩
+    · apply Or.inr
+      simp only [Set.mem_singleton_iff] at hx ⊢
+      rw [show x = 0 from Subtype.val_injective hx, map_zero]
+
+variable [CompleteSpace R] [h_cpct : ∀ a : A, CompactSpace (spectrum R a)]
+
 lemma closedEmbedding_cfcₙHom_of_cfcHom {a : A} (ha : p a) :
     ClosedEmbedding (cfcₙHom_of_cfcHom R ha) := by
   let f : C(spectrum R a, σₙ R a) :=
@@ -645,28 +673,6 @@ lemma closedEmbedding_cfcₙHom_of_cfcHom {a : A} (ha : p a) :
   convert Filter.comap_const_of_mem this with ⟨u, v⟩ <;>
   ext ⟨x, rfl⟩ <;> [exact map_zero u; exact map_zero v]
 
-lemma cfcₙHom_of_cfcHom_map_quasispectrum {a : A} (ha : p a) :
-    ∀ f : C(σₙ R a, R)₀, σₙ R (cfcₙHom_of_cfcHom R ha f) = range f := by
-  intro f
-  simp only [cfcₙHom_of_cfcHom]
-  rw [quasispectrum_eq_spectrum_union_zero]
-  simp only [NonUnitalStarAlgHom.comp_assoc, NonUnitalStarAlgHom.comp_apply,
-    NonUnitalStarAlgHom.coe_coe]
-  rw [cfcHom_map_spectrum ha]
-  ext x
-  constructor
-  · rintro (⟨x, rfl⟩ | rfl)
-    · exact ⟨⟨x.1, spectrum_subset_quasispectrum R a x.2⟩, rfl⟩
-    · exact ⟨0, map_zero f⟩
-  · rintro ⟨x, rfl⟩
-    have hx := x.2
-    simp_rw [quasispectrum_eq_spectrum_union_zero R a] at hx
-    obtain (hx | hx) := hx
-    · exact Or.inl ⟨⟨x.1, hx⟩, rfl⟩
-    · apply Or.inr
-      simp only [Set.mem_singleton_iff] at hx ⊢
-      rw [show x = 0 from Subtype.val_injective hx, map_zero]
-
 instance ContinuousFunctionalCalculus.toNonUnital : NonUnitalContinuousFunctionalCalculus R p where
   predicate_zero := cfc_predicate_zero R
   exists_cfc_of_predicate _ ha :=

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean

@@ -191,7 +191,7 @@ class UniqueContinuousFunctionalCalculus (R A : Type*) [CommSemiring R] [StarRin
 
 variable {R A : Type*} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R]
 variable [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A]
-variable [Algebra R A] [ContinuousFunctionalCalculus R p]
+variable [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p]
 
 lemma StarAlgHom.ext_continuousMap [UniqueContinuousFunctionalCalculus R A]
     (a : A) (φ ψ : C(spectrum R a, R) →⋆ₐ[R] A) (hφ : Continuous φ) (hψ : Continuous ψ)
@@ -374,18 +374,15 @@ lemma eqOn_of_cfc_eq_cfc {f g : R → R} {a : A} (h : cfc f a = cfc g a)
   congrm($(this) ⟨x, hx⟩)
 
 variable {a f g} in
-lemma cfc_eq_cfc_iff_eqOn (ha : p a := by cfc_tac)
-    (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac)
-    (hg : ContinuousOn g (spectrum R a) := by cfc_cont_tac) :
-    cfc f a = cfc g a ↔ (spectrum R a).EqOn f g :=
+lemma cfc_eq_cfc_iff_eqOn : cfc f a = cfc g a ↔ (spectrum R a).EqOn f g :=
   ⟨eqOn_of_cfc_eq_cfc, cfc_congr⟩
 
 variable (R)
 
-lemma cfc_one (ha : p a := by cfc_tac) : cfc (1 : R → R) a = 1 :=
+lemma cfc_one : cfc (1 : R → R) a = 1 :=
   cfc_apply (1 : R → R) a ▸ map_one (cfcHom (show p a from ha))
 
-lemma cfc_const_one (ha : p a := by cfc_tac) : cfc (fun _ : R ↦ 1) a = 1 := cfc_one R a
+lemma cfc_const_one : cfc (fun _ : R ↦ 1) a = 1 := cfc_one R a
 
 @[simp]
 lemma cfc_zero : cfc (0 : R → R) a = 0 := by
@@ -493,7 +490,7 @@ lemma cfc_smul_id {S : Type*} [SMul S R] [ContinuousConstSMul S R]
 lemma cfc_const_mul_id (r : R) (a : A) (ha : p a := by cfc_tac) : cfc (r * ·) a = r • a :=
   cfc_smul_id r a
 
-lemma cfc_star_id (ha : p a := by cfc_tac) : cfc (star · : R → R) a = star a := by
+lemma cfc_star_id : cfc (star · : R → R) a = star a := by
   rw [cfc_star .., cfc_id' ..]
 
 section Polynomial
@@ -523,18 +520,7 @@ lemma cfc_polynomial (q : R[X]) (a : A) (ha : p a := by cfc_tac) :
 
 end Polynomial
 
-lemma CFC.eq_algebraMap_of_spectrum_subset_singleton (r : R) (h_spec : spectrum R a ⊆ {r})
-    (ha : p a := by cfc_tac) : a = algebraMap R A r := by
-  simpa [cfc_id R a, cfc_const r a] using
-    cfc_congr (f := id) (g := fun _ : R ↦ r) (a := a) fun x hx ↦ by simpa using h_spec hx
-
-lemma CFC.eq_zero_of_spectrum_subset_zero (h_spec : spectrum R a ⊆ {0}) (ha : p a := by cfc_tac) :
-    a = 0 := by
-  simpa using eq_algebraMap_of_spectrum_subset_singleton a 0 h_spec
-
-lemma CFC.eq_one_of_spectrum_subset_one (h_spec : spectrum R a ⊆ {1}) (ha : p a := by cfc_tac) :
-    a = 1 := by
-  simpa using eq_algebraMap_of_spectrum_subset_singleton a 1 h_spec
+section Comp
 
 variable [UniqueContinuousFunctionalCalculus R A]
 
@@ -587,6 +573,21 @@ lemma cfc_comp_polynomial (q : R[X]) (f : R → R) (a : A)
     cfc (f <| q.eval ·) a = cfc f (aeval a q) := by
   rw [cfc_comp' .., cfc_polynomial ..]
 
+end Comp
+
+lemma CFC.eq_algebraMap_of_spectrum_subset_singleton (r : R) (h_spec : spectrum R a ⊆ {r})
+    (ha : p a := by cfc_tac) : a = algebraMap R A r := by
+  simpa [cfc_id R a, cfc_const r a] using
+    cfc_congr (f := id) (g := fun _ : R ↦ r) (a := a) fun x hx ↦ by simpa using h_spec hx
+
+lemma CFC.eq_zero_of_spectrum_subset_zero (h_spec : spectrum R a ⊆ {0}) (ha : p a := by cfc_tac) :
+    a = 0 := by
+  simpa using eq_algebraMap_of_spectrum_subset_singleton a 0 h_spec
+
+lemma CFC.eq_one_of_spectrum_subset_one (h_spec : spectrum R a ⊆ {1}) (ha : p a := by cfc_tac) :
+    a = 1 := by
+  simpa using eq_algebraMap_of_spectrum_subset_singleton a 1 h_spec
+
 lemma CFC.spectrum_algebraMap_subset (r : R) : spectrum R (algebraMap R A r) ⊆ {r} := by
   rw [← cfc_const r 0 (cfc_predicate_zero R),
     cfc_map_spectrum (fun _ ↦ r) 0 (cfc_predicate_zero R)]
@@ -644,16 +645,15 @@ section Inv
 variable {R A : Type*} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R]
 variable [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A]
 variable [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R p]
-variable (f : R → R) (a : A)
 
-lemma isUnit_cfc_iff (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac)
+lemma isUnit_cfc_iff (f : R → R) (a : A) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac)
     (ha : p a := by cfc_tac) : IsUnit (cfc f a) ↔ ∀ x ∈ spectrum R a, f x ≠ 0 := by
   rw [← spectrum.zero_not_mem_iff R, cfc_map_spectrum ..]
   aesop
 
 alias ⟨_, isUnit_cfc⟩ := isUnit_cfc_iff
 
-variable [HasContinuousInv₀ R]
+variable [HasContinuousInv₀ R] (f : R → R) (a : A)
 
 /-- Bundle `cfc f a` into a unit given a proof that `f` is nonzero on the spectrum of `a`. -/
 @[simps]
@@ -697,24 +697,24 @@ lemma cfc_map_div (f g : R → R) (a : A) (hg' : ∀ x ∈ spectrum R a, g x ≠
   simp only [div_eq_mul_inv]
   rw [cfc_mul .., cfc_inv g a hg']
 
-variable [UniqueContinuousFunctionalCalculus R A]
+section ContinuousOnInvSpectrum
+-- TODO: this section should probably be moved to another file altogether
+
+variable {R A : Type*} [Semifield R] [Ring A] [TopologicalSpace R] [HasContinuousInv₀ R]
+variable [Algebra R A]
 
 @[fun_prop]
 lemma Units.continuousOn_inv₀_spectrum (a : Aˣ) : ContinuousOn (· ⁻¹) (spectrum R (a : A)) :=
   continuousOn_inv₀.mono <| by
     simpa only [Set.subset_compl_singleton_iff] using spectrum.zero_not_mem R a.isUnit
 
 @[fun_prop]
-lemma Units.continuousOn_zpow₀_spectrum (a : Aˣ) (n : ℤ) :
+lemma Units.continuousOn_zpow₀_spectrum [ContinuousMul R] (a : Aˣ) (n : ℤ) :
     ContinuousOn (· ^ n) (spectrum R (a : A)) :=
   (continuousOn_zpow₀ n).mono <| by
     simpa only [Set.subset_compl_singleton_iff] using spectrum.zero_not_mem R a.isUnit
 
-lemma cfc_comp_inv (f : R → R) (a : Aˣ)
-    (hf : ContinuousOn f ((· ⁻¹) '' (spectrum R (a : A))) := by cfc_cont_tac)
-    (ha : p a := by cfc_tac) :
-    cfc (fun x ↦ f x⁻¹) (a : A) = cfc f (↑a⁻¹ : A) := by
-  rw [cfc_comp' .., cfc_inv_id _]
+end ContinuousOnInvSpectrum
 
 lemma cfcUnits_zpow (hf' : ∀ x ∈ spectrum R a, f x ≠ 0) (n : ℤ)
     (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) :
@@ -737,6 +737,14 @@ lemma cfc_zpow (a : Aˣ) (n : ℤ) (ha : p a := by cfc_tac) :
     have := cfc_pow (fun x ↦ x⁻¹ : R → R) (n + 1) (a : A)
     exact this.trans <| congr($(cfc_inv_id a) ^ (n + 1))
 
+variable [UniqueContinuousFunctionalCalculus R A]
+
+lemma cfc_comp_inv (f : R → R) (a : Aˣ)
+    (hf : ContinuousOn f ((· ⁻¹) '' (spectrum R (a : A))) := by cfc_cont_tac)
+    (ha : p a := by cfc_tac) :
+    cfc (fun x ↦ f x⁻¹) (a : A) = cfc f (↑a⁻¹ : A) := by
+  rw [cfc_comp' .., cfc_inv_id _]
+
 lemma cfc_comp_zpow (f : R → R) (n : ℤ) (a : Aˣ)
     (hf : ContinuousOn f ((· ^ n) '' (spectrum R (a : A))) := by cfc_cont_tac)
     (ha : p a := by cfc_tac) :
@@ -785,17 +793,16 @@ section Order
 section Semiring
 
 variable {R A : Type*} {p : A → Prop} [OrderedCommSemiring R] [StarRing R]
-variable [StarOrderedRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R]
+variable [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R]
 variable [∀ (α) [TopologicalSpace α], StarOrderedRing C(α, R)]
 variable [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A]
-variable [Algebra R A] [StarModule R A] [ContinuousFunctionalCalculus R p]
-variable [NonnegSpectrumClass R A]
+variable [Algebra R A] [ContinuousFunctionalCalculus R p]
 
 lemma cfcHom_mono {a : A} (ha : p a) {f g : C(spectrum R a, R)} (hfg : f ≤ g) :
     cfcHom ha f ≤ cfcHom ha g :=
   OrderHomClass.mono (cfcHom ha) hfg
 
-lemma cfcHom_nonneg_iff {a : A} (ha : p a) {f : C(spectrum R a, R)} :
+lemma cfcHom_nonneg_iff [NonnegSpectrumClass R A] {a : A} (ha : p a) {f : C(spectrum R a, R)} :
     0 ≤ cfcHom ha f ↔ 0 ≤ f := by
   constructor
   · exact fun hf x ↦ (cfcHom_map_spectrum ha (R := R) _ ▸ spectrum_nonneg_of_nonneg hf) ⟨x, rfl⟩
@@ -810,13 +817,14 @@ lemma cfc_mono {f g : R → R} {a : A} (h : ∀ x ∈ spectrum R a, f x ≤ g x)
     exact cfcHom_mono ha fun x ↦ h x.1 x.2
   · simp only [cfc_apply_of_not_predicate _ ha, le_rfl]
 
-lemma cfc_nonneg_iff (f : R → R) (a : A) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac)
+lemma cfc_nonneg_iff [NonnegSpectrumClass R A] (f : R → R) (a : A)
+    (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac)
     (ha : p a := by cfc_tac) : 0 ≤ cfc f a ↔ ∀ x ∈ spectrum R a, 0 ≤ f x := by
   rw [cfc_apply .., cfcHom_nonneg_iff, ContinuousMap.le_def]
   simp
 
-lemma StarOrderedRing.nonneg_iff_spectrum_nonneg (a : A) (ha : p a := by cfc_tac) :
-    0 ≤ a ↔ ∀ x ∈ spectrum R a, 0 ≤ x := by
+lemma StarOrderedRing.nonneg_iff_spectrum_nonneg [NonnegSpectrumClass R A] (a : A)
+    (ha : p a := by cfc_tac) : 0 ≤ a ↔ ∀ x ∈ spectrum R a, 0 ≤ x := by
   have := cfc_nonneg_iff (id : R → R) a (by fun_prop) ha
   simpa [cfc_id _ a ha] using this
 
@@ -871,7 +879,7 @@ variable {R A : Type*} {p : A → Prop} [OrderedCommRing R] [StarRing R]
 variable [MetricSpace R] [TopologicalRing R] [ContinuousStar R]
 variable [∀ (α) [TopologicalSpace α], StarOrderedRing C(α, R)]
 variable [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A]
-variable [Algebra R A] [StarModule R A] [ContinuousFunctionalCalculus R p]
+variable [Algebra R A] [ContinuousFunctionalCalculus R p]
 variable [NonnegSpectrumClass R A]
 
 lemma cfcHom_le_iff {a : A} (ha : p a) {f g : C(spectrum R a, R)} :