refactor: Remove order instances from `SetLike`

[artie2000]

• Remove order instances from SetLike
• Add class IsConcreteLE for SetLike instances whose map is order-preserving

See discussion at https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Abstracting.20the.20substructure.20lattice.20construction/with/563952738

---

[github-actions[bot]]

PR summary f91c049b4f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ IsConcreteLE + LE.ofSetLike + PartialOrder.ofSetLike + instance : IsConcreteLE (LowerSet α) α + instance : PartialOrder (AffineSubspace k P) := .ofSetLike (AffineSubspace k P) P + instance : PartialOrder (BooleanSubalgebra α) := .ofSetLike (BooleanSubalgebra α) α + instance : PartialOrder (ClopenUpperSet α) := .ofSetLike (ClopenUpperSet α) α + instance : PartialOrder (Clopens α) := .ofSetLike (Clopens α) α + instance : PartialOrder (ClosedSubgroup G) := .ofSetLike (ClosedSubgroup G) G + instance : PartialOrder (ClosedSubmodule R M) := .ofSetLike (ClosedSubmodule R M) M + instance : PartialOrder (Closeds α) := .ofSetLike (Closeds α) α + instance : PartialOrder (CompactOpens α) := .ofSetLike (CompactOpens α) α + instance : PartialOrder (Compacts α) := .ofSetLike (Compacts α) α + instance : PartialOrder (CompleteSublattice α) := .ofSetLike (CompleteSublattice α) α + instance : PartialOrder (ConvexBody V) := .ofSetLike (ConvexBody V) V + instance : PartialOrder (ConvexCone R M) := .ofSetLike (ConvexCone R M) M + instance : PartialOrder (DecSubObj X) := .ofSetLike (DecSubObj X) X + instance : PartialOrder (Finset α) := .ofSetLike (Finset α) α + instance : PartialOrder (Flag α) := .ofSetLike (Flag α) α + instance : PartialOrder (FractionalIdeal S P) := .ofSetLike (FractionalIdeal S P) P + instance : PartialOrder (G.ComponentCompl K) := .ofSetLike (G.ComponentCompl K) V + instance : PartialOrder (GroupCone G) := .ofSetLike (GroupCone G) G + instance : PartialOrder (HomogeneousIdeal 𝒜) := .ofSetLike (HomogeneousIdeal 𝒜) A + instance : PartialOrder (HomogeneousSubsemiring 𝒜) := .ofSetLike (HomogeneousSubsemiring 𝒜) A + instance : PartialOrder (Ideal P) := .ofSetLike (Ideal P) P + instance : PartialOrder (Interval α) := .ofSetLike (Interval α) α + instance : PartialOrder (IrreducibleCloseds α) := .ofSetLike (IrreducibleCloseds α) α + instance : PartialOrder (L.DefinableSet A α) := .ofSetLike (L.DefinableSet A α) (α → M) + instance : PartialOrder (L.ElementarySubstructure M) := .ofSetLike (L.ElementarySubstructure M) M + instance : PartialOrder (L.Substructure M) := .ofSetLike (L.Substructure M) M + instance : PartialOrder (LieSubalgebra R L) := .ofSetLike (LieSubalgebra R L) L + instance : PartialOrder (LieSubmodule R L M) := .ofSetLike (LieSubmodule R L M) M + instance : PartialOrder (MySubobject X) := .ofSetLike (MySubobject X) X + instance : PartialOrder (NonUnitalStarSubalgebra R A) := .ofSetLike (NonUnitalStarSubalgebra R A) A + instance : PartialOrder (NonUnitalSubalgebra R A) := .ofSetLike (NonUnitalSubalgebra R A) A + instance : PartialOrder (NonUnitalSubring R) := .ofSetLike (NonUnitalSubring R) R + instance : PartialOrder (NonUnitalSubsemiring R) := .ofSetLike (NonUnitalSubsemiring R) R + instance : PartialOrder (NonemptyChain α) := .ofSetLike (NonemptyChain α) α + instance : PartialOrder (NonemptyCompacts α) := .ofSetLike (NonemptyCompacts α) α + instance : PartialOrder (NonemptyInterval α) := .ofSetLike (NonemptyInterval α) α + instance : PartialOrder (OpenNhdsOf x) := .ofSetLike (OpenNhdsOf x) α + instance : PartialOrder (OpenNormalSubgroup G) := .ofSetLike (OpenNormalSubgroup G) G + instance : PartialOrder (OpenSubgroup G) := .ofSetLike (OpenSubgroup G) G + instance : PartialOrder (Opens α) := .ofSetLike (Opens α) α + instance : PartialOrder (PFilter P) := .ofSetLike (PFilter P) P + instance : PartialOrder (Partition s) := .ofSetLike (Partition s) α + instance : PartialOrder (PositiveCompacts α) := .ofSetLike (PositiveCompacts α) α + instance : PartialOrder (ProperCone R E) := .ofSetLike (ProperCone R E) E + instance : PartialOrder (RelUpperSet P) := .ofSetLike (RelUpperSet P) α + instance : PartialOrder (RingCone R) := .ofSetLike (RingCone R) R + instance : PartialOrder (RingPreordering R) := .ofSetLike (RingPreordering R) R + instance : PartialOrder (StarSubalgebra R A) := .ofSetLike (StarSubalgebra R A) A + instance : PartialOrder (SubDPIdeal hI) := .ofSetLike (SubDPIdeal hI) A + instance : PartialOrder (SubMulAction R M) := .ofSetLike (SubMulAction R M) M + instance : PartialOrder (SubObj X) := .ofSetLike (SubObj X) X + instance : PartialOrder (Subalgebra R A) := .ofSetLike (Subalgebra R A) A + instance : PartialOrder (Subcomplex C) := .ofSetLike (Subcomplex C) X + instance : PartialOrder (Subfield K) := .ofSetLike (Subfield K) K + instance : PartialOrder (Subgroup G) := .ofSetLike (Subgroup G) G + instance : PartialOrder (Subgroupoid C) := .ofSetLike (Subgroupoid C) (Σ c d : C, c ⟶ d) + instance : PartialOrder (Sublattice α) := .ofSetLike (Sublattice α) α + instance : PartialOrder (Sublocale X) := .ofSetLike (Sublocale X) X + instance : PartialOrder (Submodule R M) := .ofSetLike (Submodule R M) M + instance : PartialOrder (Submonoid M) := .ofSetLike (Submonoid M) M + instance : PartialOrder (Subrepresentation ρ) := .ofSetLike (Subrepresentation ρ) W + instance : PartialOrder (Subring R) := .ofSetLike (Subring R) R + instance : PartialOrder (Subsemigroup M) := .ofSetLike (Subsemigroup M) M + instance : PartialOrder (Subsemiring R) := .ofSetLike (Subsemiring R) R + instance : PartialOrder (Subspace K V) := .ofSetLike (Subspace K V) (ℙ K V) + instance : PartialOrder (Sylow p G) := .ofSetLike (Sylow p G) G + instance : PartialOrder (Sym2 α) := .ofSetLike (Sym2 α) α + instance : PartialOrder (T.CompleteType α) := .ofSetLike (T.CompleteType α) (L[[α]].Sentence) + instance : PartialOrder (TwoSidedIdeal R) := .ofSetLike (TwoSidedIdeal R) R + instance : PartialOrder (ValuationSubring K) := .ofSetLike (ValuationSubring K) K + instance : PartialOrder (VonNeumannAlgebra H) := .ofSetLike (VonNeumannAlgebra H) (H →L[ℂ] H) + instance : PartialOrder (n.Combination α) := .ofSetLike (n.Combination α) α + instance : PartialOrder (tree A) (List A) := .ofSetLike (tree A) (List A) + instance : letI := PartialOrder.ofSetLike A B; IsConcreteLE A B + mem_of_le_of_mem ++ instance : PartialOrder (HomogeneousSubmodule 𝒜 ℳ) := .ofSetLike (HomogeneousSubmodule 𝒜 ℳ) M - instance (priority := 100) instPartialOrder : PartialOrder A

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