From b99310d1f94464a1c69392c1017df16859e9bd70 Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Mon, 2 Mar 2026 18:36:57 +0000
Subject: [PATCH 01/20] IsStarProjection.conjugatE_of_nonneg_of_le

Co-authored-by: Jon Bannon <59937998+JonBannon@users.noreply.github.com>
---
 .../ContinuousFunctionalCalculus/Order.lean   | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
index ff56f4cf8b1f0d..0398fb183563d4 100644
--- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
+++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
@@ -106,6 +106,8 @@ lemma inr_nonneg_iff {a : A} : 0 ≤ (a : A⁺¹) ↔ 0 ≤ a := by
     · exact isSelfAdjoint_inr (R := ℂ) |>.mp <| .of_nonneg h
     · exact .of_nonneg h
 
+alias ⟨_root_.LE.le.of_inr, _root_.LE.le.inr⟩ := Unitization.inr_nonneg_iff
+
 lemma nnreal_cfcₙ_eq_cfc_inr (a : A) (f : ℝ≥0 → ℝ≥0)
     (hf₀ : f 0 = 0 := by cfc_zero_tac) : cfcₙ f a = cfc f (a : A⁺¹) :=
   cfcₙ_eq_cfc_inr inr_nonneg_iff ..
@@ -497,6 +499,23 @@ end Icc
 
 end CStarAlgebra
 
+open CStarAlgebra Unitization CFC in
+lemma IsStarProjection.mul_right_eq_self_of_nonneg_of_le {a e : A} (he : IsStarProjection e)
+    (ha : 0 ≤ a) (hae : a ≤ e) : a * e = a := by
+  suffices sqrt a * (1 - e : A⁺¹) = 0 by
+    rw [mul_sub, sub_eq_zero, mul_one, ← inr_mul, inr_injective.eq_iff] at this
+    rw [nonneg_iff_eq_sqrt_mul_sqrt.mp ha, mul_assoc, ← this]
+  rw [← CStarRing.star_mul_self_eq_zero_iff, star_mul, (sqrt_nonneg a).inr.star_eq, mul_assoc,
+    ← mul_assoc ((sqrt a : A) : A⁺¹), ← inr_mul, ← nonneg_iff_eq_sqrt_mul_sqrt.mp ha, ← mul_assoc]
+  apply le_antisymm (le_of_le_of_eq (star_left_conjugate_le_conjugate
+    (inr_le_iff a e |>.mpr hae) _) _) (star_left_conjugate_nonneg (by simpa) _)
+  simp [mul_assoc, (he.inr (R := ℂ)).mul_one_sub_self]
+
+lemma IsStarProjection.conjugate_of_nonneg_of_le {a e : A} (he : IsStarProjection e)
+    (ha : 0 ≤ a) (hae : a ≤ e) : e * a * e = a := by
+  have := he.mul_right_eq_self_of_nonneg_of_le ha hae
+  rwa [mul_assoc, this, ← he.2, ← star_star a, ← star_mul, star_inj, ha.star_eq]
+
 end CStar_nonunital
 
 section Pow

From 8205b4f1a8ab18897758267ef3cc39e61bbf561d Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Thu, 5 Mar 2026 14:07:54 +0000
Subject: [PATCH 02/20] star proj iff extreme

---
 Mathlib/Analysis/CStarAlgebra/Extreme.lean | 53 ++++++++++++++++++++++
 1 file changed, 53 insertions(+)
 create mode 100644 Mathlib/Analysis/CStarAlgebra/Extreme.lean

diff --git a/Mathlib/Analysis/CStarAlgebra/Extreme.lean b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
new file mode 100644
index 00000000000000..0846779edfd05c
--- /dev/null
+++ b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2026 Monica Omar, Jireh Loreaux, Jon Bannon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Monica Omar, Jireh Loreaux, Jon Bannon
+-/
+module
+
+public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
+public import Mathlib.Analysis.Convex.Extreme
+
+/-! # Extreme points of the closed unit ball in C⋆-algebras
+
+This file contains results on the extreme points of the closed unit ball in (unital) C⋆-algebras. -/
+
+/-- The star projections in a non-unital C⋆-algebra are exactly the extreme points of
+the nonnegative closed unit ball. -/
+theorem isStarProjection_iff_mem_extremePoints_nonneg_and_mem_closedUnitBall
+    [PartialOrder A] [StarOrderedRing A] {e : A} :
+    IsStarProjection e ↔ e ∈ extremePoints ℝ {x : A | 0 ≤ x ∧ x ∈ closedBall 0 1} := by
+  simp only [mem_closedBall, dist_zero_right, mem_extremePoints_iff_left, mem_setOf_eq, and_imp]
+  refine ⟨fun he ↦ ⟨⟨he.nonneg, he.norm_le⟩,
+    fun a ha ha1 b hb hb1 ⟨t, s, h0t, h0s, hts, hlin⟩ ↦ ?_⟩, fun ⟨⟨h1, h2⟩, h3⟩ ↦ ?_⟩
+  · have : t • (e * ((1 - a : A⁺¹) * e)) + s • (e * ((1 - b) * e)) =
+        (t + s) • e - e * (t • a + s • b) * e := by
+      simp [smul_sub, sub_add_eq_add_sub, add_sub, ← add_smul, hts, sub_mul, mul_sub,
+        he.inr.isIdempotentElem.eq, mul_add, add_mul, sub_sub, mul_assoc]
+    have : ((t + s) • e - e * (t • a + s • b) * e : A⁺¹) = 0 := by
+      simp [← inr_smul, ← inr_add, ← inr_mul, hts, hlin, he.isIdempotentElem.eq]
+    have H {q : ℝ} {c : A} (hq : 0 < q) (h0c : 0 ≤ c) (hc1 : ‖c‖ ≤ 1) :
+        0 ≤ q • (e * ((1 - c : A⁺¹) * e)) := by
+      rw [← smul_zero q, smul_le_smul_iff_of_pos_left hq, ← mul_assoc]
+      exact he.inr.isSelfAdjoint.conjugate_nonneg (sub_nonneg_of_le <|
+        (norm_le_one_iff_of_nonneg (c : A⁺¹) (by simpa)).mp (by simpa [norm_inr]))
+    have := le_add_iff_nonneg_right (t • (e * ((1 - a : A⁺¹) * e))) |>.mpr (H h0s hb hb1)
+    have : e * ((1 - a : A⁺¹) * e) = 0 := by rw [← smul_eq_zero_iff_right h0t.ne']; grind
+    have := he.conjugate_of_nonneg_of_le (a := t • a) (by positivity)
+      (by simpa [hlin] using le_add_of_nonneg_right (a := t • a) (by positivity : 0 ≤ s • b))
+    rw [mul_smul_comm, smul_mul_assoc] at this
+    have h : e * (e - a * e) = 0 := by rw [← (inr_injective (R := ℂ)).eq_iff]; simpa [← one_sub_mul]
+    rwa [mul_sub, ← mul_assoc, he.isIdempotentElem, h0t.ne'.isUnit.smul_left_cancel.mp this,
+      sub_eq_zero, eq_comm] at h
+  · have := calc
+      0 ≤ (e : A⁺¹) * (2 - e) := by
+        have : (e : A⁺¹) ≤ 1 := norm_le_one_iff_of_nonneg _ (by simpa) |>.mp (by simpa [norm_inr])
+        apply Commute.mul_nonneg (by simpa) (by grw [sub_nonneg, this, one_le_two])
+        simp [commute_iff_eq, mul_sub, sub_mul, mul_two, two_mul]
+      _ = (((2 : ℝ) • e - e * e : A) : A⁺¹) := by simp [mul_sub, two_smul, mul_two]
+    refine ⟨h3 _ (Commute.mul_nonneg h1 h1 rfl) ?_ ((2 : ℝ) • e - e * e) this.of_inr ?_
+      ⟨2⁻¹, 2⁻¹, by simp [smul_sub, ← one_div, smul_smul]⟩, h1.isSelfAdjoint⟩
+    · grw [norm_mul_le, h2, one_mul]
+    · rw [← norm_inr (𝕜 := ℂ), norm_le_one_iff_of_nonneg _ this, ← sub_nonneg]
+      calc 0 ≤ star (1 - e : A⁺¹) * (1 - e) := star_mul_self_nonneg _
+        _ = _ := by simp [LE.le.star_eq, h1, mul_sub, sub_mul, two_smul, sub_sub, add_sub]

From c0490672ee4a9cf7b8dd2b1f0ac423a80c428b45 Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Thu, 5 Mar 2026 14:14:06 +0000
Subject: [PATCH 03/20] variables

---
 Mathlib/Analysis/CStarAlgebra/Extreme.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Mathlib/Analysis/CStarAlgebra/Extreme.lean b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
index 0846779edfd05c..e59592cd934289 100644
--- a/Mathlib/Analysis/CStarAlgebra/Extreme.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
@@ -12,6 +12,8 @@ public import Mathlib.Analysis.Convex.Extreme
 
 This file contains results on the extreme points of the closed unit ball in (unital) C⋆-algebras. -/
 
+variable {A : Type*} [NonUnitalCStarAlgebra A]
+
 /-- The star projections in a non-unital C⋆-algebra are exactly the extreme points of
 the nonnegative closed unit ball. -/
 theorem isStarProjection_iff_mem_extremePoints_nonneg_and_mem_closedUnitBall

From 042c2be678c26c2e5ba371926bfb9981fc42da4d Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Thu, 5 Mar 2026 14:19:57 +0000
Subject: [PATCH 04/20] mk_all

---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index cd8c367a616145..2088b6a349d4bd 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1586,6 +1586,7 @@ public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary
 public import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap
 public import Mathlib.Analysis.CStarAlgebra.ContinuousMap
 public import Mathlib.Analysis.CStarAlgebra.Exponential
+public import Mathlib.Analysis.CStarAlgebra.Extreme
 public import Mathlib.Analysis.CStarAlgebra.GelfandDuality
 public import Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
 public import Mathlib.Analysis.CStarAlgebra.Hom

From 8c367be4b8ab93c6fc00adcd070a95836de76e81 Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Thu, 5 Mar 2026 14:29:15 +0000
Subject: [PATCH 05/20] fix

---
 Mathlib/Analysis/CStarAlgebra/Extreme.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/Mathlib/Analysis/CStarAlgebra/Extreme.lean b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
index e59592cd934289..1234b2e55d2aa4 100644
--- a/Mathlib/Analysis/CStarAlgebra/Extreme.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
@@ -12,6 +12,12 @@ public import Mathlib.Analysis.Convex.Extreme
 
 This file contains results on the extreme points of the closed unit ball in (unital) C⋆-algebras. -/
 
+public section
+
+set_option backward.isDefEq.respectTransparency false
+
+open Set Metric CFC CStarAlgebra Unitization
+
 variable {A : Type*} [NonUnitalCStarAlgebra A]
 
 /-- The star projections in a non-unital C⋆-algebra are exactly the extreme points of

From e5a66e725b04fe92dbf081bd48ab31ce229ffec9 Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Sat, 7 Mar 2026 18:07:33 +0000
Subject: [PATCH 06/20] part 1

---
 .../Isometric.lean                            |   3 +
 Mathlib/Analysis/CStarAlgebra/Extreme.lean    | 108 ++++++++++++++++++
 Mathlib/Analysis/Convex/Extreme.lean          |   4 +
 Mathlib/LinearAlgebra/Complex/Module.lean     |  70 ++++++++++++
 4 files changed, 185 insertions(+)

diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
index 0e7863c0d4380a..7d7e44334dc0dc 100644
--- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
+++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
@@ -344,6 +344,9 @@ lemma norm_quasispectrum_le (a : A) ⦃x : 𝕜⦄ (hx : x ∈ σₙ 𝕜 a) (ha
     ‖x‖ ≤ ‖a‖ := by
   simpa only [cfcₙ_id 𝕜 a] using norm_apply_le_norm_cfcₙ (id : 𝕜 → 𝕜) a hx
 
+alias _root_.quasispectrum.norm_le_norm_of_mem :=
+  NonUnitalIsometricContinuousFunctionalCalculus.norm_quasispectrum_le
+
 lemma isGreatest_nnnorm_quasispectrum (a : A) (ha : p a := by cfc_tac) :
     IsGreatest ((‖·‖₊) '' σₙ 𝕜 a) ‖a‖₊ := by
   simpa only [cfcₙ_id 𝕜 a] using IsGreatest.nnnorm_cfcₙ (id : 𝕜 → 𝕜) a
diff --git a/Mathlib/Analysis/CStarAlgebra/Extreme.lean b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
index 1234b2e55d2aa4..f51c26dc908266 100644
--- a/Mathlib/Analysis/CStarAlgebra/Extreme.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
@@ -18,8 +18,116 @@ set_option backward.isDefEq.respectTransparency false
 
 open Set Metric CFC CStarAlgebra Unitization
 
+@[simp] lemma Set.extremePoints_Icc {a b : ℝ} (hab : a ≤ b) :
+    Set.extremePoints ℝ (Icc a b) = {a, b} := by
+  ext x
+  rw [convex_Icc .. |>.mem_extremePoints_iff_convex_diff]
+  constructor
+  · intro ⟨h₁, h₂⟩
+    suffices x ∉ Ioo a b by grind
+    intro hx
+    have := h₂.isPreconnected.Icc_subset (a := a) (b := b) (by grind) (by grind)
+    grind
+  · rintro (rfl | rfl)
+    · simpa using ⟨hab, convex_Ioc ..⟩
+    · simpa using ⟨hab, convex_Ico ..⟩
+
+open scoped ComplexStarModule in
+lemma CStarAlgebra.one_mem_extremePoints_closedUnitBall {A : Type*} [CStarAlgebra A] :
+    1 ∈ extremePoints ℝ (closedBall (0 : A) 1) := by
+  nontriviality A
+  /- Suppose that `1` is a convex combination of `x` and `y`. Then, since `1` is self
+  adjoint, it is also a combination of their real and imaginary parts, which we
+  call `a` and `b`. Moreover, `b` is a linear polynomial in the variable `a`, so we
+  may write it as the continuous functional calculus applied to the appropriate
+  function of `a`. -/
+  refine ⟨by simp, fun x hx y hy hxy ↦ ?_⟩
+  let +nondep (eq := ha') a : A := ℜ x
+  let +nondep (eq := hb') b : A := ℜ y
+  simp only [mem_closedBall, dist_zero_right] at hx hy
+  have ha : ‖a‖ ≤ 1 := by simpa [ha'] using realPart.norm_le _ |>.trans hx
+  have hb : ‖b‖ ≤ 1 := by simpa [hb'] using realPart.norm_le _ |>.trans hy
+  obtain ⟨c₁, hc₁, c₂, hc₂, hc, hcab⟩ := by simpa [openSegment] using hxy
+  replace hcab : c₁ • a + c₂ • b = 1 := by simpa [ha', hb'] using congr((ℜ $hcab : A))
+  have : b = c₂⁻¹ • 1 - c₂⁻¹ • c₁ • a := by
+    simpa [inv_smul_smul₀ hc₂.ne', eq_sub_iff_add_eq'] using congr(c₂⁻¹ • $hcab)
+  rw [this, ← cfc_id' ℝ a, ← cfc_one ℝ a, ← cfc_smul .., ← cfc_smul .., ← cfc_smul ..,
+    ← cfc_sub .., ← cfc_smul .., ← cfc_add .., cfc_eq_cfc_iff_eqOn] at hcab
+  /- By passing to functions, we will show that `a = 1`. In particular, the constant
+  function `1` on the `ℝ`-spectrum of `a` is a convex combination of functions (one of
+  which is the identity) which are bounded in absolute value by `1`. Since `1 : ℝ` is
+  extreme in `Icc (-1) 1`, we conclude that these functions must be `1` on the
+  spectrum of `a`. -/
+  obtain rfl : a = 1 := by
+    refine CFC.eq_one_of_spectrum_subset_one (R := ℝ) a fun r hr ↦ ?_
+    have h1_mem : (1 : ℝ) ∈ openSegment ℝ r (c₂⁻¹ - c₂⁻¹ * c₁ * r) :=
+      ⟨c₁, c₂, hc₁, hc₂, hc, by simpa [mul_assoc] using hcab hr⟩
+    have key : (1 : ℝ) ∈ extremePoints ℝ (Icc (-1) 1) := by simp
+    simp only [mem_singleton_iff]
+    refine mem_extremePoints_iff_left.mp key |>.2 _ ?_ _ ?_ h1_mem
+    · simpa [abs_le] using (spectrum.norm_le_norm_of_mem hr).trans ha
+    · suffices c₂⁻¹ - c₂⁻¹ * c₁ * r ∈ spectrum ℝ b by
+        simpa [abs_le] using (spectrum.norm_le_norm_of_mem this).trans hb
+      rw [this, ← Algebra.algebraMap_eq_smul_one, sub_eq_add_neg, sub_eq_add_neg]
+      rwa [add_comm c₂⁻¹, spectrum.add_mem_add_iff, ← spectrum.neg_eq, Set.neg_mem_neg, smul_smul,
+        spectrum.smul_eq_smul _ _ (nonempty_of_mem hr), ← smul_eq_mul _ r,
+        Set.smul_mem_smul_set_iff₀ (by positivity)]
+  /- Since `ℜ x = a = 1`, so too we conclude `ℜ y = b = 1`. -/
+  obtain rfl : b = 1 := by
+    simpa [← smul_assoc, ← sub_smul, (sub_eq_iff_eq_add.mpr hc.symm).symm, mul_sub, hc₂.ne']
+  clear this hb ha hcab hb' hc hc₂ hc₁ c₁ c₂ hy hxy y
+  /- Since `ℜ x = 1`, the real and imaginary parts of `x` commute, so `x` is normal. It
+  then suffices to show that `ℑ x = 0`. -/
+  have hx' : IsStarNormal x := by simp [isStarNormal_iff_commute_realPart_imaginaryPart, ← ha']
+  suffices (ℑ x : A) = 0 by rw [← realPart_add_I_smul_imaginaryPart x, ← ha', this]; simp
+  let := spectralOrder A
+  let := spectralOrderedRing A
+  /- Note that `‖1 + (ℑ x) ^ 2‖ = ‖(ℜ x) ^ 2 + (ℑ x) ^ 2‖ = ‖star x * x‖ = ‖x‖ ^ 2 ≤ 1`.
+  Therefore, `1 + (ℑ x) ^ 2 ≤ 1`, so `(ℑ x) ^ 2 ≤ 0`. Since `(ℑ x) ^ 2` is clearly nonnegative,
+  we conclude that it is zero, and hence so also `ℑ x = 0`, as desired. -/
+  rw [← sq_le_one_iff₀ (by positivity), sq, ← CStarRing.norm_star_mul_self,
+    star_mul_self_eq_realPart_sq_add_imaginaryPart_sq, ← ha', mul_one, ← sq,
+    norm_le_one_iff_of_nonneg _ (add_nonneg zero_le_one (ℑ x).2.sq_nonneg)] at hx
+  rw [← norm_eq_zero, ← sq_eq_zero_iff, ← IsSelfAdjoint.norm_mul_self (ℑ x).2, ← sq, norm_eq_zero]
+  exact le_antisymm (by simpa using hx) (ℑ x).2.sq_nonneg
+
 variable {A : Type*} [NonUnitalCStarAlgebra A]
 
+theorem star_self_conjugate_eq_self_of_mem_extremePoints_closedUnitBall {a : A}
+    (ha : a ∈ extremePoints ℝ (closedBall 0 1)) : a * star a * a = a := by
+  let := spectralOrder A
+  let := spectralOrderedRing A
+  suffices a * abs a = a by rw [mul_assoc, ← abs_mul_abs, ← mul_assoc, this, this]
+  obtain ⟨ha, h⟩ := ha
+  simp only [mem_closedBall, dist_zero_right] at ha h
+  refine @h _ ?_ ((2 : ℝ) • a - a * abs a) ?_ ⟨2⁻¹, 2⁻¹, by simp [smul_sub, ← two_mul]⟩
+  · grw [norm_mul_le, norm_abs, ha, one_mul]
+  · calc
+      _ = ‖(2 : ℝ) • abs a - abs a * abs a‖ := by
+        simp_rw [← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _), sq, ← CStarRing.norm_star_mul_self]
+        simp only [star_sub, star_smul, star_mul, mul_sub, mul_smul_comm, sub_mul, smul_mul_assoc]
+        simp [abs_nonneg a |>.star_eq, mul_assoc, ← mul_assoc _ a, ← abs_mul_abs]
+      _ = ‖cfcₙ (fun x : ℝ ↦ 2 * x - x * x) (abs a)‖ := by
+        rw [cfcₙ_sub _ _, cfcₙ_const_mul _ _, cfcₙ_mul _ _, cfcₙ_id' ℝ (abs a)]
+      _ ≤ _ := norm_cfcₙ_le fun x hx ↦ by
+        have := x.le_norm_self.trans (by grw [quasispectrum.norm_le_norm_of_mem _ hx, norm_abs, ha])
+        rw [Real.norm_of_nonneg] <;> nlinarith [quasispectrum_nonneg_of_nonneg _ (by simp) _ hx]
+
+attribute [local grind .] IsSelfAdjoint.star_mul_self IsIdempotentElem IsSelfAdjoint.mul_star_self
+attribute [local grind] IsStarProjection
+
+/-- Every extreme point in the closed unit ball of a `NonUnitalCStarAlgebra` is a
+partial isometry (in other words, `star a * a` is a projection). -/
+theorem isStarProjection_star_mul_self_of_mem_extremePoints_closedUnitBall
+    {a : A} (ha : a ∈ extremePoints ℝ (closedBall 0 1)) : IsStarProjection (star a * a) := by
+  grind [star_self_conjugate_eq_self_of_mem_extremePoints_closedUnitBall ha]
+
+/-- Every extreme point in the closed unit ball of a `NonUnitalCStarAlgebra` is a
+partial isometry (in other words, `a * star a` is a projection). -/
+theorem isStarProjection_self_mul_star_of_mem_extremePoints_closedUnitBall
+    {a : A} (ha : a ∈ extremePoints ℝ (closedBall 0 1)) : IsStarProjection (a * star a) := by
+  grind [star_self_conjugate_eq_self_of_mem_extremePoints_closedUnitBall ha]
+
 /-- The star projections in a non-unital C⋆-algebra are exactly the extreme points of
 the nonnegative closed unit ball. -/
 theorem isStarProjection_iff_mem_extremePoints_nonneg_and_mem_closedUnitBall
diff --git a/Mathlib/Analysis/Convex/Extreme.lean b/Mathlib/Analysis/Convex/Extreme.lean
index f6dd736b7cec4a..ae6d59e33d3263 100644
--- a/Mathlib/Analysis/Convex/Extreme.lean
+++ b/Mathlib/Analysis/Convex/Extreme.lean
@@ -174,6 +174,10 @@ theorem IsExtreme.extremePoints_eq (hAB : IsExtreme 𝕜 A B) :
   Subset.antisymm (fun _ hx ↦ ⟨hx.1, hAB.extremePoints_subset_extremePoints hx⟩)
     (inter_extremePoints_subset_extremePoints_of_subset hAB.1)
 
+@[nontriviality]
+lemma Set.extremePoints_eq_self [Subsingleton E] (A : Set E) : Set.extremePoints 𝕜 A = A :=
+  subset_antisymm extremePoints_subset fun _ h ↦ ⟨h, fun _ _ _ _ _ ↦ Subsingleton.elim ..⟩
+
 end SMul
 
 section OrderedSemiring
diff --git a/Mathlib/LinearAlgebra/Complex/Module.lean b/Mathlib/LinearAlgebra/Complex/Module.lean
index 078026f7e78c75..5ad522bc7cf8ad 100644
--- a/Mathlib/LinearAlgebra/Complex/Module.lean
+++ b/Mathlib/LinearAlgebra/Complex/Module.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.Algebra.RestrictScalars
 public import Mathlib.Algebra.CharP.Invertible
+public import Mathlib.Algebra.Star.Unitary
 public import Mathlib.Data.Complex.Basic
 public import Mathlib.Data.Real.Star
 public import Mathlib.LinearAlgebra.Matrix.ToLin
@@ -524,4 +525,73 @@ lemma star_mul_self_add_self_mul_star {A : Type*} [NonUnitalNonAssocRing A] [Sta
         smul_mul_assoc]
       abel
 
+namespace ComplexStarModule
+
+variable {M : Type*} [AddCommGroup M] [StarAddMonoid M] [Module ℂ M] [StarModule ℂ M] {x y : M}
+
+lemma ext (h₁ : ℜ x = ℜ y) (h₂ : ℑ x = ℑ y) : x = y := by
+  rw [← realPart_add_I_smul_imaginaryPart x, ← realPart_add_I_smul_imaginaryPart y, h₁, h₂]
+
+lemma ext_iff : x = y ↔ ℜ x = ℜ y ∧ ℑ x = ℑ y := ⟨by grind, fun h ↦ ext h.1 h.2⟩
+
+end ComplexStarModule
+
+@[simp]
+theorem ker_imaginaryPart {E : Type*} [AddCommGroup E]
+    [Module ℂ E] [StarAddMonoid E] [StarModule ℂ E] :
+    imaginaryPart.ker = selfAdjoint.submodule ℝ E := by
+  ext x
+  simp [selfAdjoint.submodule, selfAdjoint.mem_iff, imaginaryPart, Subtype.ext_iff]
+  grind
+
+@[simp]
+lemma imaginaryPart_eq_zero_iff {A : Type*} [AddCommGroup A] [Module ℂ A]
+    [StarAddMonoid A] [StarModule ℂ A] {x : A} :
+    ℑ x = 0 ↔ IsSelfAdjoint x := by
+  simpa [-ker_imaginaryPart] using SetLike.ext_iff.mp ker_imaginaryPart x
+
+@[simp]
+lemma realPart_one {A : Type*} [Ring A] [StarRing A] [Module ℂ A] [StarModule ℂ A] :
+    ℜ (1 : A) = 1 := by
+  ext; simp [realPart_apply_coe, ← two_smul ℝ]
+
+open Complex in
+/-- An element in a non-unital star `ℂ`-algebra is normal if and only if its real and imaginary
+parts commute. -/
+lemma isStarNormal_iff_commute_realPart_imaginaryPart
+    {A : Type*} [NonUnitalNonAssocRing A] [StarRing A]
+    [Module ℂ A] [SMulCommClass ℂ A A] [IsScalarTower ℂ A A] [StarModule ℂ A]
+    {x : A} : IsStarNormal x ↔ Commute (ℜ x : A) (ℑ x : A) := by
+  conv_lhs => rw [isStarNormal_iff, ← realPart_add_I_smul_imaginaryPart x]
+  rw [commute_iff_eq]
+  simp only [star_add, selfAdjoint.star_val_eq, star_smul, Complex.star_def, Complex.conj_I,
+    neg_smul, ← sub_eq_add_neg, mul_add, sub_mul, smul_mul_assoc, mul_smul_comm, smul_sub,
+    smul_smul, Complex.I_mul_I, one_smul, sub_neg_eq_add, mul_sub, add_mul, smul_add]
+  rw [sub_eq_add_neg, add_assoc, add_sub_assoc, add_left_cancel_iff, ← sub_add,
+    ← add_assoc, add_right_cancel_iff, ← sub_eq_zero, sub_sub_eq_add_sub, add_assoc, ← two_nsmul,
+    add_comm, sub_eq_add_neg, add_assoc, ← two_nsmul, smul_neg, ← sub_eq_add_neg, sub_eq_zero]
+  refine ⟨fun h ↦ ?_, fun h ↦ congr(2 • I • $h)⟩
+  have := congr(I • (2⁻¹ : ℂ) • $h)
+  rw [← smul_one_smul ℂ 2 (I • (ℑ x * ℜ x : A)), ← smul_one_smul ℂ 2] at this
+  simpa [smul_smul]
+
+lemma star_mul_self_eq_realPart_sq_add_imaginaryPart_sq {A : Type*} [NonUnitalNonAssocRing A]
+    [StarRing A] [Module ℂ A] [SMulCommClass ℂ A A] [IsScalarTower ℂ A A] [StarModule ℂ A]
+    {x : A} [hx : IsStarNormal x] : star x * x = ℜ x * ℜ x + ℑ x * ℑ x := calc
+  star x * x = ℜ x * ℜ x + ℑ x * ℑ x + Complex.I • (ℜ x * ℑ x - ℑ x * ℜ x) := by
+    conv_lhs => rw [← realPart_add_I_smul_imaginaryPart x]
+    simp [add_mul, mul_add, smul_mul_assoc, mul_smul_comm, smul_smul, smul_sub]
+    grind
+  _ = _ := by simp [isStarNormal_iff_commute_realPart_imaginaryPart.mp hx |>.eq]
+
+lemma mem_unitary_iff_isStarNormal_and_realPart_sq_add_imaginaryPart_sq_eq_one {A : Type*} [Ring A]
+    [StarRing A] [Module ℂ A] [SMulCommClass ℂ A A] [IsScalarTower ℂ A A] [StarModule ℂ A] {x : A} :
+    x ∈ unitary A ↔ IsStarNormal x ∧ ℜ x ^ 2 + ℑ x ^ 2 = (1 : A) := by
+  rw [Unitary.mem_iff]
+  refine ⟨fun h ↦ ?_, fun ⟨hx, h⟩ ↦ ?_⟩
+  · have : IsStarNormal x := by simp [isStarNormal_iff, commute_iff_eq, h]
+    rw [star_mul_self_eq_realPart_sq_add_imaginaryPart_sq] at h
+    exact ⟨this, by simp [sq, h]⟩
+  · simp [← hx.star_comm_self.eq, star_mul_self_eq_realPart_sq_add_imaginaryPart_sq, ← sq, h]
+
 end RealImaginaryPart

From 0a6a8f6424db041182e6b7d142281ea3a632e3fb Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Sat, 7 Mar 2026 18:21:17 +0000
Subject: [PATCH 07/20] the rest

---
 .../CStarAlgebra/ApproximateUnit.lean         |  12 ++
 Mathlib/Analysis/CStarAlgebra/Extreme.lean    | 107 ++++++++++++++++++
 .../Analysis/CStarAlgebra/GelfandDuality.lean |  33 ++++++
 .../ContinuousMap/Bounded/Normed.lean         |  18 +++
 Mathlib/Topology/ContinuousMap/Compact.lean   |   5 +
 5 files changed, 175 insertions(+)

diff --git a/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean b/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean
index 0d6090ce9f5b06..5690a4f36c5aa3 100644
--- a/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean
+++ b/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean
@@ -163,6 +163,16 @@ lemma eventually_star_eq {l : Filter A} (hl : l.IsIncreasingApproximateUnit) :
     ∀ᶠ x in l, star x = x :=
   hl.eventually_isSelfAdjoint.mp <| .of_forall fun _ ↦ IsSelfAdjoint.star_eq
 
+omit [StarOrderedRing A] in
+lemma closedBall_mem {l : Filter A} (hl : l.IsIncreasingApproximateUnit) :
+    Metric.closedBall 0 1 ∈ l := by
+  simpa [Metric.closedBall] using hl.eventually_norm
+
+omit [StarOrderedRing A] in
+lemma nonneg_mem {l : Filter A} (hl : l.IsIncreasingApproximateUnit) :
+    {x | 0 ≤ x} ∈ l := by
+  simpa using hl.eventually_nonneg
+
 end Filter.IsIncreasingApproximateUnit
 
 namespace CStarAlgebra
@@ -330,4 +340,6 @@ lemma increasingApproximateUnit :
 
 end CStarAlgebra
 
+instance : (approximateUnit A).NeBot := (increasingApproximateUnit A).neBot
+
 end ApproximateUnit
diff --git a/Mathlib/Analysis/CStarAlgebra/Extreme.lean b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
index f51c26dc908266..2e896a92757357 100644
--- a/Mathlib/Analysis/CStarAlgebra/Extreme.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
 public import Mathlib.Analysis.Convex.Extreme
+public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
 
 /-! # Extreme points of the closed unit ball in C⋆-algebras
 
@@ -167,3 +168,109 @@ theorem isStarProjection_iff_mem_extremePoints_nonneg_and_mem_closedUnitBall
     · rw [← norm_inr (𝕜 := ℂ), norm_le_one_iff_of_nonneg _ this, ← sub_nonneg]
       calc 0 ≤ star (1 - e : A⁺¹) * (1 - e) := star_mul_self_nonneg _
         _ = _ := by simp [LE.le.star_eq, h1, mul_sub, sub_mul, two_smul, sub_sub, add_sub]
+
+/-- If `x` is an extreme point in the closed unit ball of a C⋆-algebra `A`,
+with initial projection `p = star x * x` and final projection `q = x * star x`,
+"`(1 - q) A (1 - p) = 0`". Note: This notation is an informal
+shorthand used in paper proofs to make them more transparent, but it is
+nonsense to refer to `1`, and the notation means that everything should be
+considered as fully expanded. This is reflected in the statement below.
+*The converse is Sakai 1.6.4.* -/
+private theorem eq_zero_of_eq_sub_of_mem_closedBall_of_mem_extremePoints_closedUnitBall
+    {x a b : A} (hx : x ∈ extremePoints ℝ (closedBall 0 1)) (ha : a ∈ closedBall 0 1)
+    (hb : a = b - b * (star x * x) - (x * star x) * b + (x * star x) * b * (star x * x)) :
+    a = 0 := by
+  have hP := isStarProjection_star_mul_self_of_mem_extremePoints_closedUnitBall hx
+  have hQ := isStarProjection_self_mul_star_of_mem_extremePoints_closedUnitBall hx
+  set p := star x * x with hp
+  /- Notice that `x = q * x * p`, and `star x = p * star x * q` formally yield
+  `star x * (1 - q) * b * (1 - p) = 0` with the above abusive notation. By substituting for `a` in
+  `‖star a * x * star x * a‖` and expanding, we obtain this, and its adjoint, rigorously. -/
+  have hxa : star x * a = 0 := by
+    rw [← norm_eq_zero, ← mul_self_eq_zero, ← CStarRing.norm_star_mul_self]
+    simp [hb, mul_add, mul_sub, add_mul, sub_mul]
+    grind
+  have hax : star a * x = 0 := by simpa [star_mul] using congr(star $hxa)
+  /- Similarly, guided by the formal `star a = (1 - p) * star b * (1 - q)`, we obtain
+  the following by substitution and expansion. -/
+  have hpa : p * (star a * a) = 0 := by
+    simp only [hb, mul_add, mul_sub, star_add, star_sub, star_mul, add_mul, sub_mul]
+    grind [star_star_mul x x]
+  -- The facts `hxa` and `hax` yield that cross terms vanish.
+  have : star (x + a) * (x + a) = p + star a * a := by simp [hp, mul_add, add_mul, hax, hxa]
+  -- This, the C⋆-identity and `hpa` obtain
+  have : ‖p + star a * a‖ = ‖x + a‖ * ‖x + a‖ := by rw [← this, CStarRing.norm_star_mul_self]
+  /- Since `p` and `star a * a` are self-adjoint
+  with product zero that the norm of their sum is the max of the norms of these contractions. -/
+  have hmax : ‖p + star a * a‖ ≤ 1 := by
+    rw [IsSelfAdjoint.star_mul_self x |>.norm_add_eq_max hpa (.star_mul_self a), sup_le_iff, hp]
+    simp only [CStarRing.norm_star_mul_self]
+    grw [mem_closedBall_zero_iff.mp hx.1, mem_closedBall_zero_iff.mp ha, one_mul, and_self]
+  have : ‖x + a‖ ≤ 1 := sq_le_one_iff₀ (by positivity) |>.mp <| by grind
+  /- Using `hxa` and `hax`, cross terms vanish and we have
+  `‖x - a‖ * ‖x - a‖ = ‖p + star a * a‖ ≤ 1`. -/
+  have : ‖x - a‖ ≤ 1 := sq_le_one_iff₀ (by positivity) |>.mp <| by
+    simp [sq, ← CStarRing.norm_star_mul_self, sub_mul, mul_sub, hax, hxa, ← hp, hmax]
+  exact add_eq_left.mp <| @hx.2 (x + a) (by simpa) (x - a) (by simpa)
+    ⟨2⁻¹, 2⁻¹, by simp [smul_add, smul_sub, ← add_smul, ← one_div]⟩
+
+open Filter Topology in
+/-- When `x` is an extreme point of the closed unit ball in an a priori non-unital C⋆-algebra,
+then `star x * x + x * star x - x * star x * star x * x` is a right identity.
+(See also `CStarAlgebra.ofExtremePtOne_mul` for the left identity.) -/
+theorem CStarAlgebra.mul_ofExtremePtOne {x : A} (hx : x ∈ extremePoints ℝ (closedBall 0 1))
+    (a : A) : a * (star x * x + x * star x - x * star x * (star x * x)) = a := by
+  let := spectralOrder A
+  let := spectralOrderedRing A
+  let u := approximateUnit A
+  let hu := increasingApproximateUnit A
+  let f (t : A) : A := t - t * (star x * x) - x * star x * t + x * star x * t * (star x * x)
+  have h (t : A) : f t = 0 := by
+    simpa using eq_zero_of_eq_sub_of_mem_closedBall_of_mem_extremePoints_closedUnitBall
+      hx (inv_norm_smul_mem_unitClosedBall (f t)) (b := ‖f t‖⁻¹ • t)
+      (by simp [← mul_assoc, smul_mul_assoc, mul_smul_comm, sub_sub, ← smul_sub, ← smul_add, f])
+  have h_tendsto : Tendsto (fun t ↦ a * f t) u
+      (𝓝 (a - a * (star x * x + x * star x - x * star x * (star x * x)))) := by
+    conv => enter [1, t]; simp only [f]; rw [sub_add, sub_sub, add_sub, mul_sub]
+    apply_rules [Tendsto.sub, Tendsto.add, hu.tendsto_mul_left, hu.tendsto_mul_right,
+      Tendsto.mul_const, Tendsto.const_mul]
+  simpa [h, sub_eq_zero, eq_comm (a := (0 : A)), eq_comm (a := a)] using h_tendsto
+
+@[simp]
+theorem star_mem_extremePoints_closedBall_zero_iff {A : Type*} [NonUnitalSeminormedRing A]
+    [StarRing A] [NormedStarGroup A] [Module ℝ A] [StarModule ℝ A] {x : A} (c : ℝ) :
+    star x ∈ extremePoints ℝ (closedBall 0 c) ↔ x ∈ extremePoints ℝ (closedBall 0 c) := by
+  suffices ∀ x : A, x ∈ extremePoints ℝ (closedBall 0 c) → star x ∈ extremePoints ℝ (closedBall 0 c)
+    from ⟨fun h ↦ star_star x ▸ this (star x) h, this x⟩
+  refine fun x hx ↦ ⟨by simpa using hx.1, fun y hy z hz ⟨α, β, hα, hβ, hαβ, hxyz⟩ ↦ ?_⟩
+  rw [eq_star_iff_eq_star, eq_comm] at hxyz ⊢
+  apply @hx.2 _ (by simpa using hy) (star z) (by simpa using hz) ⟨star α, star β, ?_⟩
+  simp [← hxyz, hα, hβ, hαβ]
+
+/-- When `x` is an extreme point of the closed unit ball in an a priori non-unital C⋆-algebra,
+then `star x * x + x * star x - x * star x * star x * x` is a left identity.
+(See also `CStarAlgebra.mul_ofExtremePtOne` for the right identity.) -/
+theorem CStarAlgebra.ofExtremePtOne_mul {x : A} (hx : x ∈ extremePoints ℝ (closedBall 0 1))
+    (a : A) : (star x * x + x * star x - x * star x * (star x * x)) * a = a := by
+  simpa [add_comm] using congr(star $(mul_ofExtremePtOne (x := star x) (by simpa) (star a)))
+
+/-- The ring structure given an extreme point of the closed unit ball on a non-unital
+C⋆-algebra. Only an implementation for `CStarAlgebra.ofExtremePt`. -/
+abbrev CStarAlgebra.ringOfExtremePt {x : A} (hx : x ∈ extremePoints ℝ (closedBall 0 1)) :
+    Ring A where
+  one := star x * x + x * star x - x * star x * (star x * x)
+  one_mul y := ofExtremePtOne_mul hx y
+  mul_one y := mul_ofExtremePtOne hx y
+
+lemma CStarAlgebra.ofExtremePt_one_def {x : A} (hx : x ∈ extremePoints ℝ (closedBall 0 1)) :
+    letI := CStarAlgebra.ringOfExtremePt hx
+    1 = star x * x + x * star x - x * star x * (star x * x) :=
+  rfl
+
+/-- Upgrade a non-unital C⋆-algebra to a unital C⋆-algebra, given there exists an
+extreme point of the closed unit ball. -/
+abbrev CStarAlgebra.ofExtremePt {x : A} (hx : x ∈ extremePoints ℝ (closedBall 0 1)) :
+    CStarAlgebra A where
+  __ := ‹NonUnitalCStarAlgebra A›
+  __ := ringOfExtremePt hx
+  __ := Algebra.ofModule smul_mul_assoc mul_smul_comm
diff --git a/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean b/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean
index 14950ace52e6ff..e1f01cc6671495 100644
--- a/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean
+++ b/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean
@@ -295,3 +295,36 @@ lemma WeakDual.CharacterSpace.homeoEval_naturality {X Y 𝕜 : Type*} [RCLike 
     (homeoEval Y 𝕜 : C(_, _)).comp f =
       (f.compStarAlgHom' 𝕜 𝕜 |> compContinuousMap).comp (homeoEval X 𝕜 : C(_, _)) :=
   rfl
+
+open scoped CStarAlgebra in
+open Unitization in
+lemma CommCStarAlgebra.norm_add_eq_max {A : Type*} [NonUnitalCommCStarAlgebra A]
+    {a b : A} (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)
+
+open NonUnitalStarAlgebra in
+lemma IsSelfAdjoint.norm_add_eq_max {A : Type*} [NonUnitalCStarAlgebra A]
+    {a b : A} (hab : a * b = 0) (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) :
+    ‖a + b‖ = max ‖a‖ ‖b‖ := by
+  let S : NonUnitalStarSubalgebra ℂ A := (adjoin ℂ {a, b}).topologicalClosure
+  have hS : IsClosed (S : Set A) := (adjoin ℂ {a, b}).isClosed_topologicalClosure
+  have hab' : a * b = b * a := by
+    rw [hab, eq_comm]; simpa [ha.star_eq, hb.star_eq] using congr(star $hab)
+  let _ : NonUnitalCommRing (adjoin ℂ {a, b}) :=
+    adjoinNonUnitalCommRingOfComm ℂ (by grind) (by grind [IsSelfAdjoint.star_eq])
+  let _ : NonUnitalCommRing S := (adjoin ℂ {a, b}).nonUnitalCommRingTopologicalClosure mul_comm
+  let _ : NonUnitalCommCStarAlgebra S := { }
+  let c : S := ⟨a, subset_closure <| subset_adjoin _ _ <| by grind⟩
+  let d : S := ⟨b, subset_closure <| subset_adjoin _ _ <| by grind⟩
+  exact CommCStarAlgebra.norm_add_eq_max (a := c) (b := d) (by ext; simpa)
+
+lemma IsSelfAdjoint.norm_sub_eq_max {A : Type*} [NonUnitalCStarAlgebra A]
+    {a b : A} (hab : a * b = 0) (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) :
+    ‖a - b‖ = max ‖a‖ ‖b‖ := by
+  rw [← sq_eq_sq₀ (by positivity) (by positivity)]
+  simp only [sq, ← ha.norm_add_eq_max hab hb, ← CStarRing.norm_star_mul_self]
+  have : b * a = 0 := by simpa [ha.star_eq, hb.star_eq] using congr(star $hab)
+  simp [sub_mul, mul_sub, hb.star_eq, ha.star_eq, hab, this, add_mul, mul_add]
diff --git a/Mathlib/Topology/ContinuousMap/Bounded/Normed.lean b/Mathlib/Topology/ContinuousMap/Bounded/Normed.lean
index c074a2ddc96f21..c35e33efb4c55e 100644
--- a/Mathlib/Topology/ContinuousMap/Bounded/Normed.lean
+++ b/Mathlib/Topology/ContinuousMap/Bounded/Normed.lean
@@ -611,4 +611,22 @@ lemma norm_sub_nonneg (f : α →ᵇ ℝ) :
 
 end
 
+/-- If the product of bounded continuous functions is zero, then the norm of their sum is the
+maximum of their norms. -/
+lemma norm_add_eq_max {X R : Type*} [TopologicalSpace X] [NormedRing R] [IsDomain R]
+    {f g : X →ᵇ R} (h : f * g = 0) : ‖f + g‖ = max ‖f‖ ‖g‖ := by
+  have hfg : ∀ x, f x = 0 ∨ g x = 0 := by simpa [DFunLike.ext_iff, mul_eq_zero] using h
+  have hfg' (x : X) : ‖(f + g) x‖ = max ‖f x‖ ‖g x‖ := by obtain (h | h) := hfg x <;> simp [h]
+  apply le_antisymm
+  · rw [norm_le (by positivity)]
+    intro x
+    rw [hfg']
+    apply max_le <;> exact norm_coe_le_norm _ x |>.trans (by simp)
+  · apply max_le
+    all_goals
+      rw [norm_le (by positivity)]
+      intro x
+      grw [← (f + g).norm_coe_le_norm x, hfg']
+      simp
+
 end BoundedContinuousFunction
diff --git a/Mathlib/Topology/ContinuousMap/Compact.lean b/Mathlib/Topology/ContinuousMap/Compact.lean
index 18481b23e5a173..d14fabc4216018 100644
--- a/Mathlib/Topology/ContinuousMap/Compact.lean
+++ b/Mathlib/Topology/ContinuousMap/Compact.lean
@@ -460,4 +460,9 @@ instance [NonUnitalNormedRing β] [StarRing β] [CStarRing β] : CStarRing C(α,
 
 end CStarRing
 
+lemma norm_add_eq_max {X R : Type*} [TopologicalSpace X] [NormedRing R] [IsDomain R]
+    [CompactSpace X] {f g : C(X, R)} (h : f * g = 0) : ‖f + g‖ = max ‖f‖ ‖g‖ := by
+  replace h : mkOfCompact f * mkOfCompact g = 0 := by ext x; simpa using congr($h x)
+  simpa using BoundedContinuousFunction.norm_add_eq_max h
+
 end ContinuousMap

From 36f7a2e1d3e1013643a8aeef7310091713f80ac0 Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Sat, 7 Mar 2026 18:28:05 +0000
Subject: [PATCH 08/20] imports

---
 Mathlib/Analysis/CStarAlgebra/Extreme.lean | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Analysis/CStarAlgebra/Extreme.lean b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
index 2e896a92757357..08e4046c819bff 100644
--- a/Mathlib/Analysis/CStarAlgebra/Extreme.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
@@ -7,13 +7,16 @@ module
 
 public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
 public import Mathlib.Analysis.Convex.Extreme
-public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
+
+import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
+import Mathlib.Analysis.CStarAlgebra.ApproximateUnit
+import Mathlib.Analysis.CStarAlgebra.GelfandDuality
 
 /-! # Extreme points of the closed unit ball in C⋆-algebras
 
 This file contains results on the extreme points of the closed unit ball in (unital) C⋆-algebras. -/
 
-public section
+@[expose] public section
 
 set_option backward.isDefEq.respectTransparency false
 

From 42ca3e85310686c12e6284449df74212ae00ec07 Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Fri, 13 Mar 2026 14:58:15 +0000
Subject: [PATCH 09/20] move

---
 Mathlib/Analysis/CStarAlgebra/Extreme.lean     | 17 ++---------------
 Mathlib/Analysis/Convex/Strict/Extreme.lean    |  5 +++++
 Mathlib/Analysis/Convex/StrictConvexSpace.lean |  3 +++
 Mathlib/Analysis/Normed/Group/Real.lean        |  3 +++
 4 files changed, 13 insertions(+), 15 deletions(-)

diff --git a/Mathlib/Analysis/CStarAlgebra/Extreme.lean b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
index 08e4046c819bff..b4b3c4045413bd 100644
--- a/Mathlib/Analysis/CStarAlgebra/Extreme.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
@@ -8,9 +8,10 @@ module
 public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
 public import Mathlib.Analysis.Convex.Extreme
 
-import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
+import Mathlib.Analysis.Convex.Strict.Extreme
 import Mathlib.Analysis.CStarAlgebra.ApproximateUnit
 import Mathlib.Analysis.CStarAlgebra.GelfandDuality
+import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
 
 /-! # Extreme points of the closed unit ball in C⋆-algebras
 
@@ -22,20 +23,6 @@ set_option backward.isDefEq.respectTransparency false
 
 open Set Metric CFC CStarAlgebra Unitization
 
-@[simp] lemma Set.extremePoints_Icc {a b : ℝ} (hab : a ≤ b) :
-    Set.extremePoints ℝ (Icc a b) = {a, b} := by
-  ext x
-  rw [convex_Icc .. |>.mem_extremePoints_iff_convex_diff]
-  constructor
-  · intro ⟨h₁, h₂⟩
-    suffices x ∉ Ioo a b by grind
-    intro hx
-    have := h₂.isPreconnected.Icc_subset (a := a) (b := b) (by grind) (by grind)
-    grind
-  · rintro (rfl | rfl)
-    · simpa using ⟨hab, convex_Ioc ..⟩
-    · simpa using ⟨hab, convex_Ico ..⟩
-
 open scoped ComplexStarModule in
 lemma CStarAlgebra.one_mem_extremePoints_closedUnitBall {A : Type*} [CStarAlgebra A] :
     1 ∈ extremePoints ℝ (closedBall (0 : A) 1) := by
diff --git a/Mathlib/Analysis/Convex/Strict/Extreme.lean b/Mathlib/Analysis/Convex/Strict/Extreme.lean
index 194c8dc5ddede5..cfb52e39e1db4a 100644
--- a/Mathlib/Analysis/Convex/Strict/Extreme.lean
+++ b/Mathlib/Analysis/Convex/Strict/Extreme.lean
@@ -84,3 +84,8 @@ theorem StrictConvexSpace.extremePoints_closedBall_eq_sphere [Nontrivial A] {x :
     closedBall_diff_ball]
 
 end Normed
+
+@[simp] lemma Set.extremePoints_Icc {a b : ℝ} (hab : a ≤ b) :
+    extremePoints ℝ (Icc a b) = {a, b} := by
+  rw [Real.Icc_eq_closedBall, StrictConvexSpace.extremePoints_closedBall_eq_sphere]
+  grind [Real.sphere_eq_pair]
diff --git a/Mathlib/Analysis/Convex/StrictConvexSpace.lean b/Mathlib/Analysis/Convex/StrictConvexSpace.lean
index ebfddc691e2c91..181e5c66a92501 100644
--- a/Mathlib/Analysis/Convex/StrictConvexSpace.lean
+++ b/Mathlib/Analysis/Convex/StrictConvexSpace.lean
@@ -212,3 +212,6 @@ theorem norm_midpoint_lt_iff (h : ‖x‖ = ‖y‖) : ‖(1 / 2 : ℝ) • (x +
   rw [norm_smul, Real.norm_of_nonneg (one_div_nonneg.2 zero_le_two), ← inv_eq_one_div, ←
     div_eq_inv_mul, div_lt_iff₀ (zero_lt_two' ℝ), mul_two, ← not_sameRay_iff_of_norm_eq h,
     not_sameRay_iff_norm_add_lt, h]
+
+instance Real.instStrictConvexSpace : StrictConvexSpace ℝ ℝ where
+  strictConvex_closedBall _ _ := strictConvex_iff_convex.mpr (convex_closedBall _ _)
diff --git a/Mathlib/Analysis/Normed/Group/Real.lean b/Mathlib/Analysis/Normed/Group/Real.lean
index 43a65abede9381..07a968f2f88104 100644
--- a/Mathlib/Analysis/Normed/Group/Real.lean
+++ b/Mathlib/Analysis/Normed/Group/Real.lean
@@ -114,6 +114,9 @@ theorem toNNReal_eq_nnnorm_of_nonneg (hr : 0 ≤ r) : r.toNNReal = ‖r‖₊ :=
 theorem ofReal_le_enorm (r : ℝ) : ENNReal.ofReal r ≤ ‖r‖ₑ := by
   rw [enorm_eq_ofReal_abs]; gcongr; exact le_abs_self _
 
+lemma sphere_eq_pair {x r : ℝ} (hr : 0 ≤ r) : Metric.sphere x r = {x - r, x + r} := by
+  ext; simp; grind
+
 end Real
 
 section SeminormedCommGroup

From 504fa80c5206cb4e596b025d7be39df54c9a3dbc Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Fri, 20 Mar 2026 13:37:46 +0000
Subject: [PATCH 10/20] Update Real.lean

---
 Mathlib/Analysis/Normed/Group/Real.lean | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/Mathlib/Analysis/Normed/Group/Real.lean b/Mathlib/Analysis/Normed/Group/Real.lean
index 07a968f2f88104..43a65abede9381 100644
--- a/Mathlib/Analysis/Normed/Group/Real.lean
+++ b/Mathlib/Analysis/Normed/Group/Real.lean
@@ -114,9 +114,6 @@ theorem toNNReal_eq_nnnorm_of_nonneg (hr : 0 ≤ r) : r.toNNReal = ‖r‖₊ :=
 theorem ofReal_le_enorm (r : ℝ) : ENNReal.ofReal r ≤ ‖r‖ₑ := by
   rw [enorm_eq_ofReal_abs]; gcongr; exact le_abs_self _
 
-lemma sphere_eq_pair {x r : ℝ} (hr : 0 ≤ r) : Metric.sphere x r = {x - r, x + r} := by
-  ext; simp; grind
-
 end Real
 
 section SeminormedCommGroup

From eeb2b2b2a314cd09e8cfa3532b9d54acf14d3271 Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Sun, 19 Jul 2026 11:49:37 +0100
Subject: [PATCH 11/20] isunital class

---
 Mathlib/Algebra/Algebra/Defs.lean          |  6 ++++
 Mathlib/Algebra/Group/Defs.lean            | 38 ++++++++++++++++++++++
 Mathlib/Algebra/Ring/Defs.lean             | 35 ++++++++++++++++++++
 Mathlib/Analysis/CStarAlgebra/Classes.lean | 13 ++++++++
 4 files changed, 92 insertions(+)

diff --git a/Mathlib/Algebra/Algebra/Defs.lean b/Mathlib/Algebra/Algebra/Defs.lean
index ed95babadabe62..18858a87579893 100644
--- a/Mathlib/Algebra/Algebra/Defs.lean
+++ b/Mathlib/Algebra/Algebra/Defs.lean
@@ -421,3 +421,9 @@ theorem algebraMap.smul' [Monoid A] [MulDistribMulAction A C] [SMulDistribClass
     algebraMap B C (a • b) = a • (algebraMap B C b) := coe_smul' _ _ _
 
 end algebraMap
+
+attribute [local instance] IsUnital.toSemiring in
+/-- A unital non-unital algebra is an algebra. -/
+noncomputable abbrev IsUnital.toAlgebra {R A : Type*} [CommSemiring R] [NonUnitalSemiring A]
+    [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [IsUnital A] : Algebra R A :=
+  .ofModule smul_mul_assoc mul_smul_comm
diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean
index d948baeee2b0ef..0a6426f1f20052 100644
--- a/Mathlib/Algebra/Group/Defs.lean
+++ b/Mathlib/Algebra/Group/Defs.lean
@@ -45,6 +45,8 @@ We register the following instances:
 
 -/
 
+set_option linter.style.longFile 1700
+
 @[expose] public section
 
 assert_not_exists MonoidWithZero DenselyOrdered Function.const_injective
@@ -418,6 +420,38 @@ theorem mul_one : ∀ a : M, a * 1 = a :=
 
 end MulOneClass
 
+section IsUnital
+
+/-- A multiplicative magma is **unital** if there exists a unit.
+
+**Note**: Do not use this unless it is the only reasonable way to phrase or prove a statement.
+In general you should use `NonUnitalRing`, `Ring`, etc. -/
+@[mk_iff] class IsUnital (A : Type*) [Mul A] : Prop where
+  isUnital : ∃ u : A, ∀ x : A, u * x = x ∧ x * u = x
+
+/-- A multiplicative magma is **not-unital** if there does not exist a unit. -/
+@[mk_iff] class IsNotUnital (A : Type*) [Mul A] : Prop where
+  isNotUnital : ∀ u : A, ∃ x : A, u * x ≠ x ∨ x * u ≠ x
+
+@[simp] lemma not_isUnital_iff_isNotUnital {A : Type*} [Mul A] : ¬IsUnital A ↔ IsNotUnital A := by
+  simp [isUnital_iff, isNotUnital_iff, -not_and, Classical.not_and_iff_not_or_not]
+
+@[simp] lemma not_isNotUnital_iff_isUnital {A : Type*} [Mul A] : ¬IsNotUnital A ↔ IsUnital A := by
+  grind [not_isUnital_iff_isNotUnital]
+
+variable {A : Type*}
+
+/-- A unital magma is `MulOneClass`. -/
+noncomputable abbrev IsUnital.toMulOneClass [Mul A] [IsUnital A] : MulOneClass A where
+  one := isUnital.choose
+  one_mul a := (isUnital.choose_spec a).1
+  mul_one a := (isUnital.choose_spec a).2
+
+lemma MulOneClass.isUnital [MulOneClass A] : IsUnital A where
+  isUnital := ⟨1, fun x ↦ ⟨one_mul x, mul_one x⟩⟩
+
+end IsUnital
+
 section
 
 variable {M : Type u}
@@ -784,6 +818,10 @@ end IsDedekindFiniteMonoid
 
 end Monoid
 
+attribute [local instance] IsUnital.toMulOneClass in
+/-- A unital semigroup is a monoid. -/
+noncomputable abbrev IsUnital.toMonoid {A : Type*} [Semigroup A] [IsUnital A] : Monoid A where
+
 /-- An additive monoid is torsion-free if scalar multiplication by every non-zero element `n : ℕ` is
 injective. -/
 @[mk_iff]
diff --git a/Mathlib/Algebra/Ring/Defs.lean b/Mathlib/Algebra/Ring/Defs.lean
index 5bcb9b4e73ec77..ff1fc7bf83ddea 100644
--- a/Mathlib/Algebra/Ring/Defs.lean
+++ b/Mathlib/Algebra/Ring/Defs.lean
@@ -529,3 +529,38 @@ scoped instance (priority := 50) [Ring R] [IsMulCommutative R] :
     CommRing R where
 
 end IsMulCommutative
+
+noncomputable section
+namespace IsUnital
+variable {A : Type*}
+
+attribute [local instance] IsUnital.toMulOneClass
+
+/-- A unital non-associative semiring is a non-associative semiring. -/
+abbrev toNonAssocSemiring [NonUnitalNonAssocSemiring A] [IsUnital A] : NonAssocSemiring A where
+
+/-- A unital non-unital non-associative commutative semiring is a non-associative
+commutative semiring. -/
+abbrev toNonAssocCommSemiring [NonUnitalNonAssocCommSemiring A] [IsUnital A] :
+    NonAssocCommSemiring A where
+
+/-- A unital non-unital semiring is a semiring. -/
+abbrev toSemiring [NonUnitalSemiring A] [IsUnital A] : Semiring A where
+
+/-- A unital non-unital commutative semiring is a commutative semiring. -/
+abbrev toCommSemiring [NonUnitalCommSemiring A] [IsUnital A] : CommSemiring A where
+
+/-- A unital non-unital non-associative ring is a non-associative ring. -/
+abbrev toNonAssocRing [NonUnitalNonAssocRing A] [IsUnital A] : NonAssocRing A where
+
+/-- A unital non-unital non-associative commutative ring is a non-associative commutative ring. -/
+abbrev toNonAssocCommRing [NonUnitalNonAssocCommRing A] [IsUnital A] : NonAssocCommRing A where
+
+/-- A unital non-unital ring is a ring. -/
+abbrev toRing [NonUnitalRing A] [IsUnital A] : Ring A where
+
+/-- A unital non-unital commutative ring is a commutative ring. -/
+abbrev toCommRing [NonUnitalCommRing A] [IsUnital A] : CommRing A where
+
+end IsUnital
+end
diff --git a/Mathlib/Analysis/CStarAlgebra/Classes.lean b/Mathlib/Analysis/CStarAlgebra/Classes.lean
index 023287c12afe89..49cfcde32ba0f4 100644
--- a/Mathlib/Analysis/CStarAlgebra/Classes.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Classes.lean
@@ -141,3 +141,16 @@ noncomputable instance [CStarAlgebra A] : CStarAlgebra Aᵐᵒᵖ where
 noncomputable instance [CommCStarAlgebra A] : CommCStarAlgebra Aᵐᵒᵖ where
 
 end MulOpposite
+
+attribute [local instance] IsUnital.toMulOneClass in
+/-- A unital non-unital C⋆-algebra is a C⋆-algebra. -/
+noncomputable abbrev IsUnital.toCStarAlgebra [NonUnitalCStarAlgebra A] [IsUnital A] :
+    CStarAlgebra A where
+  __ := ‹NonUnitalCStarAlgebra A›
+  __ := toSemiring
+  __ := toAlgebra
+
+attribute [local instance] IsUnital.toCStarAlgebra in
+/-- A unital non-unital commutative C⋆-algebra is a commutative C⋆-algebra. -/
+noncomputable abbrev IsUnital.toCommCStarAlgebra [NonUnitalCommCStarAlgebra A] [IsUnital A] :
+    CommCStarAlgebra A where

From e4260788f0aab114d76d31ce45b094e694111d17 Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Sun, 19 Jul 2026 11:58:12 +0100
Subject: [PATCH 12/20] fix

---
 Mathlib/Analysis/CStarAlgebra/Classes.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Analysis/CStarAlgebra/Classes.lean b/Mathlib/Analysis/CStarAlgebra/Classes.lean
index 49cfcde32ba0f4..ac668009b9a87a 100644
--- a/Mathlib/Analysis/CStarAlgebra/Classes.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Classes.lean
@@ -144,7 +144,7 @@ end MulOpposite
 
 attribute [local instance] IsUnital.toMulOneClass in
 /-- A unital non-unital C⋆-algebra is a C⋆-algebra. -/
-noncomputable abbrev IsUnital.toCStarAlgebra [NonUnitalCStarAlgebra A] [IsUnital A] :
+noncomputable abbrev IsUnital.toCStarAlgebra {A : Type*} [NonUnitalCStarAlgebra A] [IsUnital A] :
     CStarAlgebra A where
   __ := ‹NonUnitalCStarAlgebra A›
   __ := toSemiring
@@ -152,5 +152,5 @@ noncomputable abbrev IsUnital.toCStarAlgebra [NonUnitalCStarAlgebra A] [IsUnital
 
 attribute [local instance] IsUnital.toCStarAlgebra in
 /-- A unital non-unital commutative C⋆-algebra is a commutative C⋆-algebra. -/
-noncomputable abbrev IsUnital.toCommCStarAlgebra [NonUnitalCommCStarAlgebra A] [IsUnital A] :
-    CommCStarAlgebra A where
+noncomputable abbrev IsUnital.toCommCStarAlgebra {A : Type*} [NonUnitalCommCStarAlgebra A]
+    [IsUnital A] : CommCStarAlgebra A where

From dac10dacc9fc2197c066deaf869e91a1bdd8cb1d Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Sun, 19 Jul 2026 12:09:42 +0100
Subject: [PATCH 13/20] fix

---
 .../CStarAlgebra/ApproximateUnit.lean         |  2 --
 Mathlib/Analysis/CStarAlgebra/Extreme.lean    |  8 +++--
 .../Analysis/CStarAlgebra/GelfandDuality.lean | 33 -------------------
 .../ContinuousMap/Bounded/Normed.lean         | 18 ----------
 Mathlib/Topology/ContinuousMap/Compact.lean   |  5 ---
 5 files changed, 5 insertions(+), 61 deletions(-)

diff --git a/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean b/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean
index 9db328a2b75689..0e759020348256 100644
--- a/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean
+++ b/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean
@@ -335,6 +335,4 @@ instance : (approximateUnit A).NeBot := (increasingApproximateUnit A).neBot
 
 end CStarAlgebra
 
-instance : (approximateUnit A).NeBot := (increasingApproximateUnit A).neBot
-
 end ApproximateUnit
diff --git a/Mathlib/Analysis/CStarAlgebra/Extreme.lean b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
index 5a70a5facf2d12..51afa9e8a393f2 100644
--- a/Mathlib/Analysis/CStarAlgebra/Extreme.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
@@ -15,11 +15,13 @@ import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
 
 /-! # Extreme points of the closed unit ball in C⋆-algebras
 
-This file contains results on the extreme points of the closed unit ball in (unital) C⋆-algebras. -/
+This file contains results on the extreme points of the closed unit ball in (unital) C⋆-algebras.
 
-@[expose] public section
+## References
+
+[C⋆-algebras and W⋆-algebras][sakai1971] -/
 
-set_option backward.isDefEq.respectTransparency false
+@[expose] public section
 
 open Set Metric CFC CStarAlgebra Unitization
 
diff --git a/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean b/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean
index 0c4703c73be30d..68ae5a326fbd8f 100644
--- a/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean
+++ b/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean
@@ -410,36 +410,3 @@ lemma WeakDual.CharacterSpace.homeoEval_naturality {X Y 𝕜 : Type*} [RCLike 
     (homeoEval Y 𝕜 : C(_, _)).comp f =
       (f.compStarAlgHom' 𝕜 𝕜 |> compContinuousMap).comp (homeoEval X 𝕜 : C(_, _)) :=
   rfl
-
-open scoped CStarAlgebra in
-open Unitization in
-lemma CommCStarAlgebra.norm_add_eq_max {A : Type*} [NonUnitalCommCStarAlgebra A]
-    {a b : A} (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)
-
-open NonUnitalStarAlgebra in
-lemma IsSelfAdjoint.norm_add_eq_max {A : Type*} [NonUnitalCStarAlgebra A]
-    {a b : A} (hab : a * b = 0) (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) :
-    ‖a + b‖ = max ‖a‖ ‖b‖ := by
-  let S : NonUnitalStarSubalgebra ℂ A := (adjoin ℂ {a, b}).topologicalClosure
-  have hS : IsClosed (S : Set A) := (adjoin ℂ {a, b}).isClosed_topologicalClosure
-  have hab' : a * b = b * a := by
-    rw [hab, eq_comm]; simpa [ha.star_eq, hb.star_eq] using congr(star $hab)
-  let _ : NonUnitalCommRing (adjoin ℂ {a, b}) :=
-    adjoinNonUnitalCommRingOfComm ℂ (by grind) (by grind [IsSelfAdjoint.star_eq])
-  let _ : NonUnitalCommRing S := (adjoin ℂ {a, b}).nonUnitalCommRingTopologicalClosure mul_comm
-  let _ : NonUnitalCommCStarAlgebra S := { }
-  let c : S := ⟨a, subset_closure <| subset_adjoin _ _ <| by grind⟩
-  let d : S := ⟨b, subset_closure <| subset_adjoin _ _ <| by grind⟩
-  exact CommCStarAlgebra.norm_add_eq_max (a := c) (b := d) (by ext; simpa)
-
-lemma IsSelfAdjoint.norm_sub_eq_max {A : Type*} [NonUnitalCStarAlgebra A]
-    {a b : A} (hab : a * b = 0) (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) :
-    ‖a - b‖ = max ‖a‖ ‖b‖ := by
-  rw [← sq_eq_sq₀ (by positivity) (by positivity)]
-  simp only [sq, ← ha.norm_add_eq_max hab hb, ← CStarRing.norm_star_mul_self]
-  have : b * a = 0 := by simpa [ha.star_eq, hb.star_eq] using congr(star $hab)
-  simp [sub_mul, mul_sub, hb.star_eq, ha.star_eq, hab, this, add_mul, mul_add]
diff --git a/Mathlib/Topology/ContinuousMap/Bounded/Normed.lean b/Mathlib/Topology/ContinuousMap/Bounded/Normed.lean
index 2ddec14911f6a6..609b034fba192a 100644
--- a/Mathlib/Topology/ContinuousMap/Bounded/Normed.lean
+++ b/Mathlib/Topology/ContinuousMap/Bounded/Normed.lean
@@ -650,22 +650,4 @@ lemma norm_sub_nonneg (f : α →ᵇ ℝ) :
 
 end
 
-/-- If the product of bounded continuous functions is zero, then the norm of their sum is the
-maximum of their norms. -/
-lemma norm_add_eq_max {X R : Type*} [TopologicalSpace X] [NormedRing R] [IsDomain R]
-    {f g : X →ᵇ R} (h : f * g = 0) : ‖f + g‖ = max ‖f‖ ‖g‖ := by
-  have hfg : ∀ x, f x = 0 ∨ g x = 0 := by simpa [DFunLike.ext_iff, mul_eq_zero] using h
-  have hfg' (x : X) : ‖(f + g) x‖ = max ‖f x‖ ‖g x‖ := by obtain (h | h) := hfg x <;> simp [h]
-  apply le_antisymm
-  · rw [norm_le (by positivity)]
-    intro x
-    rw [hfg']
-    apply max_le <;> exact norm_coe_le_norm _ x |>.trans (by simp)
-  · apply max_le
-    all_goals
-      rw [norm_le (by positivity)]
-      intro x
-      grw [← (f + g).norm_coe_le_norm x, hfg']
-      simp
-
 end BoundedContinuousFunction
diff --git a/Mathlib/Topology/ContinuousMap/Compact.lean b/Mathlib/Topology/ContinuousMap/Compact.lean
index bb007bbac46b07..5565d1fb17d209 100644
--- a/Mathlib/Topology/ContinuousMap/Compact.lean
+++ b/Mathlib/Topology/ContinuousMap/Compact.lean
@@ -514,9 +514,4 @@ instance [NonUnitalNormedRing β] [StarRing β] [CStarRing β] : CStarRing C(α,
 
 end CStarRing
 
-lemma norm_add_eq_max {X R : Type*} [TopologicalSpace X] [NormedRing R] [IsDomain R]
-    [CompactSpace X] {f g : C(X, R)} (h : f * g = 0) : ‖f + g‖ = max ‖f‖ ‖g‖ := by
-  replace h : mkOfCompact f * mkOfCompact g = 0 := by ext x; simpa using congr($h x)
-  simpa using BoundedContinuousFunction.norm_add_eq_max h
-
 end ContinuousMap

From 708a13e5baec041a7017c4325ad708cbcdea47c2 Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Sun, 19 Jul 2026 12:18:08 +0100
Subject: [PATCH 14/20] fix

---
 Mathlib/Analysis/CStarAlgebra/Extreme.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Analysis/CStarAlgebra/Extreme.lean b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
index 51afa9e8a393f2..1fe6bc78bba4ed 100644
--- a/Mathlib/Analysis/CStarAlgebra/Extreme.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
@@ -94,7 +94,7 @@ theorem star_self_conjugate_eq_self_of_mem_extremePoints_closedUnitBall {a : A}
   obtain ⟨ha, h⟩ := ha
   simp only [mem_closedBall, dist_zero_right] at ha h
   refine @h _ ?_ ((2 : ℝ) • a - a * abs a) ?_ ⟨2⁻¹, 2⁻¹, by simp [smul_sub, ← two_mul]⟩
-  · grw [norm_mul_le, norm_abs, ha, one_mul]
+  · grw [norm_mul_le, norm_abs, ha, one_mul, ha]
   · calc
       _ = ‖(2 : ℝ) • abs a - abs a * abs a‖ := by
         simp_rw [← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _), sq, ← CStarRing.norm_star_mul_self]
@@ -156,9 +156,10 @@ private theorem eq_zero_of_eq_sub_of_mem_closedBall_of_mem_extremePoints_closedU
   /- Since `p` and `star a * a` are self-adjoint
   with product zero that the norm of their sum is the max of the norms of these contractions. -/
   have hmax : ‖p + star a * a‖ ≤ 1 := by
-    rw [IsSelfAdjoint.star_mul_self x |>.norm_add_eq_max hpa (.star_mul_self a), sup_le_iff, hp]
+    rw [IsSelfAdjoint.star_mul_self x |>.norm_add_eq_max (.star_mul_self a) hpa, sup_le_iff]
     simp only [CStarRing.norm_star_mul_self]
-    grw [mem_closedBall_zero_iff.mp hx.1, mem_closedBall_zero_iff.mp ha, one_mul, and_self]
+    grw [mem_closedBall_zero_iff.mp hx.1, mem_closedBall_zero_iff.mp hx.1,
+      mem_closedBall_zero_iff.mp ha, mem_closedBall_zero_iff.mp ha, one_mul, and_self]
   have : ‖x + a‖ ≤ 1 := sq_le_one_iff₀ (by positivity) |>.mp <| by grind
   /- Using `hxa` and `hax`, cross terms vanish and we have
   `‖x - a‖ * ‖x - a‖ = ‖p + star a * a‖ ≤ 1`. -/

From 82189d984a96ddce6c0e3386381772af5761123e Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Sun, 19 Jul 2026 12:21:46 +0100
Subject: [PATCH 15/20] isunital

---
 Mathlib/Analysis/CStarAlgebra/Extreme.lean | 35 +++++++++-------------
 1 file changed, 14 insertions(+), 21 deletions(-)

diff --git a/Mathlib/Analysis/CStarAlgebra/Extreme.lean b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
index 1fe6bc78bba4ed..379c939b0915b5 100644
--- a/Mathlib/Analysis/CStarAlgebra/Extreme.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
@@ -6,6 +6,7 @@ Authors: Monica Omar, Jireh Loreaux, Jon Bannon
 module
 
 public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
+public import Mathlib.Analysis.CStarAlgebra.Unitary.Maps
 public import Mathlib.Analysis.Convex.Extreme
 
 import Mathlib.Analysis.Convex.Strict.Extreme
@@ -84,6 +85,11 @@ lemma CStarAlgebra.one_mem_extremePoints_closedUnitBall {A : Type*} [CStarAlgebr
   rw [← norm_eq_zero, ← sq_eq_zero_iff, ← IsSelfAdjoint.norm_mul_self (ℑ x).2, ← sq, norm_eq_zero]
   exact le_antisymm (by simpa using hx) (ℑ x).2.sq_nonneg
 
+lemma Unitary.coe_mem_extremePoints_unitClosedBall {A : Type*} [CStarAlgebra A] (u : unitary A) :
+    (u : A) ∈ extremePoints ℝ (closedBall 0 1) := by
+  rw [← map_zero (mulLeft ℝ A u), ← LinearIsometryEquiv.image_closedBall, ← image_extremePoints]
+  exact ⟨1 , ⟨one_mem_extremePoints_closedUnitBall, by simp⟩⟩
+
 variable {A : Type*} [NonUnitalCStarAlgebra A]
 
 theorem star_self_conjugate_eq_self_of_mem_extremePoints_closedUnitBall {a : A}
@@ -121,7 +127,6 @@ theorem isStarProjection_self_mul_star_of_mem_extremePoints_closedUnitBall
     {a : A} (ha : a ∈ extremePoints ℝ (closedBall 0 1)) : IsStarProjection (a * star a) := by
   grind [star_self_conjugate_eq_self_of_mem_extremePoints_closedUnitBall ha]
 
-
 /-- If `x` is an extreme point in the closed unit ball of a C⋆-algebra `A`,
 with initial projection `p = star x * x` and final projection `q = x * star x`,
 "`(1 - q) A (1 - p) = 0`". Note: This notation is an informal
@@ -208,28 +213,16 @@ theorem CStarAlgebra.ofExtremePtOne_mul {x : A} (hx : x ∈ extremePoints ℝ (c
     (a : A) : (star x * x + x * star x - x * star x * (star x * x)) * a = a := by
   simpa [add_comm] using congr(star $(mul_ofExtremePtOne (x := star x) (by simpa) (star a)))
 
-/-- The ring structure given an extreme point of the closed unit ball on a non-unital
-C⋆-algebra. Only an implementation for `CStarAlgebra.ofExtremePt`. -/
-abbrev CStarAlgebra.ringOfExtremePt {x : A} (hx : x ∈ extremePoints ℝ (closedBall 0 1)) :
-    Ring A where
-  one := star x * x + x * star x - x * star x * (star x * x)
-  one_mul y := ofExtremePtOne_mul hx y
-  mul_one y := mul_ofExtremePtOne hx y
-
-lemma CStarAlgebra.ofExtremePt_one_def {x : A} (hx : x ∈ extremePoints ℝ (closedBall 0 1)) :
-    letI := CStarAlgebra.ringOfExtremePt hx
-    1 = star x * x + x * star x - x * star x * (star x * x) :=
-  rfl
+attribute [local instance] IsUnital.toCStarAlgebra in
+/-- A C⋆-algebra is unital iff there exists an extreme point of the closed unit ball.
 
-/-- Upgrade a non-unital C⋆-algebra to a unital C⋆-algebra, given there exists an
-extreme point of the closed unit ball. -/
-abbrev CStarAlgebra.ofExtremePt {x : A} (hx : x ∈ extremePoints ℝ (closedBall 0 1)) :
-    CStarAlgebra A where
-  __ := ‹NonUnitalCStarAlgebra A›
-  __ := ringOfExtremePt hx
-  __ := Algebra.ofModule smul_mul_assoc mul_smul_comm
+To upgrade a non-unital C⋆-algebra to a unital one, use `IsUnital.toCStarAlgebra`. -/
+theorem CStarAlgebra.isUnital_iff :
+    IsUnital A ↔ (extremePoints ℝ (closedBall (0 : A) 1)).Nonempty := by
+  rw [Set.nonempty_def]
+  refine ⟨fun h ↦ ⟨1, one_mem_extremePoints_unitClosedBall⟩, fun ⟨x, hx⟩ ↦ ?_⟩
+  exact ⟨_, fun y ↦ ⟨ofExtremePtOne_mul hx y, mul_ofExtremePtOne hx y⟩⟩
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The star projections in a non-unital C⋆-algebra are exactly the extreme points of
 the nonnegative closed unit ball. -/
 theorem isStarProjection_iff_mem_extremePoints_setOfPred_nonneg_inter_unitClosedBall

From 678b65855a60d7091d965f30ade70c01349c0940 Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Sun, 19 Jul 2026 12:22:42 +0100
Subject: [PATCH 16/20] remove expose

---
 Mathlib/Analysis/CStarAlgebra/Extreme.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Analysis/CStarAlgebra/Extreme.lean b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
index 379c939b0915b5..2e847f27ea841d 100644
--- a/Mathlib/Analysis/CStarAlgebra/Extreme.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
@@ -22,7 +22,7 @@ This file contains results on the extreme points of the closed unit ball in (uni
 
 [C⋆-algebras and W⋆-algebras][sakai1971] -/
 
-@[expose] public section
+public section
 
 open Set Metric CFC CStarAlgebra Unitization
 

From d0560b98233caa1e79a291d6d56f94f2238251b9 Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Sun, 19 Jul 2026 13:21:31 +0100
Subject: [PATCH 17/20] fix

---
 Mathlib/Analysis/CStarAlgebra/Extreme.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Analysis/CStarAlgebra/Extreme.lean b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
index 2e847f27ea841d..c03685b1d43b32 100644
--- a/Mathlib/Analysis/CStarAlgebra/Extreme.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
@@ -27,7 +27,7 @@ public section
 open Set Metric CFC CStarAlgebra Unitization
 
 open scoped ComplexStarModule in
-lemma CStarAlgebra.one_mem_extremePoints_closedUnitBall {A : Type*} [CStarAlgebra A] :
+lemma CStarAlgebra.one_mem_extremePoints_unitClosedBall {A : Type*} [CStarAlgebra A] :
     1 ∈ extremePoints ℝ (closedBall (0 : A) 1) := by
   nontriviality A
   /- Suppose that `1` is a convex combination of `x` and `y`. Then, since `1` is self
@@ -88,7 +88,7 @@ lemma CStarAlgebra.one_mem_extremePoints_closedUnitBall {A : Type*} [CStarAlgebr
 lemma Unitary.coe_mem_extremePoints_unitClosedBall {A : Type*} [CStarAlgebra A] (u : unitary A) :
     (u : A) ∈ extremePoints ℝ (closedBall 0 1) := by
   rw [← map_zero (mulLeft ℝ A u), ← LinearIsometryEquiv.image_closedBall, ← image_extremePoints]
-  exact ⟨1 , ⟨one_mem_extremePoints_closedUnitBall, by simp⟩⟩
+  exact ⟨1 , ⟨one_mem_extremePoints_unitClosedBall, by simp⟩⟩
 
 variable {A : Type*} [NonUnitalCStarAlgebra A]
 
@@ -170,6 +170,7 @@ private theorem eq_zero_of_eq_sub_of_mem_closedBall_of_mem_extremePoints_closedU
   `‖x - a‖ * ‖x - a‖ = ‖p + star a * a‖ ≤ 1`. -/
   have : ‖x - a‖ ≤ 1 := sq_le_one_iff₀ (by positivity) |>.mp <| by
     simp [sq, ← CStarRing.norm_star_mul_self, sub_mul, mul_sub, hax, hxa, ← hp, hmax]
+  rw [mem_extremePoints_iff_left] at hx
   exact add_eq_left.mp <| @hx.2 (x + a) (by simpa) (x - a) (by simpa)
     ⟨2⁻¹, 2⁻¹, by simp [smul_add, smul_sub, ← add_smul, ← one_div]⟩
 
@@ -203,6 +204,7 @@ theorem star_mem_extremePoints_closedBall_zero_iff {A : Type*} [NonUnitalSeminor
     from ⟨fun h ↦ star_star x ▸ this (star x) h, this x⟩
   refine fun x hx ↦ ⟨by simpa using hx.1, fun y hy z hz ⟨α, β, hα, hβ, hαβ, hxyz⟩ ↦ ?_⟩
   rw [eq_star_iff_eq_star, eq_comm] at hxyz ⊢
+  rw [mem_extremePoints_iff_left] at hx
   apply @hx.2 _ (by simpa using hy) (star z) (by simpa using hz) ⟨star α, star β, ?_⟩
   simp [← hxyz, hα, hβ, hαβ]
 

From f9f2d312257dfcaaa2140ac89fb205a6ead6c5f6 Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Sun, 19 Jul 2026 13:22:54 +0100
Subject: [PATCH 18/20] fix

---
 Mathlib/Analysis/CStarAlgebra/Extreme.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Analysis/CStarAlgebra/Extreme.lean b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
index c03685b1d43b32..2ddaef8fe80ba1 100644
--- a/Mathlib/Analysis/CStarAlgebra/Extreme.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
@@ -97,7 +97,7 @@ theorem star_self_conjugate_eq_self_of_mem_extremePoints_closedUnitBall {a : A}
   let := spectralOrder A
   let := spectralOrderedRing A
   suffices a * abs a = a by rw [mul_assoc, ← abs_mul_abs, ← mul_assoc, this, this]
-  obtain ⟨ha, h⟩ := ha
+  obtain ⟨ha, h⟩ := mem_extremePoints_iff_left.mp ha
   simp only [mem_closedBall, dist_zero_right] at ha h
   refine @h _ ?_ ((2 : ℝ) • a - a * abs a) ?_ ⟨2⁻¹, 2⁻¹, by simp [smul_sub, ← two_mul]⟩
   · grw [norm_mul_le, norm_abs, ha, one_mul, ha]

From d521c2d567ede7fad33921772e55d8e21b4331cd Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Mon, 20 Jul 2026 20:15:28 +0100
Subject: [PATCH 19/20] inline instance

---
 Mathlib/Analysis/CStarAlgebra/Extreme.lean | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Analysis/CStarAlgebra/Extreme.lean b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
index 2ddaef8fe80ba1..99b55b61d4744e 100644
--- a/Mathlib/Analysis/CStarAlgebra/Extreme.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
@@ -215,15 +215,18 @@ theorem CStarAlgebra.ofExtremePtOne_mul {x : A} (hx : x ∈ extremePoints ℝ (c
     (a : A) : (star x * x + x * star x - x * star x * (star x * x)) * a = a := by
   simpa [add_comm] using congr(star $(mul_ofExtremePtOne (x := star x) (by simpa) (star a)))
 
-attribute [local instance] IsUnital.toCStarAlgebra in
 /-- A C⋆-algebra is unital iff there exists an extreme point of the closed unit ball.
 
 To upgrade a non-unital C⋆-algebra to a unital one, use `IsUnital.toCStarAlgebra`. -/
 theorem CStarAlgebra.isUnital_iff :
     IsUnital A ↔ (extremePoints ℝ (closedBall (0 : A) 1)).Nonempty := by
   rw [Set.nonempty_def]
-  refine ⟨fun h ↦ ⟨1, one_mem_extremePoints_unitClosedBall⟩, fun ⟨x, hx⟩ ↦ ?_⟩
-  exact ⟨_, fun y ↦ ⟨ofExtremePtOne_mul hx y, mul_ofExtremePtOne hx y⟩⟩
+  refine ⟨fun h ↦ let := h.toCStarAlgebra; ⟨1, one_mem_extremePoints_unitClosedBall⟩, ?_⟩
+  exact fun ⟨x, hx⟩ ↦ ⟨_, fun y ↦ ⟨ofExtremePtOne_mul hx y, mul_ofExtremePtOne hx y⟩⟩
+
+theorem CStarAlgebra.isNotUnital_iff :
+    IsNotUnital A ↔ extremePoints ℝ (closedBall (0 : A) 1) = ∅ := by
+  simp [← not_isUnital_iff_isNotUnital, isUnital_iff, not_nonempty_iff_eq_empty]
 
 /-- The star projections in a non-unital C⋆-algebra are exactly the extreme points of
 the nonnegative closed unit ball. -/

From 5569c7c2b1d021a9539c6148d2a8a68316ace83b Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Tue, 21 Jul 2026 07:09:51 +0100
Subject: [PATCH 20/20] cleanup

---
 Mathlib/Analysis/CStarAlgebra/Extreme.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Analysis/CStarAlgebra/Extreme.lean b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
index 99b55b61d4744e..69dbf1116bfa01 100644
--- a/Mathlib/Analysis/CStarAlgebra/Extreme.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Extreme.lean
@@ -220,13 +220,13 @@ theorem CStarAlgebra.ofExtremePtOne_mul {x : A} (hx : x ∈ extremePoints ℝ (c
 To upgrade a non-unital C⋆-algebra to a unital one, use `IsUnital.toCStarAlgebra`. -/
 theorem CStarAlgebra.isUnital_iff :
     IsUnital A ↔ (extremePoints ℝ (closedBall (0 : A) 1)).Nonempty := by
-  rw [Set.nonempty_def]
+  rw [nonempty_def]
   refine ⟨fun h ↦ let := h.toCStarAlgebra; ⟨1, one_mem_extremePoints_unitClosedBall⟩, ?_⟩
   exact fun ⟨x, hx⟩ ↦ ⟨_, fun y ↦ ⟨ofExtremePtOne_mul hx y, mul_ofExtremePtOne hx y⟩⟩
 
 theorem CStarAlgebra.isNotUnital_iff :
     IsNotUnital A ↔ extremePoints ℝ (closedBall (0 : A) 1) = ∅ := by
-  simp [← not_isUnital_iff_isNotUnital, isUnital_iff, not_nonempty_iff_eq_empty]
+  simpa [not_nonempty_iff_eq_empty] using isUnital_iff.not
 
 /-- The star projections in a non-unital C⋆-algebra are exactly the extreme points of
 the nonnegative closed unit ball. -/