priority := low for all IsTwoSided instances but the CommRing one

leanprover-community · Nov 17, 2024 · a3ff84c · a3ff84c
1 parent acca5fd
commit a3ff84c
Show file tree

Hide file tree

Showing 5 changed files with 13 additions and 11 deletions.
diff --git a/Mathlib/RingTheory/Ideal/Basic.lean b/Mathlib/RingTheory/Ideal/Basic.lean
@@ -56,7 +56,7 @@ def pi : Ideal (ι → α) where
 theorem mem_pi (x : ι → α) : x ∈ I.pi ι ↔ ∀ i, x i ∈ I :=
   Iff.rfl
 
-instance [I.IsTwoSided] : (I.pi ι).IsTwoSided :=
+instance (priority := low) [I.IsTwoSided] : (I.pi ι).IsTwoSided :=
   ⟨fun _b hb i ↦ mul_mem_right _ _ (hb i)⟩
 
 end Pi

diff --git a/Mathlib/RingTheory/Ideal/Colon.lean b/Mathlib/RingTheory/Ideal/Colon.lean
@@ -25,7 +25,7 @@ variable {N N₁ N₂ P P₁ P₂ : Submodule R M}
 def colon (N P : Submodule R M) : Ideal R :=
   annihilator (P.map N.mkQ)
 
-instance : (N.colon P).IsTwoSided := inferInstanceAs (annihilator _).IsTwoSided
+instance (priority := low) : (N.colon P).IsTwoSided := inferInstanceAs (annihilator _).IsTwoSided
 
 theorem mem_colon {r} : r ∈ N.colon P ↔ ∀ p ∈ P, r • p ∈ N :=
   mem_annihilator.trans

diff --git a/Mathlib/RingTheory/Ideal/Lattice.lean b/Mathlib/RingTheory/Ideal/Lattice.lean
@@ -32,11 +32,12 @@ namespace Ideal
 
 variable [Semiring α] (I : Ideal α) {a b : α}
 
-instance : IsTwoSided (⊥ : Ideal α) := ⟨fun _ h ↦ by rw [h, zero_mul]; exact zero_mem _⟩
+instance (priority := low) : IsTwoSided (⊥ : Ideal α) :=
+  ⟨fun _ h ↦ by rw [h, zero_mul]; exact zero_mem _⟩
 
-instance : IsTwoSided (⊤ : Ideal α) := ⟨fun _ _ ↦ trivial⟩
+instance (priority := low) : IsTwoSided (⊤ : Ideal α) := ⟨fun _ _ ↦ trivial⟩
 
-instance {ι} (I : ι → Ideal α) [∀ i, (I i).IsTwoSided] : (⨅ i, I i).IsTwoSided :=
+instance (priority := low) {ι} (I : ι → Ideal α) [∀ i, (I i).IsTwoSided] : (⨅ i, I i).IsTwoSided :=
   ⟨fun _ h ↦ (Submodule.mem_iInf _).mpr (mul_mem_right _ _ <| (Submodule.mem_iInf _).mp h ·)⟩
 
 theorem eq_top_of_unit_mem (x y : α) (hx : x ∈ I) (h : y * x = 1) : I = ⊤ :=

diff --git a/Mathlib/RingTheory/Ideal/Maps.lean b/Mathlib/RingTheory/Ideal/Maps.lean
@@ -102,7 +102,7 @@ theorem map_le_comap_of_inverse [RingHomClass G S R] (g : G) (I : Ideal R)
 
 variable [RingHomClass F R S]
 
-instance [K.IsTwoSided] : (comap f K).IsTwoSided :=
+instance (priority := low) [K.IsTwoSided] : (comap f K).IsTwoSided :=
   ⟨fun b ha ↦ by rw [mem_comap, map_mul]; exact mul_mem_right _ _ ha⟩
 
 /-- The `Ideal` version of `Set.preimage_subset_image_of_inverse`. -/
@@ -323,7 +323,7 @@ theorem map_eq_submodule_map (f : R →+* S) [h : RingHomSurjective f] (I : Idea
     I.map f = Submodule.map f.toSemilinearMap I :=
   Submodule.ext fun _ => mem_map_iff_of_surjective f h.1
 
-instance (f : R →+* S) [RingHomSurjective f] (I : Ideal R) [I.IsTwoSided] :
+instance (priority := low) (f : R →+* S) [RingHomSurjective f] (I : Ideal R) [I.IsTwoSided] :
     (I.map f).IsTwoSided where
   mul_mem_of_left b ha := by
     rw [map_eq_submodule_map] at ha ⊢
@@ -581,7 +581,7 @@ variable (f : F) (g : G)
 def ker : Ideal R :=
   Ideal.comap f ⊥
 
-instance : (ker f).IsTwoSided := inferInstanceAs (Ideal.comap f ⊥).IsTwoSided
+instance (priority := low) : (ker f).IsTwoSided := inferInstanceAs (Ideal.comap f ⊥).IsTwoSided
 
 variable {f} in
 /-- An element is in the kernel if and only if it maps to zero. -/
@@ -688,7 +688,8 @@ def Module.annihilator : Ideal R := RingHom.ker (Module.toAddMonoidEnd R M)
 theorem Module.mem_annihilator {r} : r ∈ Module.annihilator R M ↔ ∀ m : M, r • m = 0 :=
   ⟨fun h ↦ (congr($h ·)), (AddMonoidHom.ext ·)⟩
 
-instance : (Module.annihilator R M).IsTwoSided := inferInstanceAs (RingHom.ker _).IsTwoSided
+instance (priority := low) : (Module.annihilator R M).IsTwoSided :=
+  inferInstanceAs (RingHom.ker _).IsTwoSided
 
 theorem LinearMap.annihilator_le_of_injective (f : M →ₗ[R] M') (hf : Function.Injective f) :
     Module.annihilator R M' ≤ Module.annihilator R M := fun x h ↦ by

diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean
@@ -398,14 +398,14 @@ theorem pow_right_mono (e : I ≤ J) (n : ℕ) : I ^ n ≤ J ^ n := by
 
 namespace IsTwoSided
 
-instance [J.IsTwoSided] : (I * J).IsTwoSided :=
+instance (priority := low) [J.IsTwoSided] : (I * J).IsTwoSided :=
   ⟨fun b ha ↦ Submodule.mul_induction_on ha
     (fun i hi j hj ↦ by rw [mul_assoc]; exact mul_mem_mul hi (mul_mem_right _ _ hj))
     fun x y hx hy ↦ by rw [right_distrib]; exact add_mem hx hy⟩
 
 variable [I.IsTwoSided] (m n : ℕ)
 
-instance : (I ^ n).IsTwoSided :=
+instance (priority := low) : (I ^ n).IsTwoSided :=
   n.rec
     (by rw [Submodule.pow_zero, one_eq_top]; infer_instance)
     (fun _ _ ↦ by rw [Submodule.pow_succ]; infer_instance)