From 40ddf5800f2b26363967c9340cb7a39bf9eb0c8f Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Mon, 20 Apr 2026 18:23:04 +0300
Subject: [PATCH 1/2] feat(Algebra/Group/Commutator): tag
 `addCommutatorElement` as a scoped instance

---
 Mathlib/Algebra/Group/Commutator.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/Group/Commutator.lean b/Mathlib/Algebra/Group/Commutator.lean
index e0b0b3d11fa884..9d4f6dd453e07f 100644
--- a/Mathlib/Algebra/Group/Commutator.lean
+++ b/Mathlib/Algebra/Group/Commutator.lean
@@ -30,7 +30,7 @@ def commutatorElement {G : Type*} [Group G] : Bracket G G :=
 
 namespace commutatorElement
 
-attribute [scoped instance] commutatorElement
+attribute [scoped instance] commutatorElement addCommutatorElement
 
 end commutatorElement
 

From 1e956144dc8e6eb1a4654d7339743f1250edd18e Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Mon, 20 Apr 2026 20:26:07 +0300
Subject: [PATCH 2/2] move scoped instance to `addCommutatorElement` namespace

---
 Mathlib/Algebra/Group/Commutator.lean | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/Group/Commutator.lean b/Mathlib/Algebra/Group/Commutator.lean
index 9d4f6dd453e07f..f6fb3c2445b6b9 100644
--- a/Mathlib/Algebra/Group/Commutator.lean
+++ b/Mathlib/Algebra/Group/Commutator.lean
@@ -30,10 +30,16 @@ def commutatorElement {G : Type*} [Group G] : Bracket G G :=
 
 namespace commutatorElement
 
-attribute [scoped instance] commutatorElement addCommutatorElement
+attribute [scoped instance] commutatorElement
 
 end commutatorElement
 
+namespace addCommutatorElement
+
+attribute [scoped instance] addCommutatorElement
+
+end addCommutatorElement
+
 open scoped commutatorElement
 
 @[to_additive]