mathlib

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

fix(tactic/norm_num): Do not allow typos in simp lemmas if they are unused (#17981) Previously ```lean 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`