chore(data/set/function): remove useless @[simp] (#8736)
This lemma
```
lemma eq_on_empty (f₁ f₂ : α → β) : eq_on f₁ f₂ ∅ := λ x, false.elim
```
is currently marked `@[simp]`, but can never fire, because after noting `eq_on` is `@[reducible]`, the pattern we would be replacing looks like `?f ?x`, which Lean3's simp doesn't like.
On the other hand, @dselsam's experiments with discrimination trees in simp in the binport of mathlib are spending most of their time on this lemma!
Let's get rid of it.
