chore(set/function): remove reducible on eq_on (#8738)
This backs out #8736, and instead removes the unnecessary `@[reducible]`.
This leaves the `simp` lemma available if anyone wants it (although it is not currently used in mathlib3), but should still resolve the problem that @dselsam's experimental `simp` in the binport of mathlib3 was excessively enthusiastic about using this lemma.
