Update comment.

Vierkantor · web-flow · commit dec48d23712c · 2025-01-23T15:44:18.000+01:00
diff --git a/Mathlib/AlgebraicGeometry/AffineScheme.lean b/Mathlib/AlgebraicGeometry/AffineScheme.lean
@@ -812,7 +812,6 @@ def SpecMapRestrictBasicOpenIso {R S : CommRingCat} (f : R ⟶ S) (r : R) :
         show _ =
           (f ≫ (Scheme.ΓSpecIso S).inv ≫ (Spec S).presheaf.map (homOfLE le_top).op)
         ext
-        -- This `simp` is too slow, but I can't find an easy way to speed it up...
         simp only [Localization.awayMap, IsLocalization.Away.map, AlgEquiv.toRingEquiv_eq_coe,
           RingEquiv.toCommRingCatIso_hom, AlgEquiv.toRingEquiv_toRingHom, CommRingCat.hom_comp,
           CommRingCat.hom_ofHom, RingHom.comp_apply, IsLocalization.map_eq, RingHom.coe_coe,
