feat(Order): use to_dual for PFilter

[staroperator]

We can get rid of the whole PFilter file now.

---

• depends on: feat(Order/Ideal): more results on order ideals #34820

---

[github-actions]

PR summary eccf962962

Import changes exceeding 2%

%	File
+4.96%	Mathlib.Order.Ideal
+4.73%	Mathlib.Order.PrimeIdeal

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Order.PFilter	485	0	-485 (-100.00%)
Mathlib.Order.Ideal	484	508	+24 (+4.96%)
Mathlib.Order.PrimeIdeal	486	509	+23 (+4.73%)

Import changes for all files

Files	Import difference
Mathlib.Order.PFilter	-485
Mathlib.RingTheory.IdealFilter.Topology	-1
Mathlib.ModelTheory.Fraisse Mathlib.ModelTheory.PartialEquiv	1
Mathlib.Order.PrimeSeparator	20
Mathlib.Order.PrimeIdeal	23
Mathlib.Order.CountableDenseLinearOrder Mathlib.Order.Ideal	24

---

Declarations diff

+ Coinitial
+ IsProper.exists_le_maximal
+ _root_.Order.PFilter.IsProper
+ _root_.Order.PFilter.IsUltra
+ biSup_mem
+ biSup_mem_iff
+ eq_top_iff_top_mem
+ exists_maximal
+ iSup_mem
+ iSup_mem_iff
+ instance [LE P] [OrderTop P] : IsCoatomic (Ideal P) := by
+ instance _root_.Order.PFilter.instCompleteLattice [SemilatticeInf P] [OrderTop P] :
+ instance _root_.Order.PFilter.instLattice [SemilatticeInf P] [IsDirectedOrder P] :
+ instance _root_.Order.PFilter.instPartialOrderPFilter : PartialOrder (PFilter P)
+ isMaximal_of_isCoatom
+ isProper_iff_top_notMem
+ isProper_of_isCoatom
+ isProper_principal_iff
+ le_toIdeal
+ mem_toIdeal
+ sequenceOfCofinals.mono
+ sequenceOfCoinitials
+ toIdeal_le
- IsPFilter.of_def
- IsPFilter.toPFilter
- antitone_principal
- directed
- ext
- infGi
- inf_mem
- inf_mem_iff
- instance : OrderBot (PFilter P)
- instance : PartialOrder (Ideal P) := .ofSetLike (Ideal P) P
- instance : PartialOrder (PFilter P) := .ofSetLike (PFilter P) P
- instance : SetLike (PFilter P) P
- instance [Inhabited P] : Inhabited (PFilter P) := ⟨⟨default⟩⟩
- instance {P} [Preorder P] [OrderBot P] : OrderTop (PFilter P)
- isPFilter
- mem_mk
- mem_of_le
- mem_of_mem_of_le
- mem_principal
- nonempty
- principal
- principal_le_iff
- principal_le_principal_iff
- sInf_gc
- sequenceOfCofinals.monotone
- top_mem

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).

---

note: file Mathlib/Order/PFilter.lean was removed.
Please create a follow-up pull request adding a module deprecation. Thanks!

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(Order/Ideal): more results on order ideals #34820
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

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