Commit 2021-08-18 05:11 40b7dc75

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.