perf: de-prioritize Subalgebra.algebra' and `IntermediateField.alge…

…bra'` (#9936) Like in #9655, these instances tend to be slow to fail, so we should assign them a low priority. Zulip discussions: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Algebra.2Eid.20for.20IntermediateField https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Timeout.20in.20Submodule.20.28.F0.9D.93.9E.20K.29.20.28.F0.9D.93.9E.20K.29 Co-authored-by: Anne Baanen <[email protected]>
leanprover-community · Jan 24, 2024 · 725f123 · 725f123
1 parent 4fe0086
commit 725f123
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 2 deletions.
diff --git 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
@@ -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'