diff --git a/Mathlib/Analysis/NormedSpace/Star/GelfandDuality.lean b/Mathlib/Analysis/NormedSpace/Star/GelfandDuality.lean
index 14338cca23ec7..bec670f8b890d 100644
--- a/Mathlib/Analysis/NormedSpace/Star/GelfandDuality.lean
+++ b/Mathlib/Analysis/NormedSpace/Star/GelfandDuality.lean
@@ -52,16 +52,10 @@ Then `η₁ : id → F ∘ G := gelfandStarTransform` and
 
 ## TODO
 
-* After `StarAlgEquiv` is defined, realize `gelfandTransform` as a `StarAlgEquiv`.
-* Prove that if `A` is the unital C⋆-algebra over `ℂ` generated by a fixed normal element `x` in
-  a larger C⋆-algebra `B`, then `characterSpace ℂ A` is homeomorphic to `spectrum ℂ x`.
-* From the previous result, construct the **continuous functional calculus**.
-* Show that if `X` is a compact Hausdorff space, then `X` is (canonically) homeomorphic to
-  `characterSpace ℂ C(X, ℂ)`.
-* Conclude using the previous fact that the functors `C(·, ℂ)` and `characterSpace ℂ ·` along with
-  the canonical homeomorphisms described above constitute a natural contravariant equivalence of
-  the categories of compact Hausdorff spaces (with continuous maps) and commutative unital
-  C⋆-algebras (with unital ⋆-algebra homomorphisms); this is known as **Gelfand duality**.
+* After defining the category of commutative unital C⋆-algebras, bundle the existing unbundled
+  **Gelfand duality** into an actual equivalence (duality) of categories associated to the
+  functors `C(·, ℂ)` and `characterSpace ℂ ·` and the natural isomorphisms `gelfandStarTransform`
+  and `WeakDual.CharacterSpace.homeoEval`.
 
 ## Tags