Commit 2026-03-18 17:28 e90aebbb

chore: golf using fin_omega, simp_all and grind +splitIndPred (#36509) 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):

• Fin.lt_sub_iff: 46 ms before, <30 ms after 🎉
• ArchimedeanClass.add_left_cancel_of_ne_top: 134 ms before, <30 ms after 🎉
• exists_seq_of_forall_finset_exists': <30 ms before, 53 ms after
• Filter.hasBasis_biInf_of_directed': unchanged 🎉
• Filter.hasBasis_biInf_of_directed: <30 ms before, 53 ms after 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