Commit 2025-11-21 15:15 ee16c226

perf: de-instance some WithLp norm structures used for type synonyms (#31819) The recent refactor of WithLp into a one-field structure caused an unexpected slowdown in completely unrelated files. Some sleuthing by @kbuzzard revealed that this was caused by Lean performing unification on some new instances which are only intended for type synonyms. Because these are only intended for synonyms, we de-instance them here, and they can be copied over when a user creates a synonym. During the investigation, we also uncovered that one of the statements (normSMulClassSeminormedAddCommGroupToProd) for the Prod synonyms was using the wrong norm, and Lean had secretly elaborated the statement using Prod.toNorm instead. We fix this error and prevent stray elaboration by locally disabling the usual Prod/Pi norm instances.