Commit 2021-08-18 16:14 a47d49db

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.