chore(Order/RelClasses): remove redundant instances

[SnirBroshi]

Some instances can be synthesized but are necessary to help to_dual, so they are kept.

---

Also remove instance names using to_dual none.

[github-actions]

PR summary b94a989b30

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ instance [LinearOrder α] : Std.Total (α := α) (· ≤ ·)
+ instance [LinearOrder α] : Std.Trichotomous (α := α) (· < ·)
+ instance [PartialOrder α] : Std.Antisymm (α := α) (· ≤ ·)
+ instance [Preorder α] : Std.Asymm (α := α) (· < ·)
- LE.total
- instAntisymmLe
- instAntisymmLt
- instAsymmLt
- instIrreflLt
- instTrichotomousLe
- instTrichotomousLt
- instance : @Std.Antisymm ZFSet (· ⊆ ·)
- instance : @Std.Refl (Quotient s) (· ≤ ·)
- instance : @Std.Refl ZFSet (· ⊆ ·)
- instance : IsNonstrictStrictOrder ZFSet (· ⊆ ·) (· ⊂ ·)
- instance : IsTrans (Quotient s) (· ≤ ·)
- instance : IsTrans ZFSet (· ⊆ ·)
- instance [Preorder α] : IsTrans α (· < ·)
- instance [Preorder α] : IsTrans α (· ≤ ·)
- isTrans_le
- isTrans_lt

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

• +4 new declarations
• −34 removed declarations

-LE.total
-LE.total'
-Quotient.instIsTransLe
-Quotient.instReflLe_mathlib
-ZFSet.instAntisymmLe
-ZFSet.instIsNonstrictStrictOrderLeLt
-ZFSet.instIsTransLe
-ZFSet.instReflLe
-instAntisymmGe
-instAntisymmGt
-instAntisymmLe
+instAntisymmLe_mathlib
-instAntisymmLt
-instAsymmGt
-instAsymmLt
+instAsymmLt_mathlib
-instIrreflGt
-instIrreflLt
-instIsLinearOrderGe
-instIsNonstrictStrictOrderGeGt
-instIsPartialOrderGe
-instIsPreorderGe
-instIsStrictOrderGt
-instIsStrictTotalOrderGt
-instIsTransGe
-instIsTransGt
-instIsTransLe
-instIsTransLt
+instTotalLe_mathlib
-instTrichotomousGe
-instTrichotomousGt
-instTrichotomousLe
-instTrichotomousLt
+instTrichotomousLt_mathlib
-isTrans_ge
-isTrans_gt
-isTrans_le
-isTrans_lt

---

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

Current commit b94a989b30
Reference commit a4bb538cf7

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

[SnirBroshi]

!bench

[leanprover-radar]

Benchmark results for b94a989 against a4bb538 are in. No significant results found. @SnirBroshi

• ✅ build//instructions: -7.8G (-0.01%)

Small changes (1✅)

• ✅ build/module/Mathlib.Geometry.Manifold.SmoothApprox//instructions: -267.4M (-2.89%)