Commit 2026-03-26 19:33 51369e6e

View on Github →

chore: golf using exact/simpa (#35731) 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):

  • AlgebraicGeometry.Scheme.Cover.exists_of_trans_eq_trans: unchanged 🎉
  • AlgebraicGeometry.compactSpace_iff_exists: unchanged 🎉
  • SimplexCategory.eq_id_of_mono: unchanged 🎉
  • SimplexCategory.eq_id_of_epi: unchanged 🎉
  • CategoryTheory.GrothendieckTopology.isIso_toPlus_of_isSheaf: unchanged 🎉
  • CategoryTheory.Functor.isTriangulated_of_op: unchanged 🎉
  • SimpleGraph.chromaticNumber_top: unchanged 🎉
  • SimpleGraph.Subgraph.singletonSubgraph_connected: unchanged 🎉
  • SimpleGraph.Walk.exists_length_eq_one_iff: unchanged 🎉
  • Turing.TM2to1.addBottom_modifyNth: unchanged 🎉
  • IsNoetherian.iff_fg: unchanged 🎉
  • contMDiff_inclusion: unchanged 🎉
  • FermatLastTheoremForThree_of_FermatLastTheoremThreeGen: 146 ms before, 91 ms after 🎉
  • FermatLastTheoremForThreeGen.lambda_sq_dvd_c: 313 ms before, 218 ms after 🎉
  • WithTop.isGLB_sInf: unchanged 🎉
  • WithBot.succ_eq_bot: 56 ms before, <30 ms after 🎉
  • WithTop.pred_eq_top: unchanged 🎉 Profiled using set_option trace.profiler true in.

Estimated changes

modified theorem IsNoetherian.iff_fg