From 6df3f662f0f23e837b70ef1f4a8b8dde4a7aa521 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Fri, 24 Oct 2025 18:20:43 +0200
Subject: use simp only everywhere except for last goal

---
 Nominal/Category.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'Nominal/Category.lean')

diff --git a/Nominal/Category.lean b/Nominal/Category.lean
index 29a0b73..721dfb0 100644
--- a/Nominal/Category.lean
+++ b/Nominal/Category.lean
@@ -66,6 +66,10 @@ instance : ConcreteCategory (Nom 𝔸) (· →ₑ[𝔸] ·) where
 instance : HasForget₂ (Nom 𝔸) (Action Type (FPerm 𝔸)) where
   forget₂ :=
     { obj X := Action.ofMulAction (FPerm 𝔸) X.carrier
-      map f := ⟨f.toFun, by intro π; ext x; simp; apply f.equivariant⟩ }
+      map f := ⟨f.toFun, by
+        intro π
+        ext x
+        simp only [EquivariantMap.toFun_eq_coe, types_comp_apply, Action.ofMulAction_apply]
+        apply f.equivariant⟩ }
 
 end Forget
-- 
cgit v1.3.1