Commit 2026-03-02 16:30 827d1348
View on Github →chore: golf using simp (#35726)
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):
IsScalarTower.adjoin_range_toAlgHom: 106 ms before, 41 ms after 🎉ChainComplex.mkAux_eq_shortComplex_mk_d_comp_d: unchanged 🎉QuadraticAlgebra.algebraMap_dvd_iff_dvd: 91 ms before, 34 ms after 🎉orthonormal_fourier: unchanged 🎉Real.tendsto_euler_sin_prod: 712 ms before, 96 ms after 🎉CategoryTheory.CatCommSq.vInv_vInv: 224 ms before, 120 ms after 🎉CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π_apply: unchanged 🎉CategoryTheory.MonObj.one_associator: 96 ms before, 54 ms after 🎉SimpleGraph.chromaticNumber_ne_top_iff_exists: unchanged 🎉Multiset.antidiagonal_cons: 104 ms before, <30 ms after 🎉Nat.getLast_digit_ne_zero: 153 ms before, 89 ms after 🎉QPF.suppPreservation_iff_liftpPreservation: unchanged 🎉List.Vector.reverse_get_zero: 128 ms before, 46 ms after 🎉ZMod.neg_eq_self_iff: 166 ms before, 93 ms after 🎉alternatingGroup.kleinFour_eq_commutator: unchanged 🎉Matrix.det_succ_row: 647 ms before, 328 ms after 🎉TensorPower.mul_one: 483 ms before, 298 ms after 🎉NumberField.mixedEmbedding.convexBodySumFun_eq_zero_iff: unchanged 🎉Real.coe_fib_eq': 233 ms before, 159 ms after 🎉Zsqrtd.intCast_dvd_intCast: unchanged 🎉ProbabilityTheory.gaussianReal_map_const_mul: 583 ms before, 198 ms after 🎉ProbabilityTheory.gaussianReal_map_linearMap: unchanged 🎉Finset.univ_of_card_le_three: 194 ms before, 151 ms after 🎉IsFractionRing.isUnit_den_iff: 400 ms before, 137 ms after 🎉MatrixEquivTensor.right_inv: 329 ms before, 259 ms after 🎉Algebra.norm_algebraMap_of_basis: unchanged 🎉Polynomial.content_X_mul: unchanged 🎉Ordinal.nfp_mul_one: unchanged 🎉Ordinal.nfp_mul_zero: unchanged 🎉unique_topology_of_t2: unchanged 🎉TopCat.binaryCofan_isColimit_iff: 3138 ms before, 1214 ms after 🎉ContinuousMap.sup_mem_closed_subalgebra: unchanged 🎉OpenPartialHomeomorph.subtypeRestr_symm_eqOn_of_le: 108 ms before, 45 ms after 🎉 Profiled usingset_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