Commit 2025-02-19 07:30 cba55ba8

perf: make Decidable Injective approximately twice as fast (#21975) The existing implementation takes the definition (∀ x y, f x = f y → x = y) directly. This is suboptimal because:

1. Every pair of values is checked twice (both (x, y) and (y, x))
2. The diagonals (x, x) are checked redundantly
3. The outputs of f are not cached, which might be a problem if f is expensive This PR proposes a new implementation of Decidable Injective and Decidable InjOn. It collects the outputs in a Multiset, then decides Multiset.Nodup. Because Nodup is built upon List.Pairwise, which only checks unordered non-diagonal pairs, the above problems are addressed automatically. This also allows for dropping DecidableEq on the input type, as that was to work around the diagonal case. Thank you @edegeltje and @plp127 for suggesting List.Pairwise, and many other people in the [Zulip thread] for the discussion around Sym2 (which ended up being unused here, but was still valuable). [Zulip thread]: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Idea.3A.20Helper.20for.20speeding.20up.20Decidable.20on.20symmetric.20props