refactor(Order/OmegaCompletePartialOrder): make Chain a structure

[YaelDillies]

It has a different LE to OrderHom, hence should not be an abbrev.

---

[github-actions]

PR summary 00fca21215

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ coe_map
+ coe_toOrderHom
+ instLE
+ instance : FunLike (Chain α) ℕ α
+ instance : OrderHomClass (Chain α) ℕ α
+ zip_apply
- instance : FunLike (Chain α) ℕ α := inferInstanceAs <| FunLike (ℕ →o α) ℕ α
- instance : LE (Chain α) where le x y := ∀ i, ∃ j, x i ≤ y j
- instance : OrderHomClass (Chain α) ℕ α := inferInstanceAs <| OrderHomClass (ℕ →o α) ℕ α

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]

This mostly looks good, just some questions/comments.

[vihdzp]

Is this comment still relevant? If not, why not use simps here?

[YaelDillies]

No, it isn't relevant anymore because simps! can't see through Chain anymore. I can't use simps here because it generates an _apply lemma instead of a coe_ one, which is what's needed further down. I know about simps -isApplied but unfortunately simps doesn't know that this should change the name from _apply to coe_. Feel free to open an issue about this.

[YaelDillies]

I have opened #37331 for it