Dangerous simp lemmas

[gebner]

We mark some lemmas as simp that were innocuous in Lean 3, but are dangerous now.

The typical case is that the lhs is reducible. For example, Lean 3 triggered only on inj_on applications, while Lean 4 tries to apply the lemma to everything (often causing nontermination):

attribute [-simp] Set.inj_on_empty Set.inj_on_singleton

[digama0]

Can we backport remove these? It should not be too hard to write a lint for mathlib to detect them.

[gebner]

We could also remove reducible from set.inj_on.

[digama0]

That would be another way to silence the lint, yes. (And I agree that's the way to go here.)