From fc4b13639259cb11b4a3d70960148c2dc9760236 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Sun, 15 Feb 2026 18:05:33 +0100
Subject: [PATCH 1/3] 1st commit

---
 Mathlib/Algebra/Group/Subgroup/Actions.lean    | 5 -----
 Mathlib/Algebra/Group/Submonoid/MulAction.lean | 4 ++++
 2 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Algebra/Group/Subgroup/Actions.lean b/Mathlib/Algebra/Group/Subgroup/Actions.lean
index 29faa3fd7b839d..e814723dff96d6 100644
--- a/Mathlib/Algebra/Group/Subgroup/Actions.lean
+++ b/Mathlib/Algebra/Group/Subgroup/Actions.lean
@@ -27,11 +27,6 @@ variable {G α β : Type*} [Group G]
 section MulAction
 variable [MulAction G α] {S : Subgroup G}
 
-/-- The action by a subgroup is the action by the underlying group. -/
-@[to_additive
-/-- The additive action by an add_subgroup is the action by the underlying `AddGroup`. -/]
-instance instMulAction : MulAction S α := inferInstanceAs (MulAction S.toSubmonoid α)
-
 @[to_additive] lemma smul_def (g : S) (m : α) : g • m = (g : G) • m := rfl
 
 @[to_additive (attr := simp)]
diff --git a/Mathlib/Algebra/Group/Submonoid/MulAction.lean b/Mathlib/Algebra/Group/Submonoid/MulAction.lean
index 749b84d10e7d4e..2d0f71fa4fc738 100644
--- a/Mathlib/Algebra/Group/Submonoid/MulAction.lean
+++ b/Mathlib/Algebra/Group/Submonoid/MulAction.lean
@@ -114,6 +114,10 @@ variable [Monoid M']
 instance mulAction [MulAction M' α] (S : Submonoid M') : MulAction S α :=
   inferInstance
 
+instance {β S : Type*} [SMul M' α] [SMul M' β] [SMul α β] [SetLike S M']
+    [h : SMulDistribClass M' α β] (N' : S) :
+    SMulDistribClass N' α β := ⟨fun g _ _ ↦ h.smul_distrib_smul g _ _⟩
+
 example {S : Submonoid M'} : IsScalarTower S M' M' := by infer_instance
 
 end Submonoid

From 50a6a6ca494840778a51026a93aad50041ffbbb2 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Mon, 16 Feb 2026 09:11:34 +0100
Subject: [PATCH 2/3] put back instance

---
 Mathlib/Algebra/Group/Subgroup/Actions.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/Mathlib/Algebra/Group/Subgroup/Actions.lean b/Mathlib/Algebra/Group/Subgroup/Actions.lean
index e814723dff96d6..29faa3fd7b839d 100644
--- a/Mathlib/Algebra/Group/Subgroup/Actions.lean
+++ b/Mathlib/Algebra/Group/Subgroup/Actions.lean
@@ -27,6 +27,11 @@ variable {G α β : Type*} [Group G]
 section MulAction
 variable [MulAction G α] {S : Subgroup G}
 
+/-- The action by a subgroup is the action by the underlying group. -/
+@[to_additive
+/-- The additive action by an add_subgroup is the action by the underlying `AddGroup`. -/]
+instance instMulAction : MulAction S α := inferInstanceAs (MulAction S.toSubmonoid α)
+
 @[to_additive] lemma smul_def (g : S) (m : α) : g • m = (g : G) • m := rfl
 
 @[to_additive (attr := simp)]

From dbf7da578375e396621eae020b7a5f978439e719 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Mon, 16 Feb 2026 11:14:34 +0100
Subject: [PATCH 3/3] name instance

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

diff --git a/Mathlib/Algebra/Group/Submonoid/MulAction.lean b/Mathlib/Algebra/Group/Submonoid/MulAction.lean
index 2d0f71fa4fc738..9d71e2a9cab955 100644
--- a/Mathlib/Algebra/Group/Submonoid/MulAction.lean
+++ b/Mathlib/Algebra/Group/Submonoid/MulAction.lean
@@ -114,7 +114,7 @@ variable [Monoid M']
 instance mulAction [MulAction M' α] (S : Submonoid M') : MulAction S α :=
   inferInstance
 
-instance {β S : Type*} [SMul M' α] [SMul M' β] [SMul α β] [SetLike S M']
+instance smulDistribClass {β S : Type*} [SMul M' α] [SMul M' β] [SMul α β] [SetLike S M']
     [h : SMulDistribClass M' α β] (N' : S) :
     SMulDistribClass N' α β := ⟨fun g _ _ ↦ h.smul_distrib_smul g _ _⟩