[Merged by Bors] - chore: delete unused test file#30497

grunweg wants to merge 1 commit intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

grunweg:delete-superfluousgrunweg/mathlib4:delete-superfluousCopy head branch name to clipboard