From a9ecd67750b97fe53018b24c9b6f21a46853c1d4 Mon Sep 17 00:00:00 2001
From: erd1 <the.erd.one@gmail.com>
Date: Mon, 27 Nov 2023 21:16:22 +0800
Subject: [PATCH] remove bad instances

---
 FltRegular/NumberTheory/AuxLemmas.lean     | 20 ++++++++++----------
 FltRegular/NumberTheory/Different.lean     |  2 ++
 FltRegular/NumberTheory/IdealNorm.lean     |  2 ++
 FltRegular/NumberTheory/QuotientTrace.lean |  3 +++
 FltRegular/NumberTheory/Unramified.lean    |  2 ++
 5 files changed, 19 insertions(+), 10 deletions(-)

diff --git a/FltRegular/NumberTheory/AuxLemmas.lean b/FltRegular/NumberTheory/AuxLemmas.lean
index f1b6903a..00009d8c 100644
--- a/FltRegular/NumberTheory/AuxLemmas.lean
+++ b/FltRegular/NumberTheory/AuxLemmas.lean
@@ -475,16 +475,16 @@ lemma inv_le_comm (hI : I ≠ 0) (hJ : J ≠ 0) : I⁻¹ ≤ J ↔ J⁻¹ ≤ I
 
 end FractionalIdeal
 
--- Mathlib/RingTheory/Localization/FractionRing.lean
-noncomputable
-instance {A B} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDomain B]
-    [NoZeroSMulDivisors A B] : Algebra (FractionRing A) (FractionRing B) :=
-  FractionRing.liftAlgebra A _
-
--- Mathlib/RingTheory/Localization/FractionRing.lean
-instance {A B} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDomain B]
-    [NoZeroSMulDivisors A B] : IsScalarTower A (FractionRing A) (FractionRing B) :=
-  FractionRing.isScalarTower_liftAlgebra _ _
+-- -- Mathlib/RingTheory/Localization/FractionRing.lean
+-- noncomputable
+-- instance {A B} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDomain B]
+--     [NoZeroSMulDivisors A B] : Algebra (FractionRing A) (FractionRing B) :=
+--   FractionRing.liftAlgebra A _
+
+-- -- Mathlib/RingTheory/Localization/FractionRing.lean
+-- instance {A B} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDomain B]
+--     [NoZeroSMulDivisors A B] : IsScalarTower A (FractionRing A) (FractionRing B) :=
+--   FractionRing.isScalarTower_liftAlgebra _ _
 
 open nonZeroDivisors
 section
diff --git a/FltRegular/NumberTheory/Different.lean b/FltRegular/NumberTheory/Different.lean
index 988ae9d9..2684a748 100644
--- a/FltRegular/NumberTheory/Different.lean
+++ b/FltRegular/NumberTheory/Different.lean
@@ -25,6 +25,8 @@ import Mathlib.NumberTheory.KummerDedekind
 -/
 universe u
 
+attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
+
 variable (A K) {B} {L : Type u} [CommRing A] [Field K] [CommRing B] [Field L]
 variable [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L]
 variable [IsScalarTower A K L] [IsScalarTower A B L]
diff --git a/FltRegular/NumberTheory/IdealNorm.lean b/FltRegular/NumberTheory/IdealNorm.lean
index ed233d6e..9e2e8258 100644
--- a/FltRegular/NumberTheory/IdealNorm.lean
+++ b/FltRegular/NumberTheory/IdealNorm.lean
@@ -14,6 +14,8 @@ Generalizes `Ideal.spanNorm` in `Mathlib/RingTheory/Ideal/Norm.lean` to non-free
 -/
 open scoped nonZeroDivisors
 
+attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
+
 section intNorm
 
 universe u v w
diff --git a/FltRegular/NumberTheory/QuotientTrace.lean b/FltRegular/NumberTheory/QuotientTrace.lean
index 1a10bd2b..85d4cb93 100644
--- a/FltRegular/NumberTheory/QuotientTrace.lean
+++ b/FltRegular/NumberTheory/QuotientTrace.lean
@@ -15,6 +15,9 @@ import FltRegular.NumberTheory.AuxLemmas
   The trace map on `B → A` coincides with the trace map on `B⧸pB → A⧸p`.
 
 -/
+
+attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
+
 section LocalRing
 
 variable {R S} [CommRing R] [CommRing S] [Algebra R S] [LocalRing R] [Module.Free R S] [Module.Finite R S]
diff --git a/FltRegular/NumberTheory/Unramified.lean b/FltRegular/NumberTheory/Unramified.lean
index f5644987..8db49674 100644
--- a/FltRegular/NumberTheory/Unramified.lean
+++ b/FltRegular/NumberTheory/Unramified.lean
@@ -19,6 +19,8 @@ import FltRegular.NumberTheory.Different
 -/
 open BigOperators UniqueFactorizationMonoid
 
+attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
+
 variable (R K S L : Type*) [CommRing R] [CommRing S] [Algebra R S] [Field K] [Field L]
     [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] [Algebra S L] -- [IsFractionRing S L]
     [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] -- [IsNoetherian R S]