Commit 2023-06-15 04:49 28ad0a65
View on Github →chore: remove reducible from Function.Surjective (#5063)
The @[reducible] attribute on Function.Surjective is apparently not needed, and currently prevents @[simp] lemmas with Function.Surjective side conditions from firing, see zulip discussion.