Commit 2023-07-15 01:08 c1acdccdView on Github →
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