Commit 2025-05-12 12:44 61963a9c

chore: remove double spaces between arguments (#24810) Mathlib style is to have only one space. This also touches a handful of comments: while subjective, these were all such occurrences in mathlib. Starting a bikeshedding thread about those does not seem useful, and (unlike for spaces after periods) there are no competing style rules in other languages either. If that part is controversial, I'll happily revert it.