Commit 2022-08-22 16:05 6c88b50f
View on Github →fix: remove @[reducible] attribute from Function.injective (#375)
In mathlib3, function.injective is not reducible, so Function.injective should not be reducible here either.
To avoid errors in Order/Basic ("@[ext] attribute only applies to structures or lemmas proving x = y"), we need to adjust extAttribute too.
Fixes some problems seen in #372.