Commit 2026-04-10 19:05 927c562e

chore: golf proofs (#37475) 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):

• ✅️ LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot: unchanged 🎉
• ✅️ LinearOrder.strong_induction_of_finite: unchanged 🎉
• ✅️ ProbabilityTheory.poissonPMFRealSum: 140 ms before, <30 ms after 🎉 Profiled using set_option trace.profiler true in.