[Merged by Bors] - chore: miscellaneous linter whitespace fixes#30663

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

grunweg:whitespace1019grunweg/mathlib4:whitespace1019Copy head branch name to clipboard