Merge remote-tracking branch 'origin/master' into adomani/deprecation…

…s_script

Mathlib.lean

@@ -1006,6 +1006,7 @@ import Mathlib.Analysis.BoxIntegral.Partition.Measure
 import Mathlib.Analysis.BoxIntegral.Partition.Split
 import Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
 import Mathlib.Analysis.BoxIntegral.Partition.Tagged
+import Mathlib.Analysis.CStarAlgebra.ApproximateUnit
 import Mathlib.Analysis.CStarAlgebra.Basic
 import Mathlib.Analysis.CStarAlgebra.Classes
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
@@ -2261,6 +2262,7 @@ import Mathlib.Data.Fin.Tuple.Finset
 import Mathlib.Data.Fin.Tuple.NatAntidiagonal
 import Mathlib.Data.Fin.Tuple.Reflection
 import Mathlib.Data.Fin.Tuple.Sort
+import Mathlib.Data.Fin.Tuple.Take
 import Mathlib.Data.Fin.VecNotation
 import Mathlib.Data.FinEnum
 import Mathlib.Data.Finite.Card
@@ -4620,6 +4622,7 @@ import Mathlib.Topology.Algebra.Affine
 import Mathlib.Topology.Algebra.Algebra
 import Mathlib.Topology.Algebra.Algebra.Rat
 import Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
+import Mathlib.Topology.Algebra.ClopenNhdofOne
 import Mathlib.Topology.Algebra.ClosedSubgroup
 import Mathlib.Topology.Algebra.ConstMulAction
 import Mathlib.Topology.Algebra.Constructions

Mathlib/Algebra/Algebra/Equiv.lean

@@ -130,7 +130,6 @@ theorem mk_coe (e : A₁ ≃ₐ[R] A₂) (e' h₁ h₂ h₃ h₄ h₅) :
 theorem toEquiv_eq_coe : e.toEquiv = e :=
   rfl
 
--- Porting note: `protected` used to be an attribute below
 @[simp]
 protected theorem coe_coe {F : Type*} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂] (f : F) :
     ⇑(f : A₁ ≃ₐ[R] A₂) = f :=

Mathlib/Algebra/GroupWithZero/Divisibility.lean

@@ -139,9 +139,6 @@ theorem dvd_antisymm : a ∣ b → b ∣ a → a = b := by
   rw [mul_assoc, eq_comm, mul_right_eq_self₀, mul_eq_one] at hcd
   obtain ⟨rfl, -⟩ | rfl := hcd <;> simp
 
--- Porting note: `attribute [protected]` is currently unsupported
--- attribute [protected] Nat.dvd_antisymm --This lemma is in core, so we protect it here
-
 theorem dvd_antisymm' : a ∣ b → b ∣ a → b = a :=
   flip dvd_antisymm
 

Mathlib/Algebra/ModEq.lean

@@ -174,16 +174,13 @@ protected theorem sub_iff_right :
     a₂ ≡ b₂ [PMOD p] → (a₁ - a₂ ≡ b₁ - b₂ [PMOD p] ↔ a₁ ≡ b₁ [PMOD p]) := fun ⟨m, hm⟩ =>
   (Equiv.subRight m).symm.exists_congr_left.trans <| by simp [sub_sub_sub_comm, hm, sub_smul, ModEq]
 
-alias ⟨add_left_cancel, add⟩ := ModEq.add_iff_left
+protected alias ⟨add_left_cancel, add⟩ := ModEq.add_iff_left
 
-alias ⟨add_right_cancel, _⟩ := ModEq.add_iff_right
+protected alias ⟨add_right_cancel, _⟩ := ModEq.add_iff_right
 
-alias ⟨sub_left_cancel, sub⟩ := ModEq.sub_iff_left
+protected alias ⟨sub_left_cancel, sub⟩ := ModEq.sub_iff_left
 
-alias ⟨sub_right_cancel, _⟩ := ModEq.sub_iff_right
-
--- Porting note: doesn't work
--- attribute [protected] add_left_cancel add_right_cancel add sub_left_cancel sub_right_cancel sub
+protected alias ⟨sub_right_cancel, _⟩ := ModEq.sub_iff_right
 
 protected theorem add_left (c : α) (h : a ≡ b [PMOD p]) : c + a ≡ c + b [PMOD p] :=
   modEq_rfl.add h

Mathlib/Algebra/Module/Equiv/Defs.lean

@@ -391,6 +391,18 @@ theorem toLinearMap_symm_comp_eq (f : M₃ →ₛₗ[σ₃₁] M₁) (g : M₃ 
   · simp [← H, ← e₁₂.toEquiv.symm_comp_eq f g]
   · simp [H, e₁₂.toEquiv.symm_comp_eq f g]
 
+@[simp]
+theorem comp_toLinearMap_eq_iff (f g : M₃ →ₛₗ[σ₃₁] M₁) :
+    e₁₂.toLinearMap.comp f = e₁₂.toLinearMap.comp g ↔ f = g := by
+  refine ⟨fun h => ?_, congrArg e₁₂.comp⟩
+  rw [← (toLinearMap_symm_comp_eq g (e₁₂.toLinearMap.comp f)).mpr h, eq_toLinearMap_symm_comp]
+
+@[simp]
+theorem eq_comp_toLinearMap_iff (f g : M₂ →ₛₗ[σ₂₃] M₃) :
+    f.comp e₁₂.toLinearMap = g.comp e₁₂.toLinearMap ↔ f = g := by
+  refine ⟨fun h => ?_, fun a ↦ congrFun (congrArg LinearMap.comp a) e₁₂.toLinearMap⟩
+  rw [(eq_comp_toLinearMap_symm g (f.comp e₁₂.toLinearMap)).mpr h.symm, eq_comp_toLinearMap_symm]
+
 @[simp]
 theorem refl_symm [Module R M] : (refl R M).symm = LinearEquiv.refl R M :=
   rfl

Mathlib/Algebra/Ring/Int.lean

@@ -176,13 +176,8 @@ lemma even_mul_pred_self (n : ℤ) : Even (n * (n - 1)) := by
 lemma natAbs_odd : Odd n.natAbs ↔ Odd n := by
   rw [← not_even_iff_odd, ← Nat.not_even_iff_odd, natAbs_even]
 
-alias ⟨_, _root_.Even.natAbs⟩ := natAbs_even
-
-alias ⟨_, _root_.Odd.natAbs⟩ := natAbs_odd
-
--- Porting note: "protected"-attribute not implemented yet.
--- mathlib3 had:
--- `attribute [protected] Even.natAbs Odd.natAbs`
+protected alias ⟨_, _root_.Even.natAbs⟩ := natAbs_even
+protected alias ⟨_, _root_.Odd.natAbs⟩ := natAbs_odd
 
 lemma four_dvd_add_or_sub_of_odd {a b : ℤ} (ha : Odd a) (hb : Odd b) :
     4 ∣ a + b ∨ 4 ∣ a - b := by

Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean

@@ -808,7 +808,6 @@ lemma baseChange_polynomial : (W.baseChange B).toAffine.polynomial =
     (W.baseChange A).toAffine.polynomial.map (mapRingHom f) := by
   rw [← map_polynomial, map_baseChange]
 
-variable {g} in
 lemma baseChange_equation (hf : Function.Injective f) (x y : A) :
     (W.baseChange B).toAffine.Equation (f x) (f y) ↔ (W.baseChange A).toAffine.Equation x y := by
   erw [← map_equation _ hf, map_baseChange]

Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean

@@ -61,7 +61,7 @@ structure VariableChange (R : Type u) [CommRing R] where
 
 namespace VariableChange
 
-variable (C C' C'' : VariableChange R)
+variable (C C' : VariableChange R)
 
 /-- The identity linear change of variables given by the identity matrix. -/
 def id : VariableChange R :=

Mathlib/Analysis/BoxIntegral/Integrability.lean

@@ -321,7 +321,8 @@ theorem AEContinuous.hasBoxIntegral [CompleteSpace E] {f : (ι → ℝ) → E} (
   constructor
   · let v := {x : (ι → ℝ) | ContinuousAt f x}
     have : AEStronglyMeasurable f (μ.restrict v) :=
-      (ContinuousAt.continuousOn fun _ h ↦ h).aestronglyMeasurable (measurableSet_of_continuousAt f)
+      (continuousOn_of_forall_continuousAt fun _ h ↦ h).aestronglyMeasurable
+      (measurableSet_of_continuousAt f)
     refine this.mono_measure (Measure.le_iff.2 fun s hs ↦ ?_)
     repeat rw [μ.restrict_apply hs]
     apply le_of_le_of_eq <| μ.mono s.inter_subset_left

Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean

@@ -0,0 +1,107 @@
+/-
+Copyright (c) 2024 Jireh Loreaux. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jireh Loreaux
+-/
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
+import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow
+
+/-! # Positive contractions in a C⋆-algebra form an approximate unit
+
+This file will show (although it does not yet) that the collection of positive contractions (of norm
+strictly less than one) in a possibly non-unital C⋆-algebra form an approximate unit. The key step
+is to show that this set is directed using the continuous functional calculus applied with the
+functions `fun x : ℝ≥0, 1 - (1 + x)⁻¹` and `fun x : ℝ≥0, x * (1 - x)⁻¹`, which are inverses on
+the interval `{x : ℝ≥0 | x < 1}`.
+
+## Main declarations
+
++ `CFC.monotoneOn_one_sub_one_add_inv`: the function `f := fun x : ℝ≥0, 1 - (1 + x)⁻¹` is
+  *operator monotone* on `Set.Ici (0 : A)` (i.e., `cfcₙ f` is monotone on `{x : A | 0 ≤ x}`).
++ `Set.InvOn.one_sub_one_add_inv`: the functions `f := fun x : ℝ≥0, 1 - (1 + x)⁻¹` and
+  `g := fun x : ℝ≥0, x * (1 - x)⁻¹` are inverses on `{x : ℝ≥0 | x < 1}`.
++ `CStarAlgebra.directedOn_nonneg_ball`: the set `{x : A | 0 ≤ x} ∩ Metric.ball 0 1` is directed.
+
+## TODO
+
++ Prove the approximate identity result by following Ken Davidson's proof in
+  "C*-Algebras by Example"
+
+-/
+
+variable {A : Type*} [NonUnitalCStarAlgebra A]
+
+local notation "σₙ" => quasispectrum
+local notation "σ" => spectrum
+
+open Unitization NNReal CStarAlgebra
+
+variable [PartialOrder A] [StarOrderedRing A]
+
+lemma CFC.monotoneOn_one_sub_one_add_inv :
+    MonotoneOn (cfcₙ (fun x : ℝ≥0 ↦ 1 - (1 + x)⁻¹)) (Set.Ici (0 : A)) := by
+  intro a ha b hb hab
+  simp only [Set.mem_Ici] at ha hb
+  rw [← inr_le_iff .., nnreal_cfcₙ_eq_cfc_inr a _, nnreal_cfcₙ_eq_cfc_inr b _]
+  rw [← inr_le_iff a b (.of_nonneg ha) (.of_nonneg hb)] at hab
+  rw [← inr_nonneg_iff] at ha hb
+  have h_cfc_one_sub (c : A⁺¹) (hc : 0 ≤ c := by cfc_tac) :
+      cfc (fun x : ℝ≥0 ↦ 1 - (1 + x)⁻¹) c = 1 - cfc (·⁻¹ : ℝ≥0 → ℝ≥0) (1 + c) := by
+    rw [cfc_tsub _ _ _ (fun x _ ↦ by simp) (hg := by fun_prop (disch := intro _ _; positivity)),
+      cfc_const_one ℝ≥0 c, cfc_comp' (·⁻¹) (1 + ·) c ?_, cfc_add .., cfc_const_one ℝ≥0 c,
+      cfc_id' ℝ≥0 c]
+    exact continuousOn_id.inv₀ (Set.forall_mem_image.mpr fun x _ ↦ by dsimp only [id]; positivity)
+  rw [h_cfc_one_sub (a : A⁺¹), h_cfc_one_sub (b : A⁺¹)]
+  gcongr
+  rw [← CFC.rpow_neg_one_eq_cfc_inv, ← CFC.rpow_neg_one_eq_cfc_inv]
+  exact rpow_neg_one_le_rpow_neg_one (add_nonneg zero_le_one ha) (by gcongr) <|
+    isUnit_of_le isUnit_one zero_le_one <| le_add_of_nonneg_right ha
+
+lemma Set.InvOn.one_sub_one_add_inv : Set.InvOn (fun x ↦ 1 - (1 + x)⁻¹) (fun x ↦ x * (1 - x)⁻¹)
+    {x : ℝ≥0 | x < 1} {x : ℝ≥0 | x < 1} := by
+  have : (fun x : ℝ≥0 ↦ x * (1 + x)⁻¹) = fun x ↦ 1 - (1 + x)⁻¹ := by
+    ext x : 1
+    field_simp
+    simp [tsub_mul, inv_mul_cancel₀]
+  rw [← this]
+  constructor <;> intro x (hx : x < 1)
+  · have : 0 < 1 - x := tsub_pos_of_lt hx
+    field_simp [tsub_add_cancel_of_le hx.le, tsub_tsub_cancel_of_le hx.le]
+  · field_simp [mul_tsub]
+
+lemma norm_cfcₙ_one_sub_one_add_inv_lt_one (a : A) :
+    ‖cfcₙ (fun x : ℝ≥0 ↦ 1 - (1 + x)⁻¹) a‖ < 1 :=
+  nnnorm_cfcₙ_nnreal_lt fun x _ ↦ tsub_lt_self zero_lt_one (by positivity)
+
+-- the calls to `fun_prop` with a discharger set off the linter
+set_option linter.style.multiGoal false in
+lemma CStarAlgebra.directedOn_nonneg_ball :
+    DirectedOn (· ≤ ·) ({x : A | 0 ≤ x} ∩ Metric.ball 0 1) := by
+  let f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹
+  let g : ℝ≥0 → ℝ≥0 := fun x => x * (1 - x)⁻¹
+  suffices ∀ a b : A, 0 ≤ a → 0 ≤ b → ‖a‖ < 1 → ‖b‖ < 1 →
+      a ≤ cfcₙ f (cfcₙ g a + cfcₙ g b) by
+    rintro a ⟨(ha₁ : 0 ≤ a), ha₂⟩ b ⟨(hb₁ : 0 ≤ b), hb₂⟩
+    simp only [Metric.mem_ball, dist_zero_right] at ha₂ hb₂
+    refine ⟨cfcₙ f (cfcₙ g a + cfcₙ g b), ⟨by simp, ?_⟩, ?_, ?_⟩
+    · simpa only [Metric.mem_ball, dist_zero_right] using norm_cfcₙ_one_sub_one_add_inv_lt_one _
+    · exact this a b ha₁ hb₁ ha₂ hb₂
+    · exact add_comm (cfcₙ g a) (cfcₙ g b) ▸ this b a hb₁ ha₁ hb₂ ha₂
+  rintro a b ha₁ - ha₂ -
+  calc
+    a = cfcₙ (f ∘ g) a := by
+      conv_lhs => rw [← cfcₙ_id ℝ≥0 a]
+      refine cfcₙ_congr (Set.InvOn.one_sub_one_add_inv.1.eqOn.symm.mono fun x hx ↦ ?_)
+      exact lt_of_le_of_lt (le_nnnorm_of_mem_quasispectrum hx) ha₂
+    _ = cfcₙ f (cfcₙ g a) := by
+      rw [cfcₙ_comp f g a ?_ (by simp [f, tsub_self]) ?_ (by simp [g]) ha₁]
+      · fun_prop (disch := intro _ _; positivity)
+      · have (x) (hx : x ∈ σₙ ℝ≥0 a) :  1 - x ≠ 0 := by
+          refine tsub_pos_of_lt ?_ |>.ne'
+          exact lt_of_le_of_lt (le_nnnorm_of_mem_quasispectrum hx) ha₂
+        fun_prop (disch := assumption)
+    _ ≤ cfcₙ f (cfcₙ g a + cfcₙ g b) := by
+      have hab' : cfcₙ g a ≤ cfcₙ g a + cfcₙ g b := le_add_of_nonneg_right cfcₙ_nonneg_of_predicate
+      exact CFC.monotoneOn_one_sub_one_add_inv cfcₙ_nonneg_of_predicate
+        (cfcₙ_nonneg_of_predicate.trans hab') hab'

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/PosPart.lean

@@ -4,18 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jireh Loreaux
 -/
 
-import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
 import Mathlib.Topology.ContinuousMap.StarOrdered
+import Mathlib.Analysis.InnerProductSpace.Basic
+import Mathlib.Topology.ContinuousMap.StoneWeierstrass
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
 
 /-! # The positive (and negative) parts of a selfadjoint element in a C⋆-algebra
 
 This file defines the positive and negative parts of a selfadjoint element in a C⋆-algebra via
-the continuous functional calculus and develops the basic API.
-
-## TODO
-
-+ Prove that the positive and negative parts are unique.
-
+the continuous functional calculus and develops the basic API, including the uniqueness of the
+positive and negative parts.
 -/
 
 variable {A : Type*} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A]
@@ -129,4 +127,102 @@ lemma posPart_eq_zero_iff (a : A) (ha : IsSelfAdjoint a) :
   nth_rw 2 [← posPart_sub_negPart a]
   simp
 
+local notation "σₙ" => quasispectrum
+
+open ContinuousMapZero
+
+variable [UniqueNonUnitalContinuousFunctionalCalculus ℝ A]
+variable [TopologicalRing A] [T2Space A]
+
+open NonUnitalContinuousFunctionalCalculus in
+/-- The positive and negative parts of a selfadjoint element `a` are unique. That is, if
+`a = b - c` is the difference of nonnegative elements whose product is zero, then these are
+precisely `a⁺` and `a⁻`. -/
+lemma posPart_negPart_unique {a b c : A} (habc : a = b - c) (hbc : b * c = 0)
+    (hb : 0 ≤ b := by cfc_tac) (hc : 0 ≤ c := by cfc_tac) :
+    b = a⁺ ∧ c = a⁻ := by
+  /- The key idea is to show that `cfcₙ f a = cfcₙ f b + cfcₙ f (-c)` for all real-valued `f`
+  continuous on the union of the spectra of `a`, `b`, and `-c`. Then apply this to `f = (·⁺)`.
+  The equality holds because both sides constitute star homomorphisms which agree on `f = id` since
+  `a = b - c`. -/
+  /- `a`, `b`, `-c` are selfadjoint. -/
+  have hb' : IsSelfAdjoint b := .of_nonneg hb
+  have hc' : IsSelfAdjoint (-c) := .neg <| .of_nonneg hc
+  have ha : IsSelfAdjoint a := habc ▸ hb'.sub <| .of_nonneg hc
+  /- It suffices to show `b = a⁺` since `a⁺ - a⁻ = a = b - c` -/
+  rw [and_iff_left_of_imp ?of_b_eq]
+  case of_b_eq =>
+    rw [← posPart_sub_negPart a] at habc
+    rintro rfl
+    linear_combination (norm := abel1) habc
+  /- `s := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)` is compact and each of these sets are subsets of `s`.
+  Moreover, `0 ∈ s`. -/
+  let s := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
+  have hs : CompactSpace s := by
+    refine isCompact_iff_compactSpace.mp <| (IsCompact.union ?_ ?_).union ?_
+    all_goals exact isCompact_quasispectrum _
+  obtain ⟨has, hbs, hcs⟩ : σₙ ℝ a ⊆ s ∧ σₙ ℝ b ⊆ s ∧ σₙ ℝ (-c) ⊆ s := by
+    refine ⟨?_, ?_, ?_⟩; all_goals intro; aesop
+  let _ : Zero s := ⟨0, by aesop⟩
+  have s0 : (0 : s) = (0 : ℝ) := rfl
+  /- The continuous functional calculi for functions `f g : C(s, ℝ)₀` applied to `b` and `(-c)`
+  are orthogonal (i.e., the product is always zero). -/
+  have mul₁ (f g : C(s, ℝ)₀) :
+      (cfcₙHomSuperset hb' hbs f) * (cfcₙHomSuperset hc' hcs g) = 0 := by
+    refine f.nonUnitalStarAlgHom_apply_mul_eq_zero s0 _ _ ?id ?star_id
+      (cfcₙHomSuperset_continuous hb' hbs)
+    case' star_id => rw [star_trivial]
+    all_goals
+      refine g.mul_nonUnitalStarAlgHom_apply_eq_zero s0 _ _ ?_ ?_
+        (cfcₙHomSuperset_continuous hc' hcs)
+      all_goals simp only [star_trivial, cfcₙHomSuperset_id' hb' hbs, cfcₙHomSuperset_id' hc' hcs,
+        mul_neg, hbc, neg_zero]
+  have mul₂ (f g : C(s, ℝ)₀) : (cfcₙHomSuperset hc' hcs f) * (cfcₙHomSuperset hb' hbs g) = 0 := by
+    simpa only [star_mul, star_zero, ← map_star, star_trivial] using congr(star $(mul₁ g f))
+  /- `fun f ↦ cfcₙ f b + cfcₙ f (-c)` defines a star homomorphism `ψ : C(s, ℝ)₀ →⋆ₙₐ[ℝ] A` which
+  agrees with the star homomorphism `cfcₙ · a : C(s, ℝ)₀ →⋆ₙₐ[ℝ] A` since
+  `cfcₙ id a = a = b - c = cfcₙ id b + cfcₙ id (-c)`. -/
+  let ψ : C(s, ℝ)₀ →⋆ₙₐ[ℝ] A :=
+    { (cfcₙHomSuperset hb' hbs : C(s, ℝ)₀ →ₗ[ℝ] A) + (cfcₙHomSuperset hc' hcs : C(s, ℝ)₀ →ₗ[ℝ] A)
+        with
+      toFun := cfcₙHomSuperset hb' hbs + cfcₙHomSuperset hc' hcs
+      map_zero' := by simp [-cfcₙHomSuperset_apply]
+      map_mul' := fun f g ↦ by
+        simp only [Pi.add_apply, map_mul, mul_add, add_mul, mul₂, add_zero, mul₁, zero_add]
+      map_star' := fun f ↦ by simp [← map_star] }
+  have key : (cfcₙHomSuperset ha has) = ψ :=
+    UniqueNonUnitalContinuousFunctionalCalculus.eq_of_continuous_of_map_id s rfl
+    (cfcₙHomSuperset ha has) ψ (cfcₙHomSuperset_continuous ha has)
+    ((cfcₙHomSuperset_continuous hb' hbs).add (cfcₙHomSuperset_continuous hc' hcs))
+    (by simpa [ψ, -cfcₙHomSuperset_apply, cfcₙHomSuperset_id, sub_eq_add_neg] using habc)
+  /- Applying the equality of star homomorphisms to the function `(·⁺ : ℝ → ℝ)` we find that
+  `b = cfcₙ id b + cfcₙ 0 (-c) = cfcₙ (·⁺) b - cfcₙ (·⁺) (-c) = cfcₙ (·⁺) a = a⁺`, where the
+  second equality follows because these functions are equal on the spectra of `b` and `-c`,
+  respectively, since `0 ≤ b` and `-c ≤ 0`. -/
+  let f : C(s, ℝ)₀ := ⟨⟨(·⁺), by fun_prop⟩, by simp [s0]⟩
+  replace key := congr($key f)
+  simp only [cfcₙHomSuperset_apply, NonUnitalStarAlgHom.coe_mk', NonUnitalAlgHom.coe_mk, ψ,
+    Pi.add_apply, cfcₙHom_eq_cfcₙ_extend (·⁺)] at key
+  calc
+    b = cfcₙ (id : ℝ → ℝ) b + cfcₙ (0 : ℝ → ℝ) (-c) := by simp [cfcₙ_id ℝ b]
+    _ = _ := by
+      congr! 1
+      all_goals
+        refine cfcₙ_congr fun x hx ↦ Eq.symm ?_
+        lift x to σₙ ℝ _ using hx
+        simp only [Subtype.val_injective.extend_apply, comp_apply, coe_mk, ContinuousMap.coe_mk,
+          Subtype.map_coe, id_eq, posPart_eq_self, f, Pi.zero_apply, posPart_eq_zero]
+      · exact quasispectrum_nonneg_of_nonneg b hb x.val x.property
+      · obtain ⟨x, hx⟩ := x
+        simp only [← neg_nonneg]
+        rw [Unitization.quasispectrum_eq_spectrum_inr ℝ (-c), Unitization.inr_neg,
+          ← spectrum.neg_eq, Set.mem_neg, ← Unitization.quasispectrum_eq_spectrum_inr ℝ c]
+          at hx
+        exact quasispectrum_nonneg_of_nonneg c hc _ hx
+    _ = _ := key.symm
+    _ = a⁺ := by
+      refine cfcₙ_congr fun x hx ↦ ?_
+      lift x to σₙ ℝ a using hx
+      simp [Subtype.val_injective.extend_apply, f]
+
 end CFC

Mathlib/Analysis/CStarAlgebra/Spectrum.lean

@@ -86,6 +86,16 @@ theorem spectrum.subset_circle_of_unitary {u : E} (h : u ∈ unitary E) :
 
 end UnitarySpectrum
 
+section Quasispectrum
+
+open scoped NNReal in
+lemma CStarAlgebra.le_nnnorm_of_mem_quasispectrum {A : Type*} [NonUnitalCStarAlgebra A]
+    {a : A} {x : ℝ≥0} (hx : x ∈ quasispectrum ℝ≥0 a) : x ≤ ‖a‖₊ := by
+  rw [Unitization.quasispectrum_eq_spectrum_inr' ℝ≥0 ℂ] at hx
+  simpa [Unitization.nnnorm_inr] using spectrum.le_nnnorm_of_mem hx
+
+end Quasispectrum
+
 section ComplexScalars
 
 open Complex