diff --git a/Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean b/Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean
index c9c9161f345ea0..8b42732f4943b6 100644
--- a/Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean
+++ b/Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean
@@ -127,11 +127,10 @@ instance isStrictOrder : IsStrictOrder (DegLex (α →₀ ℕ)) (· < ·) where
 
 /-- The linear order on `Finsupp`s obtained by the homogeneous lexicographic ordering. -/
 noncomputable instance : LinearOrder (DegLex (α →₀ ℕ)) :=
-  LinearOrder.lift'
+  fast_instance% LinearOrder.lift'
     (fun (f : DegLex (α →₀ ℕ)) ↦ toLex ((ofDegLex f).degree, toLex (ofDegLex f)))
     (fun f g ↦ by simp)
 
-set_option backward.isDefEq.respectTransparency false in
 theorem le_iff {x y : DegLex (α →₀ ℕ)} :
     x ≤ y ↔ (ofDegLex x).degree < (ofDegLex y).degree ∨
       (ofDegLex x).degree = (ofDegLex y).degree ∧ toLex (ofDegLex x) ≤ toLex (ofDegLex y) := by
@@ -151,7 +150,6 @@ instance : IsOrderedCancelAddMonoid (DegLex (α →₀ ℕ)) where
     rw [le_iff] at h ⊢
     simpa [ofDegLex_add, map_add] using h
 
-set_option backward.isDefEq.respectTransparency false in
 theorem single_strictAnti : StrictAnti (fun (a : α) ↦ toDegLex (single a 1)) := by
   intro _ _ h
   simp only [lt_iff, ofDegLex_toDegLex, degree_single, lt_self_iff_false, Lex.single_lt_iff, h,