Commit 2025-05-24 01:40 6c8de9b8

perf: make the support of onFinset opaque (#24944) It's very handy to have defeq of the function within a Finsupp, but we almost never care about the defeq of the support, especially since it almost always involves Classical.decidable which doesn't reduce. This mplements my idea from [#mathlib4 > simp timeout at `whnf` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/simp.20timeout.20at.20.60whnf.60/near/518404806), aimed at making (mapRange _ _ _).support irreducible. This breaks the defeq of 0 = 0 + 0 on finsupp, but I think that's ok. With irreducible_def we get a 75% speedup (150⬝10⁹ instructions) on Mathlib.Algebra.Category.ModuleCat.Presheaf.Free, while with @[irreducible] we get a 12% (24⬝10⁹ instructions) slowdown.