[Merged by Bors] - feat(push): error message tweaks#38008

grunweg wants to merge 3 commits intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

grunweg:atlocation-message-tweaksgrunweg/mathlib4:atlocation-message-tweaksCopy head branch name to clipboard