diff --git a/Mathlib/Algebra/Star/BigOperators.lean b/Mathlib/Algebra/Star/BigOperators.lean
index 2887fdf49930f7..eb273c10b5b329 100644
--- a/Mathlib/Algebra/Star/BigOperators.lean
+++ b/Mathlib/Algebra/Star/BigOperators.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.BigOperators.Finsupp.Basic
 public import Mathlib.Algebra.Star.SelfAdjoint
+public import Mathlib.Tactic.ContinuousFunctionalCalculus
 
 /-! # Big-operators lemmas about `star` algebraic operations
 
@@ -26,6 +27,7 @@ theorem star_prod [CommMonoid R] [StarMul R] {α : Type*} (s : Finset α) (f : 
 theorem star_sum [AddCommMonoid R] [StarAddMonoid R] {α : Type*} (s : Finset α) (f : α → R) :
     star (∑ x ∈ s, f x) = ∑ x ∈ s, star (f x) := map_sum (starAddEquiv : R ≃+ R) _ _
 
+@[aesop safe apply (rule_sets := [CStarAlgebra])]
 theorem isSelfAdjoint_sum {ι : Type*} [AddCommMonoid R] [StarAddMonoid R] (s : Finset ι)
     {x : ι → R} (h : ∀ i ∈ s, IsSelfAdjoint (x i)) : IsSelfAdjoint (∑ i ∈ s, x i) := by
   simpa [IsSelfAdjoint, star_sum] using Finset.sum_congr rfl fun _ hi => h _ hi
diff --git a/Mathlib/Algebra/Star/SelfAdjoint.lean b/Mathlib/Algebra/Star/SelfAdjoint.lean
index 4e427b6f33b357..d7519677418462 100644
--- a/Mathlib/Algebra/Star/SelfAdjoint.lean
+++ b/Mathlib/Algebra/Star/SelfAdjoint.lean
@@ -672,6 +672,12 @@ instance IsStarNormal.one_sub [NonAssocRing R] [StarRing R] {a : R}
     [ha : IsStarNormal a] : IsStarNormal (1 - a) :=
   Commute.one_left (star a) |>.isStarNormal_sub
 
+lemma IsSelfAdjoint.commute_of_mul_eq_zero [NonUnitalNonAssocRing R] [StarRing R]
+    {a b : R} (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) (hab : a * b = 0) :
+    Commute a b := by
+  have : b * a = 0 := by simpa [ha.star_eq, hb.star_eq] using congr(star $hab)
+  grind [commute_iff_eq]
+
 namespace Pi
 variable {ι : Type*} {α : ι → Type*} [∀ i, Star (α i)] {f : ∀ i, α i}
 
diff --git a/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean b/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean
index e540d5903674b8..47d659a93d1161 100644
--- a/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean
+++ b/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean
@@ -129,6 +129,8 @@ end ComplexBanachAlgebra
 
 section ComplexCStarAlgebra
 
+section Commutative
+
 variable {A : Type*} [CommCStarAlgebra A]
 
 theorem gelfandTransform_map_star (a : A) :
@@ -192,6 +194,124 @@ noncomputable def gelfandStarTransform : A ≃⋆ₐ[ℂ] C(characterSpace ℂ A
       { gelfandTransform ℂ A with map_star' := fun x => gelfandTransform_map_star x })
     (gelfandTransform_bijective A)
 
+end Commutative
+
+namespace CommCStarAlgebra
+
+variable {A : Type*} [NonUnitalCommCStarAlgebra A] {a b : A}
+
+open scoped CStarAlgebra in
+open Unitization in
+lemma norm_add_eq_max (h : a * b = 0) : ‖a + b‖ = max ‖a‖ ‖b‖ := by
+  let f := gelfandStarTransform A⁺¹ ∘ inrNonUnitalAlgHom ℂ A
+  have hf : Isometry f := gelfandTransform_isometry _ |>.comp isometry_inr
+  simp_rw [← hf.norm_map_of_map_zero (by simp [f]), show f (a + b) = f a + f b by simp [f]]
+  exact ContinuousMap.norm_add_eq_max <| by simpa [f] using congr(f $h)
+
+lemma nnnorm_add_eq_max (h : a * b = 0) : ‖a + b‖₊ = max ‖a‖₊ ‖b‖₊ :=
+  NNReal.eq <| norm_add_eq_max h
+
+lemma norm_sub_eq_max (h : a * b = 0) : ‖a - b‖ = max ‖a‖ ‖b‖ := by
+  simpa [sub_eq_add_neg] using norm_add_eq_max (a := a) (b := -b) (by simpa)
+
+lemma nnnorm_sub_eq_max (h : a * b = 0) : ‖a - b‖₊ = max ‖a‖₊ ‖b‖₊ :=
+  NNReal.eq <| norm_sub_eq_max h
+
+open scoped Function in
+lemma nnnorm_sum_eq_sup {ι : Type*} {f : ι → A} (s : Finset ι) (h0 : Pairwise ((· * · = 0) on f)) :
+    ‖∑ i ∈ s, f i‖₊ = s.sup (‖f ·‖₊) := by
+  classical
+  induction s using Finset.induction with
+  | empty => simp
+  | insert j s hj ih =>
+    suffices f j * ∑ i ∈ s, f i = 0 by
+      simp_all only [not_false_eq_true, Finset.sum_insert, Finset.sup_insert]
+      simpa [← ih] using nnnorm_add_eq_max this
+    simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h0 (by grind)
+
+end CommCStarAlgebra
+
+section NonUnital
+
+variable {A : Type*} [NonUnitalCStarAlgebra A] {a b : A}
+
+namespace IsStarNormal
+
+open scoped IsMulCommutative in
+open NonUnitalStarAlgebra NonUnitalStarSubalgebra in
+lemma norm_add_eq_max (ha : IsStarNormal a) (hb : IsStarNormal b)
+    (hab₁ : Commute a b) (hab₂ : Commute a (star b)) (hab : a * b = 0) :
+    ‖a + b‖ = max ‖a‖ ‖b‖ := by
+  /- Since `a` and `b` are normal, commute, and commute with the `star` of the other,
+  the C⋆-subalgebra generated by `a` and `b` is commutative, and the conclusion follows from the
+  corresponding result for commutative C⋆-algebras. -/
+  -- TODO: once #36418 is merged, simplify the following using `IsMulCommutative`.
+  let S : NonUnitalStarSubalgebra ℂ A := (adjoin ℂ {a, b}).topologicalClosure
+  have hS : IsClosed (S : Set A) := (adjoin ℂ {a, b}).isClosed_topologicalClosure
+  have hab₃ : Commute (star a) b := by simpa [commute_star_comm]
+  have : IsMulCommutative (adjoin ℂ {a, b}) :=
+    isMulCommutative_adjoin ℂ (by grind) (by grind [commute_star_comm])
+  let _ : NonUnitalCommRing S := (adjoin ℂ {a, b}).nonUnitalCommRingTopologicalClosure mul_comm
+  let _ : NonUnitalCommCStarAlgebra S := { }
+  refine CommCStarAlgebra.norm_add_eq_max (A := S) (a := ⟨a, ?_⟩) (b := ⟨b, ?_⟩) (by ext; simpa)
+  all_goals apply le_topologicalClosure; aesop
+
+lemma nnnorm_add_eq_max (ha : IsStarNormal a) (hb : IsStarNormal b)
+    (hab₁ : Commute a b) (hab₂ : Commute a (star b)) (hab : a * b = 0) :
+    ‖a + b‖₊ = max ‖a‖₊ ‖b‖₊ :=
+  NNReal.eq <| ha.norm_add_eq_max hb hab₁ hab₂ hab
+
+lemma norm_sub_eq_max (ha : IsStarNormal a) (hb : IsStarNormal b)
+    (hab₁ : Commute a b) (hab₂ : Commute a (star b)) (hab : a * b = 0) :
+    ‖a - b‖ = max ‖a‖ ‖b‖ := by
+  simpa [sub_eq_add_neg] using
+    ha.norm_add_eq_max hb.neg hab₁.neg_right (by simpa using hab₂) (by simpa)
+
+lemma nnnorm_sub_eq_max (ha : IsStarNormal a) (hb : IsStarNormal b)
+    (hab₁ : Commute a b) (hab₂ : Commute a (star b)) (hab : a * b = 0) :
+    ‖a - b‖₊ = max ‖a‖₊ ‖b‖₊ :=
+  NNReal.eq <| ha.norm_sub_eq_max hb hab₁ hab₂ hab
+
+end IsStarNormal
+
+namespace IsSelfAdjoint
+
+open NonUnitalStarAlgebra in
+lemma norm_add_eq_max (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) (hab : a * b = 0) :
+    ‖a + b‖ = max ‖a‖ ‖b‖ :=
+  ha.isStarNormal.norm_add_eq_max hb.isStarNormal (by grind [commute_of_mul_eq_zero])
+    (by grind [commute_of_mul_eq_zero, hb.star_eq]) hab
+
+lemma nnnorm_add_eq_max (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) (hab : a * b = 0) :
+    ‖a + b‖₊ = max ‖a‖₊ ‖b‖₊ :=
+  NNReal.eq <| ha.norm_add_eq_max hb hab
+
+lemma norm_sub_eq_max (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) (hab : a * b = 0) :
+    ‖a - b‖ = max ‖a‖ ‖b‖ := by
+  simpa [sub_eq_add_neg] using ha.norm_add_eq_max hb.neg (by simpa)
+
+lemma nnnorm_sub_eq_max (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) (hab : a * b = 0) :
+    ‖a - b‖₊ = max ‖a‖₊ ‖b‖₊ :=
+  NNReal.eq <| ha.norm_sub_eq_max hb hab
+
+open scoped Function in
+lemma nnnorm_sum_eq_sup {ι : Type*} {f : ι → A} (s : Finset ι)
+    (h : ∀ i ∈ s, IsSelfAdjoint (f i)) (h0 : Pairwise ((· * · = 0) on f)) :
+    ‖∑ i ∈ s, f i‖₊ = s.sup (‖f ·‖₊) := by
+  classical
+  induction s using Finset.induction with
+  | empty => simp
+  | insert j s hj ih =>
+    suffices f j * ∑ i ∈ s, f i = 0 by
+      simp_all only [Finset.mem_insert, or_true, implies_true, forall_const, forall_eq_or_imp,
+        not_false_eq_true, Finset.sum_insert, Finset.sup_insert]
+      simpa [← ih] using h.1.nnnorm_add_eq_max (by cfc_tac) this
+    simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h0 (by grind)
+
+end IsSelfAdjoint
+
+end NonUnital
+
 end ComplexCStarAlgebra
 
 section Functoriality