feat(logic/nontrivial): function.injective.exists_ne (#3983)
feat(logic/nontrivial): function.injective.exists_ne (#3983)

Add a lemma that an injective function from a nontrivial type has an
argument at which it does not take a given value.






leanprover-community/mathlib,leanprover-community/mathlib