chore(AlgebraicGeometry): remove use of clear*- from isClosedMap_iff_specializingMap (leanprover-community#36961)

In the previous proof of isClosedMap_iff_specializingMap the tactic clearExcept (clear*-) is used to clear the auxDecl which is created by wlog since there are two wlog in the proof. This is undesirable because it requires knowledge of the unexpected behaviour of clearExcept to understand the proof. Marking the lemma as `nonrec` means that clearExcept can be removed from the proof.

Author: oliver-butterley

Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

@@ -224,7 +224,7 @@ lemma isCompact_iff_exists {U : X.Opens} :
   rwa [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, IsOpenImmersion.lift_fac]
 
 @[stacks 01K9]
-lemma isClosedMap_iff_specializingMap (f : X ⟶ Y) [QuasiCompact f] :
+nonrec lemma isClosedMap_iff_specializingMap (f : X ⟶ Y) [QuasiCompact f] :
     IsClosedMap f ↔ SpecializingMap f := by
   refine ⟨fun h ↦ h.specializingMap, fun H ↦ ?_⟩
   wlog hY : ∃ R, Y = Spec R
@@ -236,7 +236,6 @@ lemma isClosedMap_iff_specializingMap (f : X ⟶ Y) [QuasiCompact f] :
     exact IsZariskiLocalAtTarget.of_isPullback
       (P := topologically @SpecializingMap) (.of_hasPullback _ _) H
   obtain ⟨S, rfl⟩ := hY
-  clear * - H
   intro Z hZ
   replace H := hZ.stableUnderSpecialization.image H
   wlog hX : ∃ R, X = Spec R