Commit 2026-02-23 03:56 6466c770

chore: golf proofs (#35244) The goal of this golfing 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 (shown if ≥10 ms before or after):

• LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem: 199 ms before, 162 ms after 🎉
• tendsto_natCast_div_add_atTop: 247 ms before, 136 ms after 🎉
• tendsto_div_of_monotone_of_exists_subseq_tendsto_div: 2757 ms before, 2376 ms after 🎉
• CategoryTheory.Presieve.isSheaf_iff_preservesFiniteProducts: 219 ms before, 198 ms after 🎉
• CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_iff_epi₃: 15 ms before, 13 ms after 🎉
• CategoryTheory.Pretriangulated.Triangle.mor₃_eq_zero_iff_mono₁: 23 ms before, 15 ms after 🎉
• List.IsChain.cons_of_le: 22 ms before, 17 ms after 🎉
• List.Perm.inter_append: 194 ms before, 19 ms after 🎉
• Equivalence.quot_mk_eq_iff: <10 ms before, <10 ms after 🎉
• Stream'.Seq.destruct_eq_none: <10 ms before, <10 ms after 🎉
• MulAction.IsBlock.subsingleton_of_ssubset_of_stabilizer_le: 169 ms before, 105 ms after 🎉
• IsSimpleGroup.prime_card: 60 ms before, 48 ms after 🎉
• RootPairing.coxeterWeightIn_le_four: 1236 ms before, 1126 ms after 🎉
• MeasureTheory.Measure.haveLebesgueDecomposition_of_finiteMeasure: 659 ms before, 584 ms after 🎉
• IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_smulHaarMeasure: 85 ms before, 80 ms after 🎉
• MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_regular: 58 ms before, 50 ms after 🎉
• MeasureTheory.SignedMeasure.exists_subset_restrict_nonpos: 413 ms before, 325 ms after 🎉
• FirstOrder.Language.Embedding.coe_injective: <10 ms before, <10 ms after 🎉
• ProbabilityTheory.setLIntegral_stieltjesOfMeasurableRat: 343 ms before, 310 ms after 🎉
• ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_atBot_zero: 116 ms before, 75 ms after 🎉
• ProbabilityTheory.lintegral_toKernel_mem: 173 ms before, 172 ms after 🎉
• MeasureTheory.Measure.tendsto_IicSnd_atBot: 70 ms before, 63 ms after 🎉
• ProbabilityTheory.eq_condKernel_of_measure_eq_compProd': 46 ms before, 30 ms after 🎉
• MeasureTheory.StronglyMeasurable.integral_kernel_prod_right: 1298 ms before, 1142 ms after 🎉
• ProbabilityTheory.Kernel.isSFiniteKernel_withDensity_of_isFiniteKernel: 433 ms before, 429 ms after 🎉
• MeasureTheory.progMeasurable_of_tendsto': 20 ms before, <10 ms after 🎉
• MeasureTheory.Measure.infinitePi_map_piCurry_symm: 1319 ms before, 1291 ms after 🎉
• HahnModule.add_smul: 111 ms before, 75 ms after 🎉
• Module.associatedPrimes.mem_associatedPrimes_of_comap_mem_associatedPrimes_of_isLocalizedModule: 215 ms before, 198 ms after 🎉
• Ideal.comap_eq_of_scalar_tower_quotient: 97 ms before, 56 ms after 🎉 This golfing 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