tracking: #30658 split into pieces

[grunweg]

---

• depends on: style(RingTheory): fix whitespace #30685
• depends on: [Merged by Bors] - style(Analysis): fix whitespace #30687
• depends on: style(Algebra): fix whitespace #30688
• depends on: [Merged by Bors] - style(CategoryTheory): fix whitespace #30689
• depends on: style(Order): fix whitespace #30690
• depends on: style(misc): fix whitespace #30691

Not meant for merging, but for me tracking the changes locally. This PR should never land directly.
Also, note that I'm the author from git's point of view, which is entirely wrong (it's Damiano, for all of them).

[github-actions]

PR summary dde1cfffb6

Import changes exceeding 2%

%	File
+25.00%	Mathlib.Tactic.Linter.CommandStart

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.Linter.CommandStart	4	5	+1 (+25.00%)

Import changes for all files

Files	Import difference
Mathlib.Tactic.Linter.CommandStart	1

---

Declarations diff

+ AfterAtom
+ Correspondence
+ DFX
+ Exceptions
+ ExcludedSyntaxNodeKind
+ ExcludedSyntaxNodeKind.contains
+ FX
+ FX(_
+ PPinstruction
+ PPref
+ _root_.Lean.SourceInfo.compareSpaces
+ _root_.Lean.SourceInfo.getLeadTrail
+ _root_.Lean.SourceInfo.removeSpaces
+ _root_.Lean.Syntax.compare
+ _root_.Lean.Syntax.compareSpaces
+ _root_.Lean.Syntax.compareToString
+ _root_.Lean.Syntax.eraseLeadTrailSpaces
+ _root_.Lean.Syntax.regString
+ _root_.Mathlib.Linter.mex.mkWindow
+ _root_.Mathlib.Linter.mex.toLinterWarning
+ _root_.String.mkGroups
+ _root_.Substring.break
+ _root_.Substring.toRange
+ addException
+ allowedTrail
+ atomOrIdentEndPos
+ byTens
+ captureException
+ compareLeaf
+ consumeIgnoring
+ exclusions
+ forceNoSpaceAfter
+ forceSpaceAfter
+ forceSpaceAfter'
+ generateCorrespondence
+ getChoiceNode
+ getExceptions
+ ignoreSpaceAfter
+ insertSpaces
+ insertSpacesAux
+ instance (priority := 100) small_succ (α : Type v) : Small.{v + 1} α
+ instance : Inhabited ℍ[R] := inferInstanceAs <| Inhabited ℍ[R,-1,0,-1]
+ instance : ToString Exceptions
+ instance [Nontrivial R] : Nontrivial ℍ[R,c₁,c₂,c₃] := (equivTuple c₁ c₂ c₃).surjective.nontrivial
+ instance [Repr R] {a b c : R} : Repr ℍ[R,a,b,c]
+ instance [SMul S R] : SMul S ℍ[R] := inferInstanceAs <| SMul S ℍ[R,-1,0,-1]
+ instance [Subsingleton R] : Subsingleton ℍ[R,c₁,c₂,c₃] := (equivTuple c₁ c₂ c₃).subsingleton
+ invisible
+ leftInverse_of_surjective_of_rightInverse
+ leftInverse_of_surjective_of_rightInverse1
+ mex
+ mex.toString
+ mkExpectedWindow
+ mkRangeError
+ mkStrings
+ mkWdw
+ mkWindowSubstring
+ mkWindowSubstring'
+ modifyTail
+ onlineComment
+ ppCategory'
+ pretty
+ processAtomOrIdent
+ readWhile
+ reduceWhitespace
+ reportedAndUnreportedExceptions
+ scanWatching
+ skipped
+ totalExclusions
+ unparseable
+ validateAtomOrId
+ validateSpaceAfter
+ validateSpaceAfter'
+ withVerbose
++ «--»
- bar
- foo
- instance (priority := 100) small_succ (α : Type v) : Small.{v+1} α
- instance : Inhabited ℍ[R] := inferInstanceAs <| Inhabited ℍ[R,-1, 0, -1]
- instance [Nontrivial R] : Nontrivial ℍ[R, c₁, c₂, c₃] := (equivTuple c₁ c₂ c₃).surjective.nontrivial
- instance [Repr R] {a b c : R} : Repr ℍ[R, a, b, c]
- instance [SMul S R] : SMul S ℍ[R] := inferInstanceAs <| SMul S ℍ[R,-1, 0, -1]
- instance [Subsingleton R] : Subsingleton ℍ[R, c₁, c₂, c₃] := (equivTuple c₁ c₂ c₃).subsingleton
--++ instance {R} : Add R := sorry

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh 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).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• style(RingTheory): fix whitespace #30685
• [Merged by Bors] - style(Analysis): fix whitespace #30687
• style(Algebra): fix whitespace #30688
• [Merged by Bors] - style(CategoryTheory): fix whitespace #30689
• style(Order): fix whitespace #30690
• style(misc): fix whitespace #30691
  By Dependent Issues (🤖). Happy coding!

[mathlib4-merge-conflict-bot]

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