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/Support.lean | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'Nominal/Support.lean')

diff --git a/Nominal/Support.lean b/Nominal/Support.lean
index 89021a0..430aa8c 100644
--- a/Nominal/Support.lean
+++ b/Nominal/Support.lean
@@ -62,7 +62,8 @@ lemma support_inter {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S.Finite
   -- First we obtain an injection m : S \ T → (π'.supp ∪ S ∪ T)ᶜ.
   have h_cod_inf : ((π'.supp ∪ S ∪ T)ᶜ).Infinite := by
     apply Set.Finite.infinite_compl
-    simp; exact ⟨⟨h_π_fin, h_S_finite⟩, h_T_finite⟩
+    simp only [Set.finite_union]
+    exact ⟨⟨h_π_fin, h_S_finite⟩, h_T_finite⟩
   have h_dom_fin : (S \ T).Finite :=
     Set.Finite.diff h_S_finite
 
@@ -308,7 +309,7 @@ lemma fresh_exists {x : X} : ∃ (a : 𝔸), a # x := by
 lemma fresh_swap_fix {a b : 𝔸} {x : X} : a # x → b # x → ⸨a, b⸩ ∈ PermSet.fix' 𝔸 x := by
   intro ha hb
   suffices ⸨a, b⸩ • x = (1 : FPerm 𝔸) • x by
-    simp only [one_smul, PermSet.fix', Set.mem_setOf_eq] at *; assumption
+    simp [one_smul, PermSet.fix'] at *; assumption
   apply PermSet.support_permutations_eq
   · exact supp_is_support 𝔸
   · intro c hc
@@ -316,13 +317,13 @@ lemma fresh_swap_fix {a b : 𝔸} {x : X} : a # x → b # x → ⸨a, b⸩ ∈ P
 
 /-- If a proposition holds for suitably fresh a, then one can always pick such an a. -/
 lemma for_fresh_exists {P : 𝔸 → Prop} : (И a, P a) → (∃ a, P a) := by
-  simp [NominalSet.ForFresh]; intro h
+  simp only [ForFresh]; intro h
   exact h.nonempty
 
 /-- Extensionality lemma for the freshness quantifier. -/
 lemma for_fresh_ext {P Q : 𝔸 → Prop} : (∀ a, P a ↔ Q a) → (И a, P a) = (И a, Q a) := by
   intro h
-  simp [NominalSet.ForFresh]
+  simp only [ForFresh, eq_iff_iff]
   suffices {a | P a} = {a | Q a} by rw [this]
   exact Set.ext h
 
-- 
cgit v1.3.1