diff --git a/Mathlib/Algebra/EuclideanDomain/Field.lean b/Mathlib/Algebra/EuclideanDomain/Field.lean
index 3ba135fab0f1ae..b9ca7ccf17e034 100644
--- a/Mathlib/Algebra/EuclideanDomain/Field.lean
+++ b/Mathlib/Algebra/EuclideanDomain/Field.lean
@@ -9,6 +9,8 @@ public import Mathlib.Algebra.EuclideanDomain.Defs
 public import Mathlib.Algebra.Field.Defs
 public import Mathlib.Algebra.GroupWithZero.Units.Basic
 
+import Mathlib.Tactic.FastInstance
+
 /-!
 # Instances for Euclidean domains
 * `Field.toEuclideanDomain`: shows that any field is a Euclidean domain.
@@ -21,7 +23,7 @@ namespace Field
 variable {K : Type*} [Field K]
 
 -- see Note [lower instance priority]
-instance (priority := 100) toEuclideanDomain : EuclideanDomain K :=
+instance (priority := 100) toEuclideanDomain : EuclideanDomain K := fast_instance%
 { toCommRing := toCommRing
   quotient := (· / ·), remainder := fun a b => a - a * b / b, quotient_zero := div_zero,
   quotient_mul_add_remainder_eq := fun a b => by