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

(limited to 'Nominal/Equivariance.lean')

diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean
index 368d266..50cf7c2 100644
--- a/Nominal/Equivariance.lean
+++ b/Nominal/Equivariance.lean
@@ -38,7 +38,7 @@ lemma equivariant_set_iff {S : Set X} : EquivariantSet 𝔸 S ↔ ∀ (x : X) (
     · intro hx; exact h x π hx
     · intro hx
       apply (h (π • x) π⁻¹) at hx
-      simp at hx
+      simp only [inv_smul_smul] at hx
       exact hx
   · intro h x π hx
     exact (h x π).mp hx
@@ -50,7 +50,7 @@ lemma equivariant_relation_iff {R : Rel X Y} : EquivariantRelation 𝔸 R ↔ 
     · intro hxy; exact h x y π hxy
     · intro hxy
       apply (h (π • x) (π • y) π⁻¹) at hxy
-      simp at hxy
+      simp only [inv_smul_smul] at hxy
       exact hxy
   · intro h x y π hxy
     exact (h x y π).mp hxy
@@ -201,7 +201,7 @@ private lemma for_fresh_iff₁ : EquivariantRelation 𝔸 R → (И a, R a x) 
   intro hequi h
   have hinf : ({a | R a x} \ NominalSet.supp 𝔸 x).Infinite := Set.Infinite.diff h (NominalSet.supp_finite 𝔸)
   obtain ⟨a, ha⟩ := hinf.nonempty
-  simp at ha
+  simp only [Set.mem_diff, Set.mem_setOf_eq] at ha
   use a; exact ha.symm
 
 private lemma for_fresh_iff₂ : EquivariantRelation 𝔸 R → (∃ a, a # x ∧ R a x) → (∀ a, a # x → R a x) := by
@@ -220,7 +220,7 @@ private lemma for_fresh_iff₃ : EquivariantRelation 𝔸 R → (∀ a, a # x 
     intro a ha
     rw [Set.mem_compl_iff] at ha
     exact h a ha
-  simp [NominalSet.ForFresh]
+  simp only [NominalSet.ForFresh]
   apply Set.infinite_of_finite_compl
   apply Set.Finite.subset (NominalSet.supp_finite 𝔸) hsub
 
-- 
cgit v1.3.1