Commit 2026-09-28 17:33 6e123c3c

perf(Analysis/Normed/Affine/Isometry): scope the V₄/P₄ and V₁'/P₁' variables to their users (#42246) The section variable block of this file declares six torsor pairs. Each pair has four instance binders. Only two declarations use the V₄/P₄ pair: comp_assoc and trans_assoc. Only seven declarations use the V₁'/P₁' pair: AffineIsometry.injective, map_eq_iff, map_ne, and the four AffineSubspace.isometryEquivMap declarations. All other declarations carry these eight instance binders in their local context. Every typeclass search must examine them. This PR removes the two pairs from the block. Two small sections declare the V₁'/P₁' pair again, around the declarations that use it. comp_assoc and trans_assoc declare the V₄/P₄ pair in their own binders. The nine statements do not change significantly: only the order of their implicit and instance binders changes. Mathlib contains no @-application of any of the nine. Speeds up elaboration of this file by ~6%. 🤖 Generated with Claude Code