feat(Order/FunLike): define `PointwiseLE`

[urkud]

• introduce a mixin class DFunLike.PointwiseLE, use it to define DFunLike.instPartialOrder;
• add a generic DFunLike.orderEmbeddingCoe
• add DFunLike.PointwiseLE instances here and there.

With this refactor and #13022, I'm going to generalize lemmas like MeasureTheory.ae_mono to OuterMeasureClass.

---

• [x] depends on: #12983

[YaelDillies]

I've been working on removing the analogous generic instances for SetLike. What's your motivation here?

[urkud]

What's your motivation? Do you have examples of fun like / set like types where this is not the right order?

I'm going to migrate measures to fun like and some lemmas can be generalized to OuterMeasureClass if the order is given by this definition.

[YaelDillies]

Yes, the typical examples are UpperSet and Filter.

[dupuisf]

This instance scares me a bit. One example where this is the wrong order is linear maps from E →L[ℂ] E to E →L[ℂ] E, where we often want to say that f ≤ g if g - f is completely positive.

[urkud]

@YaelDillies @dupuisf I updated this PR to use a mixin instead.

[urkud]

@YaelDillies @dupuisf I updated this PR to use a mixin instead.

And now I updated commit message.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#12983~~ By Dependent Issues (🤖). Happy coding!

[YaelDillies]

Can you summarise your motivation in the PR description? You're not making anything shorter here, so the motivation can't be "Abstract away some boiler-plate". Do you have the need to reason about several pointwise ordered fun-like types at once?

[YaelDillies]

Okay, I now understand your motivation.

Why can you not make PointwiseLE (+ whatever things you need to hold pointwise) part of OuterMeasureClass?

[urkud]

1. We can drop some lemmas like coe_le_coe, coe_lt_coe, as well as PartialOrder instances. I don't do it in this PR to minimize diff.
2. I plan to add PointwiseOne, PointwiseMul etc, as well as PointwiseSup etc and use them to prove generic algebraic instances, SMul/MulAction/... instances, and *Lattice instances.
3. No other *Class instances assume additional structure on the type. I don't want to break it for one class.

[YaelDillies]

I'm not fully convinced you're not overengineering the solution

[urkud]

Resumed a relevant thread at Zulip