mathlib3

8c53048a - fix(tactic/assert_exists): avoid name collisions in linter declarations (#17550)

fix(tactic/assert_exists): avoid name collisions in linter declarations (#17550) Previously there was a check to avoid adding a declaration if it already existed. This didn't really solve the problem though, as likely the definition would be provided by two files that were unaware of each other, and the collision would only occur when both are imported simultaneously. I also forgot to `git add` the test last time.