revert one

Author: kim-em

Mathlib/Topology/Sheaves/Skyscraper.lean

@@ -232,7 +232,9 @@ theorem skyscraperPresheaf_isSheaf : (skyscraperPresheaf p₀ A).IsSheaf := by
           dsimp [skyscraperPresheaf]
           rw [if_neg]
           · exact terminalIsTerminal
-          · exact Set.notMem_empty PUnit.unit.{u + 1})))
+          · #adaptation_note /-- 2024-03-24
+            Previously the universe annotation was not needed here. -/
+            exact Set.notMem_empty PUnit.unit.{u + 1})))
 
 /--
 The skyscraper presheaf supported at `p₀` with value `A` is the sheaf that assigns `A` to all opens