refactor: remove DecidableEq and DecidableLT from LinearOrder

[astrainfinita]

---

We may eventually remove DecidableLE as well. Removing all of the Decidable* fields would not result in any loss of decidability, since LinearOrder extends Ord and requires compare to agree with the order. However, doing so may require a better-designed API around compare.

• depends on: refactor: use cmpLE in LinearOrder #42569

[github-actions]

PR summary b1f02423ec

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ Std.LawfulLECmp.eq_cmpLE
+ cmpLE_eq_eq
+ cmpLE_eq_gt
+ cmpLE_eq_lt
+ compareOfLessAndEq_eq_cmpLE
+ compare_eq_compareOfLessAndEq
+ inl_apply
+ inr_apply
+ instDecidableEq
+ instDecidableLT
+ instance (o : Ordinal) : DecidableEq o.ToType := Classical.decRel _
+ instance (o : Ordinal) : DecidableLT o.ToType := Classical.decRel _
+ instance (s t : Finset α) : Decidable (G.IsUniform ε s t)
+ instance : DecidableEq (MulArchimedeanClass M) := Classical.decRel _
+ instance : DecidableEq Ordinal := Classical.decRel _
+ instance : DecidableLT (MulArchimedeanClass M) := Classical.decRel _
+ instance : DecidableLT F
+ instance : DecidableLT Ordinal := Classical.decRel _
+ instance : DecidableLT SignType := decidableLTOfDecidableLE
+ instance [DecidableEq α] : Std.LawfulBCmp (compare (α := α))
+ instance [DecidableLE α] (s : Flag α) : LinearOrder s
+ instance [DecidableLE α] [@Std.Total α (· ≤ ·)] :
+ instance [DecidableLT α] : DecidableLT (Antisymmetrization α (· ≤ ·))
+ instance [DecidableLT α] [DecidableLT β] : Inhabited (PartialIso α β)
+ instance _root_.LowerSet.instDecidableEq : DecidableEq (LowerSet α)
+ instance _root_.LowerSet.instDecidableLT : DecidableLT (LowerSet α)
+ isGE_cmpLE
+ isLE_cmpLE
+ powers_toFun
+ signVariations_def
+ sparsePairs_def
- instance : Inhabited (PartialIso α β) := ⟨⟨∅, fun _p h _q ↦ (Finset.notMem_empty _ h).elim⟩⟩
- instance : Std.LawfulBCmp (compare (α := α))
- instance [DecidableLE α] [DecidableLT α] [@Std.Total α (· ≤ ·)] :
- instance [DecidableLE α] [DecidableLT α] [DecidableEq α] (s : Flag α) : LinearOrder s
-++- Ico_inter_Ico
--++ Ico_filter_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 b1f0242).

• +41 new declarations
• −12 removed declarations

+ArchimedeanClass.instDecidableEq
+ArchimedeanClass.instDecidableLT
+CompleteLinearOrder.compare_eq_cmpLE
-CompleteLinearOrder.compare_eq_compareOfLessAndEq
-CompleteLinearOrder.toDecidableEq
-CompleteLinearOrder.toDecidableLT
+ConditionallyCompleteLinearOrder.compare_eq_cmpLE
-ConditionallyCompleteLinearOrder.compare_eq_compareOfLessAndEq
-ConditionallyCompleteLinearOrder.toDecidableEq
-ConditionallyCompleteLinearOrder.toDecidableLT
+ENNReal.instDecidableEq
+ENNReal.instDecidableLT
+Finpartition.sparsePairs_def
+Flag.instLinearOrderSubtypeMemOfDecidableLE
-Flag.instLinearOrderSubtypeMemOfDecidableLEOfDecidableLTOfDecidableEq
+LinearOrder.compare_eq_cmpLE
-LinearOrder.compare_eq_compareOfLessAndEq
-LinearOrder.toDecidableEq
-LinearOrder.toDecidableLT
+LowerSet.instDecidableEq
+LowerSet.instDecidableLT
+MulArchimedeanClass.instDecidableEq
+MulArchimedeanClass.instDecidableLT
+NNReal.instDecidableEq
+NNReal.instDecidableLT
+Ordinal.instDecidableEq
+Ordinal.instDecidableLT
+Polynomial.signVariations_def
+SignType.instDecidableLT
+Std.LawfulLECmp.eq_cmpLE
+UpperSet.instDecidableEq
+UpperSet.instDecidableLT
+cmpLE_eq_eq
+cmpLE_eq_gt
+cmpLE_eq_lt
+compareOfLessAndEq_eq_cmpLE
+compare_eq_compareOfLessAndEq
+instDecidableEqENat
+instDecidableEqEReal
+instDecidableEqNNRat
+instDecidableEqToType
+instDecidableLTAntisymmetrizationLe
+instDecidableLTENat
+instDecidableLTEReal
+instDecidableLTNNRat
+instDecidableLTPNat
+instDecidableLTToType
-instLinearOrderAntisymmetrizationLeOfDecidableLEOfDecidableLTOfTotal
+instLinearOrderAntisymmetrizationLeOfDecidableLEOfTotal
+isGE_cmpLE
+isLE_cmpLE
+tacticCmpLE_rfl
-tacticCompareOfLessAndEq_rfl

---

Decrease in strong tech debt: (relative, absolute) = (1.61, 0.01)

Current number	Change	Type (strong)
419	-1	porting notes
385	-2	adaptation notes
6977	-4	backward.isDefEq.respectTransparency
3985	-2	backward.isDefEq.respectTransparency.types

No changes to weak technical debt.

Current commit b1f02423ec
Reference commit ac10dc7e9a

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

[mathlib-dependent-issues]

This PR/issue depends on:

• refactor: use cmpLE in LinearOrder #42569
  By Dependent Issues (🤖). Happy coding!