diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean b/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
index 32b947810285b..6412c8eb9bad4 100644
--- a/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
+++ b/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
@@ -371,7 +371,14 @@ instance : Module R S :=
 instance [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] : IsScalarTower R' R S :=
   inferInstanceAs (IsScalarTower R' R (toSubmodule S))
 
-instance algebra' [CommSemiring R'] [SMul R' R] [Algebra R' A] [IsScalarTower R' R A] :
+/- More general form of `Subalgebra.algebra`.
+
+This instance should have low priority since it is slow to fail:
+before failing, it will cause a search through all `SMul R' R` instances,
+which can quickly get expensive.
+-/
+instance (priority := 500) algebra' [CommSemiring R'] [SMul R' R] [Algebra R' A]
+    [IsScalarTower R' R A] :
     Algebra R' S :=
   { (algebraMap R' A).codRestrict S fun x => by
       rw [Algebra.algebraMap_eq_smul_one, ← smul_one_smul R x (1 : A), ←
diff --git a/Mathlib/FieldTheory/IntermediateField.lean b/Mathlib/FieldTheory/IntermediateField.lean
index ff300c72dfc1b..68b33d28ea1e9 100644
--- a/Mathlib/FieldTheory/IntermediateField.lean
+++ b/Mathlib/FieldTheory/IntermediateField.lean
@@ -374,7 +374,14 @@ theorem coe_smul {R} [Semiring R] [SMul R K] [Module R L] [IsScalarTower R K L]
   rfl
 #align intermediate_field.coe_smul IntermediateField.coe_smul
 
-instance algebra' {K'} [CommSemiring K'] [SMul K' K] [Algebra K' L] [IsScalarTower K' K L] :
+/- More general form of `IntermediateField.algebra`.
+
+This instance should have low priority since it is slow to fail:
+before failing, it will cause a search through all `SMul K' K` instances,
+which can quickly get expensive.
+-/
+instance (priority := 500) algebra' {K'} [CommSemiring K'] [SMul K' K] [Algebra K' L]
+    [IsScalarTower K' K L] :
     Algebra K' S :=
   S.toSubalgebra.algebra'
 #align intermediate_field.algebra' IntermediateField.algebra'