From 006c0fc200f2f3c6e3fc3cce6408716a0b428b64 Mon Sep 17 00:00:00 2001
From: Jireh Loreaux <loreaujy@gmail.com>
Date: Mon, 11 Nov 2024 03:06:20 +0000
Subject: [PATCH] chore: change `comm*TopologicalClosure` from `def` to
 `abbrev` (#18766)

---
 Mathlib/Topology/Algebra/Algebra.lean     |  6 ++++--
 Mathlib/Topology/Algebra/Group/Basic.lean | 10 +++++++---
 Mathlib/Topology/Algebra/Monoid.lean      |  6 ++++--
 Mathlib/Topology/Algebra/Ring/Basic.lean  | 14 +++++++++-----
 4 files changed, 24 insertions(+), 12 deletions(-)

diff --git a/Mathlib/Topology/Algebra/Algebra.lean b/Mathlib/Topology/Algebra/Algebra.lean
index 18a21636f61e4..5a979a611553c 100644
--- a/Mathlib/Topology/Algebra/Algebra.lean
+++ b/Mathlib/Topology/Algebra/Algebra.lean
@@ -555,8 +555,10 @@ theorem Subalgebra.topologicalClosure_minimal (s : Subalgebra R A) {t : Subalgeb
     (ht : IsClosed (t : Set A)) : s.topologicalClosure ≤ t :=
   closure_minimal h ht
 
-/-- If a subalgebra of a topological algebra is commutative, then so is its topological closure. -/
-def Subalgebra.commSemiringTopologicalClosure [T2Space A] (s : Subalgebra R A)
+/-- If a subalgebra of a topological algebra is commutative, then so is its topological closure.
+
+See note [reducible non-instances]. -/
+abbrev Subalgebra.commSemiringTopologicalClosure [T2Space A] (s : Subalgebra R A)
     (hs : ∀ x y : s, x * y = y * x) : CommSemiring s.topologicalClosure :=
   { s.topologicalClosure.toSemiring, s.toSubmonoid.commMonoidTopologicalClosure hs with }
 
diff --git a/Mathlib/Topology/Algebra/Group/Basic.lean b/Mathlib/Topology/Algebra/Group/Basic.lean
index 642b75b00a922..ad4448b9960eb 100644
--- a/Mathlib/Topology/Algebra/Group/Basic.lean
+++ b/Mathlib/Topology/Algebra/Group/Basic.lean
@@ -680,11 +680,15 @@ def Subgroup.connectedComponentOfOne (G : Type*) [TopologicalSpace G] [Group G]
   mul_mem' hg hh := mul_mem_connectedComponent_one hg hh
   inv_mem' hg := inv_mem_connectedComponent_one hg
 
-/-- If a subgroup of a topological group is commutative, then so is its topological closure. -/
+/-- If a subgroup of a topological group is commutative, then so is its topological closure.
+
+See note [reducible non-instances]. -/
 @[to_additive
   "If a subgroup of an additive topological group is commutative, then so is its
-  topological closure."]
-def Subgroup.commGroupTopologicalClosure [T2Space G] (s : Subgroup G)
+topological closure.
+
+See note [reducible non-instances]."]
+abbrev Subgroup.commGroupTopologicalClosure [T2Space G] (s : Subgroup G)
     (hs : ∀ x y : s, x * y = y * x) : CommGroup s.topologicalClosure :=
   { s.topologicalClosure.toGroup, s.toSubmonoid.commMonoidTopologicalClosure hs with }
 
diff --git a/Mathlib/Topology/Algebra/Monoid.lean b/Mathlib/Topology/Algebra/Monoid.lean
index b711def8cff6f..c7a1bb090d97b 100644
--- a/Mathlib/Topology/Algebra/Monoid.lean
+++ b/Mathlib/Topology/Algebra/Monoid.lean
@@ -434,8 +434,10 @@ theorem Submonoid.topologicalClosure_minimal (s : Submonoid M) {t : Submonoid M}
 
 /-- If a submonoid of a topological monoid is commutative, then so is its topological closure. -/
 @[to_additive "If a submonoid of an additive topological monoid is commutative, then so is its
-topological closure."]
-def Submonoid.commMonoidTopologicalClosure [T2Space M] (s : Submonoid M)
+topological closure.
+
+See note [reducible non-instances]."]
+abbrev Submonoid.commMonoidTopologicalClosure [T2Space M] (s : Submonoid M)
     (hs : ∀ x y : s, x * y = y * x) : CommMonoid s.topologicalClosure :=
   { s.topologicalClosure.toMonoid with
     mul_comm :=
diff --git a/Mathlib/Topology/Algebra/Ring/Basic.lean b/Mathlib/Topology/Algebra/Ring/Basic.lean
index 5376e1e26055f..c5127c95f3ca3 100644
--- a/Mathlib/Topology/Algebra/Ring/Basic.lean
+++ b/Mathlib/Topology/Algebra/Ring/Basic.lean
@@ -115,8 +115,10 @@ theorem Subsemiring.topologicalClosure_minimal (s : Subsemiring α) {t : Subsemi
   closure_minimal h ht
 
 /-- If a subsemiring of a topological semiring is commutative, then so is its
-topological closure. -/
-def Subsemiring.commSemiringTopologicalClosure [T2Space α] (s : Subsemiring α)
+topological closure.
+
+See note [reducible non-instances]. -/
+abbrev Subsemiring.commSemiringTopologicalClosure [T2Space α] (s : Subsemiring α)
     (hs : ∀ x y : s, x * y = y * x) : CommSemiring s.topologicalClosure :=
   { s.topologicalClosure.toSemiring, s.toSubmonoid.commMonoidTopologicalClosure hs with }
 
@@ -250,9 +252,11 @@ theorem Subring.topologicalClosure_minimal (s : Subring α) {t : Subring α} (h
     (ht : IsClosed (t : Set α)) : s.topologicalClosure ≤ t :=
   closure_minimal h ht
 
-/-- If a subring of a topological ring is commutative, then so is its topological closure. -/
-def Subring.commRingTopologicalClosure [T2Space α] (s : Subring α) (hs : ∀ x y : s, x * y = y * x) :
-    CommRing s.topologicalClosure :=
+/-- If a subring of a topological ring is commutative, then so is its topological closure.
+
+See note [reducible non-instances]. -/
+abbrev Subring.commRingTopologicalClosure [T2Space α] (s : Subring α)
+    (hs : ∀ x y : s, x * y = y * x) : CommRing s.topologicalClosure :=
   { s.topologicalClosure.toRing, s.toSubmonoid.commMonoidTopologicalClosure hs with }
 
 end TopologicalSemiring