chore(Data/Prod/Lex): remove backward.isDefEq.respectTransparency (#41838)

Clean up some `respectTransparency` tech debt.

Author: JovanGerb

Mathlib/Data/Prod/Lex.lean

@@ -181,13 +181,11 @@ theorem _root_.lexOrd_eq [Ord α] [Ord β] : @lexOrd α β _ _ = instOrdLexProd
 
 theorem _root_.Ord.lex_eq [oα : Ord α] [oβ : Ord β] : Ord.lex oα oβ = instOrdLexProd := rfl
 
-set_option backward.isDefEq.respectTransparency false in
 instance [Ord α] [Ord β] [Std.OrientedOrd α] [Std.OrientedOrd β] : Std.OrientedOrd (α ×ₗ β) :=
-  inferInstanceAs (Std.OrientedCmp (compareLex _ _))
+  inferInstanceAs (@Std.OrientedCmp (α × β) (compareLex _ _))
 
-set_option backward.isDefEq.respectTransparency false in
 instance [Ord α] [Ord β] [Std.TransOrd α] [Std.TransOrd β] : Std.TransOrd (α ×ₗ β) :=
-  inferInstanceAs (Std.TransCmp (compareLex _ _))
+  inferInstanceAs (@Std.TransCmp (α × β) (compareLex _ _))
 
 /-- Dictionary / lexicographic linear order for pairs. -/
 instance instLinearOrder (α β : Type*) [LinearOrder α] [LinearOrder β] : LinearOrder (α ×ₗ β) where