Commit 2023-07-15 01:08 c1acdccd

fix(tactic/norm_num): Do not allow typos in simp lemmas if they are unused (#17981) Previously

import tactic.norm_num
example : 1 + 1 = 2 :=
by norm_num [nonsense]

was legal. More realistically, if a lemma was added to the simp set then renamed, norm_num [old_name] would keep working even if the lemma no longer existed. This only seemed to happen once in mathlib, in the tests. It feels a bit silly to build the lemma set only to discard it, but we already rebuild the same lemma set on every iteration of the repeat1