refactor(Topology/Sion): use a dense and continuous completion to generalize the statements

[AntoineChambert-Loir]

Use the existence of a dense and continuous completion to simplify the final part of the proof of Sion's theorem.

As a matter of fact, only an early lemma needs to be modified and the rest holds in weaker assumptions,
leading to a serious simplification.

Since the PR proving Sion is very recent and unused, we didn't add deprecation lemmas.

---

• depends on: feat(Order/Completion): embed a linear order into a dense and complete linear order #37939

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(Order/Completion): embed a linear order into a dense and complete linear order #37939
  By Dependent Issues (🤖). Happy coding!

[github-actions]

PR summary cb39573f93

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.Sion	1450	1453	+3 (+0.21%)

Import changes for all files

Files	Import difference
Mathlib.Topology.Sion	3
Mathlib.Topology.Order.Completion (new file)	858

---

Declarations diff

+ DedekindCut.continuous_principal
+ Fill
+ continuous_some
+ exists_dense_continuous_completion
+ exists_lt_iInf_of_lt_iInf_of_sup'
+ instance : DenselyOrdered (Fill α)
+ instance : TopologicalSpace (Fill α) := Preorder.topology _
+ instance [DenselyOrdered α] : DenselyOrdered (DedekindCut α)
+ instance [Preorder α] [Preorder β] [NoMaxOrder β] [DenselyOrdered β] :
+ instance [Preorder α] [Preorder β] [NoMinOrder β] [DenselyOrdered β] :
+ instance [TopologicalSpace α] [OrderTopology α] : OrderTopology (Fill α)
+ le_principal_iff
+ lt_iff_exists
+ lt_iff_exists'
+ lt_principal_iff
+ principal_le_iff
+ principal_lt_iff
+ some
- DMCompletion.exists_isSaddlePointOn
- exists_isSaddlePointOn'
- exists_saddlePointOn'

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

[github-actions]

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!