chore: remove workarounds for lean4#1891 (#9290)

We no longer need to explicitly specify the `Monotone` and `StrictMono` arguments, after leanprover/lean4@069873d fixed leanprover/lean4#1891.

Compare to the mathlib3 declarations:
https://github.com/leanprover-community/mathlib/blob/65a1391a0106c9204fe45bc73a039f056558cb83/src/data/prod/lex.lean#L93-L107

Author: dwrensha

Mathlib/Data/Prod/Lex.lean

@@ -108,22 +108,14 @@ section Preorder
 
 variable [PartialOrder α] [Preorder β]
 
--- porting note: type class search sees right through the type synonrm for `α ×ₗ β` and uses the
--- `Preorder` structure for `α × β` instead
--- This is hopefully the same problems as in https://github.com/leanprover/lean4/issues/1891
--- and will be fixed in nightly-2022-11-30
-theorem toLex_mono : @Monotone _ _ _ (Prod.Lex.preorder α β) (toLex : α × β → α ×ₗ β) := by
+theorem toLex_mono : Monotone (toLex : α × β → α ×ₗ β) := by
   rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ ⟨ha, hb⟩
   obtain rfl | ha : a₁ = a₂ ∨ _ := ha.eq_or_lt
   · exact right _ hb
   · exact left _ _ ha
 #align prod.lex.to_lex_mono Prod.Lex.toLex_mono
 
--- porting note: type class search sees right through the type synonrm for `α ×ₗ β` and uses the
--- `Preorder` structure for `α × β` instead
--- This is hopefully the same problems as in https://github.com/leanprover/lean4/issues/1891
--- and will be fixed in nightly-2022-11-30
-theorem toLex_strictMono : @StrictMono _ _ _ (Prod.Lex.preorder α β) (toLex : α × β → α ×ₗ β) := by
+theorem toLex_strictMono : StrictMono (toLex : α × β → α ×ₗ β) := by
   rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ h
   obtain rfl | ha : a₁ = a₂ ∨ _ := h.le.1.eq_or_lt
   · exact right _ (Prod.mk_lt_mk_iff_right.1 h)