Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-15 12:38 8c53048a

View on Github →

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.

Estimated changes