chore: remove double instance on CommRing (SeparationQuotient α) (#37481)

sgouezel · sgouezel · commit 3bd2603b817f · 2026-04-01T17:01:08.000Z
We had two different instances giving ` CommRing (SeparationQuotient α)`, defined differently and independently (and non-defeq). This PR removes one of them.

Co-authored-by: sgouezel &lt;sebastien.gouezel@univ-rennes1.fr&gt;
diff --git a/Mathlib/Topology/Algebra/SeparationQuotient/Basic.lean b/Mathlib/Topology/Algebra/SeparationQuotient/Basic.lean
@@ -102,21 +102,21 @@ instance instContinuousMul [Mul M] [ContinuousMul M] : ContinuousMul (Separation
 
 @[to_additive]
 instance instCommMagma [CommMagma M] [ContinuousMul M] : CommMagma (SeparationQuotient M) :=
-  surjective_mk.commMagma mk mk_mul
+  fast_instance% surjective_mk.commMagma mk mk_mul
 
 @[to_additive]
 instance instSemigroup [Semigroup M] [ContinuousMul M] : Semigroup (SeparationQuotient M) :=
-  surjective_mk.semigroup mk mk_mul
+  fast_instance% surjective_mk.semigroup mk mk_mul
 
 @[to_additive]
 instance instCommSemigroup [CommSemigroup M] [ContinuousMul M] :
     CommSemigroup (SeparationQuotient M) :=
-  surjective_mk.commSemigroup mk mk_mul
+  fast_instance% surjective_mk.commSemigroup mk mk_mul
 
 @[to_additive]
 instance instMulOneClass [MulOneClass M] [ContinuousMul M] :
     MulOneClass (SeparationQuotient M) :=
-  surjective_mk.mulOneClass mk mk_one mk_mul
+  fast_instance% surjective_mk.mulOneClass mk mk_one mk_mul
 
 /-- `SeparationQuotient.mk` as a `MonoidHom`. -/
 @[to_additive (attr := simps) /-- `SeparationQuotient.mk` as an `AddMonoidHom`. -/]
@@ -138,11 +138,11 @@ theorem mk_pow [Monoid M] [ContinuousMul M] (x : M) (n : ℕ) : mk (x ^ n) = (mk
 
 @[to_additive]
 instance instMonoid [Monoid M] [ContinuousMul M] : Monoid (SeparationQuotient M) :=
-  surjective_mk.monoid mk mk_one mk_mul mk_pow
+  fast_instance% surjective_mk.monoid mk mk_one mk_mul mk_pow
 
 @[to_additive]
 instance instCommMonoid [CommMonoid M] [ContinuousMul M] : CommMonoid (SeparationQuotient M) :=
-  surjective_mk.commMonoid mk mk_one mk_mul mk_pow
+  fast_instance% surjective_mk.commMonoid mk mk_one mk_mul mk_pow
 
 end Monoid
 
@@ -194,11 +194,11 @@ theorem mk_zpow [Group G] [IsTopologicalGroup G] (x : G) (n : ℤ) : mk (x ^ n)
 
 @[to_additive]
 instance instGroup [Group G] [IsTopologicalGroup G] : Group (SeparationQuotient G) :=
-  surjective_mk.group mk mk_one mk_mul mk_inv mk_div mk_pow mk_zpow
+  fast_instance% surjective_mk.group mk mk_one mk_mul mk_inv mk_div mk_pow mk_zpow
 
 @[to_additive]
 instance instCommGroup [CommGroup G] [IsTopologicalGroup G] : CommGroup (SeparationQuotient G) :=
-  surjective_mk.commGroup mk mk_one mk_mul mk_inv mk_div mk_pow mk_zpow
+  fast_instance% surjective_mk.commGroup mk mk_one mk_mul mk_inv mk_div mk_pow mk_zpow
 
 @[to_additive]
 instance instIsTopologicalGroup [Group G] [IsTopologicalGroup G] :
@@ -223,23 +223,23 @@ variable {M₀ : Type*} [TopologicalSpace M₀]
 
 instance instMulZeroClass [MulZeroClass M₀] [ContinuousMul M₀] :
     MulZeroClass (SeparationQuotient M₀) :=
-  surjective_mk.mulZeroClass mk mk_zero mk_mul
+  fast_instance% surjective_mk.mulZeroClass mk mk_zero mk_mul
 
 instance instSemigroupWithZero [SemigroupWithZero M₀] [ContinuousMul M₀] :
     SemigroupWithZero (SeparationQuotient M₀) :=
-  surjective_mk.semigroupWithZero mk mk_zero mk_mul
+  fast_instance% surjective_mk.semigroupWithZero mk mk_zero mk_mul
 
 instance instMulZeroOneClass [MulZeroOneClass M₀] [ContinuousMul M₀] :
     MulZeroOneClass (SeparationQuotient M₀) :=
-  surjective_mk.mulZeroOneClass mk mk_zero mk_one mk_mul
+  fast_instance% surjective_mk.mulZeroOneClass mk mk_zero mk_one mk_mul
 
 instance instMonoidWithZero [MonoidWithZero M₀] [ContinuousMul M₀] :
     MonoidWithZero (SeparationQuotient M₀) :=
-  surjective_mk.monoidWithZero mk mk_zero mk_one mk_mul mk_pow
+  fast_instance% surjective_mk.monoidWithZero mk mk_zero mk_one mk_mul mk_pow
 
 instance instCommMonoidWithZero [CommMonoidWithZero M₀] [ContinuousMul M₀] :
     CommMonoidWithZero (SeparationQuotient M₀) :=
-  surjective_mk.commMonoidWithZero mk mk_zero mk_one mk_mul mk_pow
+  fast_instance% surjective_mk.commMonoidWithZero mk mk_zero mk_one mk_mul mk_pow
 
 end MonoidWithZero
 
@@ -249,7 +249,7 @@ variable {R : Type*} [TopologicalSpace R]
 
 instance instDistrib [Distrib R] [ContinuousMul R] [ContinuousAdd R] :
     Distrib (SeparationQuotient R) :=
-  surjective_mk.distrib mk mk_add mk_mul
+  fast_instance% surjective_mk.distrib mk mk_add mk_mul
 
 instance instLeftDistribClass [Mul R] [Add R] [LeftDistribClass R]
     [ContinuousMul R] [ContinuousAdd R] :
@@ -263,11 +263,14 @@ instance instRightDistribClass [Mul R] [Add R] [RightDistribClass R]
 
 instance instNonUnitalnonAssocSemiring [NonUnitalNonAssocSemiring R]
     [IsTopologicalSemiring R] : NonUnitalNonAssocSemiring (SeparationQuotient R) :=
-  surjective_mk.nonUnitalNonAssocSemiring mk mk_zero mk_add mk_mul mk_smul
+  fast_instance% surjective_mk.nonUnitalNonAssocSemiring mk mk_zero mk_add mk_mul mk_smul
+
+instance instIsTopologicalSemiring [NonUnitalNonAssocSemiring R] [IsTopologicalSemiring R] :
+    IsTopologicalSemiring (SeparationQuotient R) where
 
 instance instNonUnitalSemiring [NonUnitalSemiring R] [IsTopologicalSemiring R] :
     NonUnitalSemiring (SeparationQuotient R) :=
-  surjective_mk.nonUnitalSemiring mk mk_zero mk_add mk_mul mk_smul
+  fast_instance% surjective_mk.nonUnitalSemiring mk mk_zero mk_add mk_mul mk_smul
 
 instance instNatCast [NatCast R] : NatCast (SeparationQuotient R) where
   natCast n := mk n
@@ -288,59 +291,66 @@ theorem mk_intCast [IntCast R] (n : ℤ) : mk (n : R) = n := rfl
 
 instance instNonAssocSemiring [NonAssocSemiring R] [IsTopologicalSemiring R] :
     NonAssocSemiring (SeparationQuotient R) :=
-  surjective_mk.nonAssocSemiring mk mk_zero mk_one mk_add mk_mul mk_smul mk_natCast
+  fast_instance% surjective_mk.nonAssocSemiring mk mk_zero mk_one mk_add mk_mul mk_smul mk_natCast
 
 instance instNonUnitalNonAssocRing [NonUnitalNonAssocRing R] [IsTopologicalRing R] :
     NonUnitalNonAssocRing (SeparationQuotient R) :=
-  surjective_mk.nonUnitalNonAssocRing mk mk_zero mk_add mk_mul mk_neg mk_sub mk_smul mk_smul
+  fast_instance% surjective_mk.nonUnitalNonAssocRing mk mk_zero mk_add mk_mul mk_neg mk_sub
+    mk_smul mk_smul
+
+instance instIsTopologicalRing [NonUnitalNonAssocRing R] [IsTopologicalRing R] :
+    IsTopologicalRing (SeparationQuotient R) where
 
 instance instNonUnitalRing [NonUnitalRing R] [IsTopologicalRing R] :
     NonUnitalRing (SeparationQuotient R) :=
-  surjective_mk.nonUnitalRing mk mk_zero mk_add mk_mul mk_neg mk_sub mk_smul mk_smul
+  fast_instance% surjective_mk.nonUnitalRing mk mk_zero mk_add mk_mul mk_neg mk_sub mk_smul mk_smul
 
 instance instNonAssocRing [NonAssocRing R] [IsTopologicalRing R] :
     NonAssocRing (SeparationQuotient R) :=
-  surjective_mk.nonAssocRing mk mk_zero mk_one mk_add mk_mul mk_neg mk_sub mk_smul mk_smul
-    mk_natCast mk_intCast
+  fast_instance% surjective_mk.nonAssocRing mk mk_zero mk_one mk_add mk_mul mk_neg mk_sub
+    mk_smul mk_smul mk_natCast mk_intCast
 
 instance instSemiring [Semiring R] [IsTopologicalSemiring R] :
     Semiring (SeparationQuotient R) :=
-  surjective_mk.semiring mk mk_zero mk_one mk_add mk_mul mk_smul mk_pow mk_natCast
+  fast_instance% surjective_mk.semiring mk mk_zero mk_one mk_add mk_mul mk_smul mk_pow mk_natCast
 
 instance instRing [Ring R] [IsTopologicalRing R] :
     Ring (SeparationQuotient R) :=
-  surjective_mk.ring mk mk_zero mk_one mk_add mk_mul mk_neg mk_sub mk_smul mk_smul mk_pow
-    mk_natCast mk_intCast
+  fast_instance% surjective_mk.ring mk mk_zero mk_one mk_add mk_mul mk_neg mk_sub mk_smul
+    mk_smul mk_pow mk_natCast mk_intCast
 
 instance instNonUnitalNonAssocCommSemiring [NonUnitalNonAssocCommSemiring R]
     [IsTopologicalSemiring R] :
     NonUnitalNonAssocCommSemiring (SeparationQuotient R) :=
-  surjective_mk.nonUnitalNonAssocCommSemiring mk mk_zero mk_add mk_mul mk_smul
+  fast_instance% surjective_mk.nonUnitalNonAssocCommSemiring mk mk_zero mk_add mk_mul mk_smul
 
 instance instNonUnitalCommSemiring [NonUnitalCommSemiring R] [IsTopologicalSemiring R] :
     NonUnitalCommSemiring (SeparationQuotient R) :=
-  surjective_mk.nonUnitalCommSemiring mk mk_zero mk_add mk_mul mk_smul
+  fast_instance% surjective_mk.nonUnitalCommSemiring mk mk_zero mk_add mk_mul mk_smul
 
 instance instCommSemiring [CommSemiring R] [IsTopologicalSemiring R] :
     CommSemiring (SeparationQuotient R) :=
-  surjective_mk.commSemiring mk mk_zero mk_one mk_add mk_mul mk_smul mk_pow mk_natCast
+  fast_instance% surjective_mk.commSemiring mk mk_zero mk_one mk_add mk_mul mk_smul
+    mk_pow mk_natCast
 
 instance instHasDistribNeg [Mul R] [HasDistribNeg R] [ContinuousMul R] [ContinuousNeg R] :
     HasDistribNeg (SeparationQuotient R) :=
-  surjective_mk.hasDistribNeg mk mk_neg mk_mul
+  fast_instance% surjective_mk.hasDistribNeg mk mk_neg mk_mul
 
 instance instNonUnitalNonAssocCommRing [NonUnitalNonAssocCommRing R] [IsTopologicalRing R] :
     NonUnitalNonAssocCommRing (SeparationQuotient R) :=
-  surjective_mk.nonUnitalNonAssocCommRing mk mk_zero mk_add mk_mul mk_neg mk_sub mk_smul mk_smul
+  fast_instance% surjective_mk.nonUnitalNonAssocCommRing mk mk_zero mk_add mk_mul mk_neg mk_sub
+    mk_smul mk_smul
 
 instance instNonUnitalCommRing [NonUnitalCommRing R] [IsTopologicalRing R] :
     NonUnitalCommRing (SeparationQuotient R) :=
-  surjective_mk.nonUnitalCommRing mk mk_zero mk_add mk_mul mk_neg mk_sub mk_smul mk_smul
+  fast_instance% surjective_mk.nonUnitalCommRing mk mk_zero mk_add mk_mul mk_neg mk_sub
+    mk_smul mk_smul
 
 instance instCommRing [CommRing R] [IsTopologicalRing R] :
     CommRing (SeparationQuotient R) :=
-  surjective_mk.commRing mk mk_zero mk_one mk_add mk_mul mk_neg mk_sub mk_smul mk_smul mk_pow
-    mk_natCast mk_intCast
+  fast_instance% surjective_mk.commRing mk mk_zero mk_one mk_add mk_mul mk_neg mk_sub
+    mk_smul mk_smul mk_pow mk_natCast mk_intCast
 
 /-- `SeparationQuotient.mk` as a `RingHom`. -/
 @[simps]
@@ -357,17 +367,17 @@ variable {M A : Type*} [TopologicalSpace A]
 instance instDistribSMul [AddZeroClass A] [DistribSMul M A]
     [ContinuousAdd A] [ContinuousConstSMul M A] :
     DistribSMul M (SeparationQuotient A) :=
-  surjective_mk.distribSMul mkAddMonoidHom mk_smul
+  fast_instance% surjective_mk.distribSMul mkAddMonoidHom mk_smul
 
 instance instDistribMulAction [Monoid M] [AddMonoid A] [DistribMulAction M A]
     [ContinuousAdd A] [ContinuousConstSMul M A] :
     DistribMulAction M (SeparationQuotient A) :=
-  surjective_mk.distribMulAction mkAddMonoidHom mk_smul
+  fast_instance% surjective_mk.distribMulAction mkAddMonoidHom mk_smul
 
 instance instMulDistribMulAction [Monoid M] [Monoid A] [MulDistribMulAction M A]
     [ContinuousMul A] [ContinuousConstSMul M A] :
     MulDistribMulAction M (SeparationQuotient A) :=
-  surjective_mk.mulDistribMulAction mkMonoidHom mk_smul
+  fast_instance% surjective_mk.mulDistribMulAction mkMonoidHom mk_smul
 
 end DistribSMul
 
@@ -379,7 +389,7 @@ variable {R S M N : Type*} [Semiring R] [AddCommMonoid M] [Module R M]
     [TopologicalSpace N]
 
 instance instModule : Module R (SeparationQuotient M) :=
-  surjective_mk.module R mkAddMonoidHom mk_smul
+  fast_instance% surjective_mk.module R mkAddMonoidHom mk_smul
 
 variable (R M)
 
diff --git a/Mathlib/Topology/Algebra/UniformRing.lean b/Mathlib/Topology/Algebra/UniformRing.lean
@@ -11,6 +11,7 @@ public import Mathlib.Algebra.Ring.TransferInstance
 public import Mathlib.Topology.Algebra.GroupCompletion
 public import Mathlib.Topology.Algebra.Ring.Ideal
 public import Mathlib.Topology.Algebra.IsUniformGroup.Basic
+public import Mathlib.Topology.Algebra.SeparationQuotient.Basic
 
 /-!
 # Completion of topological rings:
@@ -239,34 +240,22 @@ theorem inseparableSetoid_ring (α) [Ring α] [TopologicalSpace α] [IsTopologic
 /-- Given a topological ring `α` equipped with a uniform structure that makes subtraction uniformly
 continuous, get a homeomorphism between the separated quotient of `α` and the quotient ring
 corresponding to the closure of zero. -/
-def sepQuotHomeomorphRingQuot (α) [CommRing α] [TopologicalSpace α] [IsTopologicalRing α] :
+def sepQuotHomeomorphRingQuot (α) [Ring α] [TopologicalSpace α] [IsTopologicalRing α] :
     SeparationQuotient α ≃ₜ α ⧸ (⊥ : Ideal α).closure where
   toEquiv := Quotient.congrRight fun x y => by rw [inseparableSetoid_ring]
   continuous_toFun := continuous_id.quotient_map' <| by
     rw [inseparableSetoid_ring]; exact fun _ _ ↦ id
   continuous_invFun := continuous_id.quotient_map' <| by
     rw [inseparableSetoid_ring]; exact fun _ _ ↦ id
 
-instance commRing [CommRing α] [TopologicalSpace α] [IsTopologicalRing α] :
-    CommRing (SeparationQuotient α) :=
-  (sepQuotHomeomorphRingQuot _).commRing
-
 /-- Given a topological ring `α` equipped with a uniform structure that makes subtraction uniformly
 continuous, get an equivalence between the separated quotient of `α` and the quotient ring
 corresponding to the closure of zero. -/
 def sepQuotRingEquivRingQuot (α) [CommRing α] [TopologicalSpace α] [IsTopologicalRing α] :
-    SeparationQuotient α ≃+* α ⧸ (⊥ : Ideal α).closure :=
-  (sepQuotHomeomorphRingQuot _).ringEquiv
-
-instance topologicalRing [CommRing α] [TopologicalSpace α] [IsTopologicalRing α] :
-    IsTopologicalRing (SeparationQuotient α) where
-  toContinuousAdd :=
-    (sepQuotHomeomorphRingQuot α).isInducing.continuousAdd (sepQuotRingEquivRingQuot α)
-  toContinuousMul :=
-    (sepQuotHomeomorphRingQuot α).isInducing.continuousMul (sepQuotRingEquivRingQuot α)
-  toContinuousNeg :=
-    (sepQuotHomeomorphRingQuot α).isInducing.continuousNeg <|
-      map_neg (sepQuotRingEquivRingQuot α)
+    SeparationQuotient α ≃+* α ⧸ (⊥ : Ideal α).closure where
+  __ := sepQuotHomeomorphRingQuot α
+  map_mul' := SeparationQuotient.surjective_mk.forall₂.2 (fun _ _ ↦ rfl)
+  map_add' := SeparationQuotient.surjective_mk.forall₂.2 (fun _ _ ↦ rfl)
 
 end UniformSpace
 
