refactor(Algebra): uniform API for substructures

[artie2000]

• Add class for SetLike instances whose map preserves meets - the intended interpretation is substructures whose closure properties are preserved under intersection
• Abstract out the CompleteLattice instance and closure adjunction on such instances

This change unifies a significant part of the API for algebraic substructures.

---

• depends on [Merged by Bors] - refactor: remove order instances from SetLike #32984

Original PR: #25963

[github-actions]

PR summary 6db85f34e4

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
There are 4074 files with changed transitive imports taking up over 186379 characters: this is too many to display!
You can run ci-tools/scripts/pr_summary/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

+ CompleteLattice.ofSetLike
+ CompleteLattice.of_exists_isGLB
+ IsConcreteSInf
+ List.init
+ Props.
+ Shape
+ closure_apply
+ closure_monotone
+ coe_bot
+ coe_closure
+ constrToProp
+ instance : IsConcreteLE A B
+ instance : IsConcreteSInf (Subsemigroup M) M := ⟨fun _ ↦ rfl⟩
+ isGLB_closure
+ listBoolMerge
+ mem_bot
+ mkAndList
+ mkExistsList
+ mkIffOfInductivePropImpl
+ mkOpList
+ mkOrList
+ nCasesProd
+ nCasesSum
+ not_mem_of_not_mem_closure
+ select
+ splitThenConstructor
+ toCases
+ toInductive
+ updateLambdaBinderInfoD!
++ Foo
++ IsSumNonzeroSq
+-+ closure
- notMem_of_notMem_closure

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

[vihdzp]

a) Can you deprecate instead of remove?
b) Should the PR both define IsConcreteSInf and start using it? Or can those be separate concerns?

[artie2000]

the "using it" part is just for testing - I'll mark the PR WIP sorry
defining and using should be separate PRs

[artie2000]

we may not even decide to remove all these declarations (I personally am in favour of removing)
then this PR just means we can stop having to maintain them

[vihdzp]

We should certainly have one PR for just implementing it, and another draft PR which battle tests it.