From cb31b2be7fae661b896dc1ba16c0103d760ecab4 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Tue, 12 May 2026 18:45:28 +0100 Subject: [PATCH 1/2] perf(Algebra/EuclideanDomain/Defs): prio decrease of EuclideanDomain.toCommRing --- Mathlib/Algebra/EuclideanDomain/Defs.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Mathlib/Algebra/EuclideanDomain/Defs.lean b/Mathlib/Algebra/EuclideanDomain/Defs.lean index 35621d3926a756..c1ffa901e8ad22 100644 --- a/Mathlib/Algebra/EuclideanDomain/Defs.lean +++ b/Mathlib/Algebra/EuclideanDomain/Defs.lean @@ -93,6 +93,9 @@ class EuclideanDomain (R : Type u) extends CommRing R, Nontrivial R where /-- An additional constraint on `r`. -/ mul_left_not_lt : ∀ (a) {b}, b ≠ 0 → ¬r (a * b) a +-- see Note [lower instance priority] +attribute [instance 100] EuclideanDomain.toCommRing + namespace EuclideanDomain variable {R : Type u} [EuclideanDomain R] From 84f381f6bbfe97b10d95d6f0f45b7c993cd81225 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Tue, 12 May 2026 22:42:18 +0100 Subject: [PATCH 2/2] add comment explaining why instance prio is being lowered --- Mathlib/Algebra/EuclideanDomain/Defs.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Mathlib/Algebra/EuclideanDomain/Defs.lean b/Mathlib/Algebra/EuclideanDomain/Defs.lean index c1ffa901e8ad22..48bf83f21c91ab 100644 --- a/Mathlib/Algebra/EuclideanDomain/Defs.lean +++ b/Mathlib/Algebra/EuclideanDomain/Defs.lean @@ -93,6 +93,14 @@ class EuclideanDomain (R : Type u) extends CommRing R, Nontrivial R where /-- An additional constraint on `r`. -/ mul_left_not_lt : ∀ (a) {b}, b ≠ 0 → ¬r (a * b) a +/- +Lean has far more theorems about fields than about Euclidean domains. We thus +lower the priority of `Euclideandomain.toCommRing`, encouraging typeclass inference +to try `Field.toCommRing` first. Without this priority-lowering, typeclass inference +finds the more inefficient path `Field.toEuclideanDomain.toCommRing` by default. This +priority change saves over 500G instructions across mathlib. See +https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/We.20need.20to.20talk.20about.20Euclidean.20Domains/near/594655420 +-/ -- see Note [lower instance priority] attribute [instance 100] EuclideanDomain.toCommRing