mathlib

159e1e20 - feat(tactic/assert_exists): add a linter to protect against typos (#17519)

feat(tactic/assert_exists): add a linter to protect against typos (#17519) Since this later can fail if not run in `all.lean`, we do not tag these declarations with `@[linter]`; instead they are added manually to the list of linters mathlib uses in CI.