Commit 2026-03-22 08:27 ea46a8dc

chore(AlgebraicGeometry): remove use of clear*- from isClosedMap_iff_specializingMap (#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.