Commit 2026-03-24 23:14 dee91c53

View on Github →

chore: golf proofs (#36014) The goal of this PR is to decrease the number of times lemmas are called explicitly (replacing calls to lemmas with calls to tactics). 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):

  • Polynomial.smeval_commute_left: unchanged 🎉
  • lp.norm_rpow_eq_tsum: unchanged 🎉
  • ComputablePred.rice: unchanged 🎉
  • ZNum.cmp_to_int: unchanged 🎉
  • ZMod.inv_coe_unit: unchanged 🎉
  • Ideal.Filtration.submodule_fg_iff_stable: 343 ms before, 197 ms after 🎉
  • t2Space_of_properSMul_of_t1Group: unchanged 🎉 Profiled using set_option trace.profiler true in. This PR is batched under the following guidelines:
  • Up to ~5 changed files per PR
  • Up to ~25 changed declarations per PR
  • Up to ~100 changed lines per PR

Estimated changes