feat: backport `Function.Injective` etc from Mathlib

[urkud]

Also move Std.Logic to Std.Logic.Basic.

[urkud]

I changed some names and deduplicated lemmas while backporting, so review carefully, please.

[digama0]

Std.Logic should be re-added as a import-only file for backward compatibility

[urkud]

awaiting-review

[kim-em]

I changed some names and deduplicated lemmas while backporting, so review carefully, please.

I'm not suggesting going back in this instance, but I think it is usually overall easier to do the refactor in Mathlib, then have a copy-and-paste migration to Std, then have a just-delete-stuff adaptation PR to Mathlib, rather than risking having a nightmarish adaptation PR to Mathlib due to unexpected consequences of changes during the migration.

[urkud]

I changed some names and deduplicated lemmas while backporting, so review carefully, please.

I'm not suggesting going back in this instance, but I think it is usually overall easier to do the refactor in Mathlib, then have a copy-and-paste migration to Std, then have a just-delete-stuff adaptation PR to Mathlib, rather than risking having a nightmarish adaptation PR to Mathlib due to unexpected consequences of changes during the migration.

Thank you for the information. I volunteer to adapt Mathlib.

[urkud]

I've started doing the same changes in Mathlib, see leanprover-community/mathlib4#9738 for the first batch. Let's wait with merging this PR till I sync Mathlib with it.

awaiting-author

[urkud]

UPD: @sgouezel is working on changing Surjective f from ∀ y, ∃ x, f x = y to ∀ y, ∃ x, y = f x. Waiting for updates.