chore(order/preorder_hom): more homs, golf a few proofs (#9256)

### New `preorder_hom`s

* `preorder_hom.curry`: an order isomorphism between `α × β →ₘ γ` and `α →ₘ β →ₘ γ`;
* `preorder_hom.compₘ`: a fully bundled version of `preorder_hom.comp`;
* `preorder_hom.prodₘ`: a fully bundled version of `preorder_hom.prod`;
* `preorder_hom.prod_iso`: Order isomorphism between the space of
  monotone maps to `β × γ` and the product of the spaces +of monotone
  maps to `β` and `γ`;
* `preorder_hom.pi`: construct a bundled monotone map `α →ₘ Π i, π i`
  from a family of monotone maps +`f i : α →ₘ π i`;
* `preorder_hom.pi_iso`: same thing, as an `order_iso`;
* `preorder_hom.dual`: interpret `f : α →ₘ β` as `order_dual α →ₘ order_dual β`;
* `preorder_hom.dual_iso`: same as an `order_iso` (with one more
  `order_dual` to get a monotone map, not an antitone map);

### Renamed/moved `preorder_hom`s

The following `preorder_hom`s were renamed and/or moved from
`order.omega_complete_partial_order` to `order.preorder_hom`.

* `preorder_hom.const` : moved, bundle as `β →ₘ α →ₘ β`;
* `preorder_hom.prod.diag` : `preorder_hom.diag`;
* `preorder_hom.prod.map` : `preorder_hom.prod_map`;
* `preorder_hom.prod.fst` : `preorder_hom.fst`;
* `preorder_hom.prod.snd` : `preorder_hom.snd`;
* `preorder_hom.prod.zip` : `preorder_hom.prod`;
* `pi.monotone_apply` : `pi.eval_preorder_hom`;
* `preorder_hom.monotone_apply` : `preorder_hom.apply`;
* `preorder_hom.to_fun_hom` : moved.

### Other changes

* add an instance `can_lift (α → β) (α →ₘ β)`;
- rename `omega_complete_partial_order.continuous.to_monotone` to
  `omega_complete_partial_order.continuous'.to_monotone` to enable dot
  notation, same with
  `omega_complete_partial_order.continuous.to_bundled`;
* use `order_dual` to get some proofs;
* golf some proofs;
* redefine `has_Inf.Inf` and `has_Sup.Sup` using `infi`/`supr`;
* generalize some `mono` lemmas;
* use notation `→ₘ`.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/control/lawful_fix.lean

@@ -39,7 +39,7 @@ class lawful_fix (α : Type*) [omega_complete_partial_order α] extends has_fix
 lemma lawful_fix.fix_eq' {α} [omega_complete_partial_order α] [lawful_fix α]
   {f : α → α} (hf : continuous' f) :
   has_fix.fix f = f (has_fix.fix f) :=
-lawful_fix.fix_eq (continuous.to_bundled _ hf)
+lawful_fix.fix_eq (hf.to_bundled _)
 
 namespace part
 

src/order/category/omega_complete_partial_order.lean

@@ -58,7 +58,7 @@ namespace has_products
 
 /-- The pi-type gives a cone for a product. -/
 def product {J : Type v} (f : J → ωCPO.{v}) : fan f :=
-fan.mk (of (Π j, f j)) (λ j, continuous_hom.of_mono (pi.monotone_apply j : _) (λ c, rfl))
+fan.mk (of (Π j, f j)) (λ j, continuous_hom.of_mono (pi.eval_preorder_hom j) (λ c, rfl))
 
 /-- The pi-type is a limit cone for the product. -/
 def is_product (J : Type v) (f : J → ωCPO) : is_limit (product f) :=

src/order/closure.lean

@@ -74,8 +74,7 @@ variable [partial_order α]
 /-- The identity function as a closure operator. -/
 @[simps]
 def id : closure_operator α :=
-{ to_fun := λ x, x,
-  monotone' := λ _ _ h, h,
+{ to_preorder_hom := preorder_hom.id,
   le_closure' := λ _, le_rfl,
   idempotent' := λ _, rfl }