Commit 2026-03-25 22:45 70599e79

View on Github →

chore: golf using grind and simp (#36645) 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):

  • HomotopicalAlgebra.Cylinder.LeftHomotopy.weakEquivalence_iff: unchanged 🎉
  • HomotopicalAlgebra.PathObject.RightHomotopy.weakEquivalence_iff: unchanged 🎉
  • Finset.noncommProd_mulSingle: unchanged 🎉
  • Finset.support_smulAntidiagonal_subset_smul: unchanged 🎉
  • Function.updateFinset_updateFinset_of_subset: unchanged 🎉
  • AlgebraicGeometry.PresheafedSpace.stalkMap.id: 94 ms before, <30 ms after 🎉
  • IsUpperSet.total: unchanged 🎉
  • MeasureTheory.IsStoppingTime.measurableSet_le_stopping_time: unchanged 🎉 Profiled using set_option trace.profiler true in.

Estimated changes