Commit 2026-03-24 23:14 9d7d1f86

View on Github →

chore: golf using grind and simp (#36684) The goal of this PR is to decrease the number of times lemmas are called explicitly. Any decrease in compilation time is a welcome side effect, although it is not a primary objective. Trace profiling results (differences <30 ms considered measurement noise):

CategoryTheory.classifier_isSheaf: unchanged 🎉
EuclideanGeometry.orthogonalProjection_vadd_eq_self: unchanged 🎉
AEMeasurable.map_add₀: unchanged 🎉
PrimitiveSpectrum.hull_inf: unchanged 🎉 Profiled using set_option trace.profiler true in.

Estimated changes

Modified Mathlib/CategoryTheory/Sites/Closed.lean

Modified Mathlib/Geometry/Euclidean/Projection.lean

Modified Mathlib/MeasureTheory/Measure/AEMeasurable.lean

Modified Mathlib/Topology/Order/HullKernel.lean