chore: add newline between public and private imports

[felixpernegger]

It is (or at least seems to be) convention to make a new line between public imports and private import (and public imports should come first). This PR adds those missing newlines.

Sometimes public imports were (mistakenly?) added after private imports. This PR fixes this as well and orders the imports of affected lines alphabetically.

As a standalone PR, this is pretty unimportant, but ought to make the diffs (and thus reviewing) of later PRs sorting imports etc prettier

---

[github-actions]

PR summary 933477989a

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.PNatToNat	612	613	+1 (+0.16%)

Import changes for all files

Files	Import difference
Mathlib.Tactic.PNatToNat	1

---

Declarations diff (regex)

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 9334779).

• +0 new declarations
• −0 removed declarations

No declaration differences.

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 933477989a
Reference commit bb1587137f

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-bors]

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

[felixpernegger]

Please no slowdown
!bench

[leanprover-radar]

Benchmark results for dd2637b against 0434c03 are in. No significant results found. @felixpernegger

• ✅ build//instructions: -54.8G (-0.04%)

No significant changes detected.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[themathqueen]

It is (or at least seems to be) convention to make a new line between public imports and private import (and public imports should come first).

I'm not sure having a new line between imports is a rule we have. But I'm for having public import before import.

[felixpernegger]

It is (or at least seems to be) convention to make a new line between public imports and private import (and public imports should come first).

I'm not sure having a new line between imports is a rule we have. But I'm for having public import before import.

I think this has been mentioned on Zulip here and there, originally here #mathlib4 > Mathlib has moved to the new module system @ 💬.

It is also a bit more common to have an emptyline (Regex public import.+\n\nimport gives 198 occurences vs public import.+\nimport giving 138) and has recently been discussed here #mathlib4 > Technical Debt Counters @ 💬. (Though I cant find the PR Yael is refering to)

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[kim-em]

Superseded by #44512, which groups public and private imports in 2,076 Mathlib files and has passed a full local Mathlib build.