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/Helpers/Finset.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Nominal/Helpers/Finset.lean')

diff --git a/Nominal/Helpers/Finset.lean b/Nominal/Helpers/Finset.lean
index 1287c8e..9a74ffc 100644
--- a/Nominal/Helpers/Finset.lean
+++ b/Nominal/Helpers/Finset.lean
@@ -16,7 +16,7 @@ theorem induction
     · apply insert
       · assumption
       · apply h_1; assumption
-    · simp at h
+    · simp only [not_nonempty_iff_eq_empty] at h
       rw [h]
       apply single
 
-- 
cgit v1.3.1