From 2e5f7e22761bd30857bbe067862a8b256805ecd8 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <contact@haschu.me>
Date: Wed, 15 Apr 2026 16:18:07 +0200
Subject: fs constructions

---
 Nominal/Instances/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Nominal/Instances/Basic.lean')

diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean
index 7a88eeb..a7aec47 100644
--- a/Nominal/Instances/Basic.lean
+++ b/Nominal/Instances/Basic.lean
@@ -398,7 +398,7 @@ instance : PermSet 𝔸 S where
     exact MulAction.one_smul x.val
   mul_smul π τ x := by
     apply Subtype.ext
-    exact SemigroupAction.mul_smul π τ x.val
+    exact mul_smul π τ x.val
 
 @[simp] lemma smul_val (π : FPerm 𝔸) (x : S) : (π • x).val = π • x.val := rfl
 
-- 
cgit v1.3.1