use simp only everywhere except for last goal

2 files changed, 23 insertions, 12 deletions

diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean
index 891f00f..d7fade9 100644
--- a/Nominal/Instances/Abstraction.lean
+++ b/Nominal/Instances/Abstraction.lean
@@ -88,7 +88,7 @@ private lemma alpha_eq_pred_equivariant : EquivariantRelation 𝔸 (AlphaEqPred
   rw [AlphaEqPred, AlphaEqPred]
   intro h
   have h' : π • ⸨a, x.fst.atom⸩ • x.fst.body = π • ⸨a, x.snd.atom⸩ • x.snd.body := by congr
-  simp [smul_smul, FPerm.mul_swap_eq_swap_mul] at h'
+  simp only [smul_smul, FPerm.mul_swap_eq_swap_mul] at h'
   simpa [smul_smul]
 
 lemma alpha_eq_iff_exists {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∃ c, c # x ∧ c # y ∧ ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body := by
@@ -96,14 +96,14 @@ lemma alpha_eq_iff_exists {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∃
     rw [alpha_eq_iff_pred, this]
     apply Equivariance.for_fresh_iff_exists
     exact alpha_eq_pred_equivariant
-  simp only [Prod.fresh, AlphaEqPred, @and_assoc]
+  simp [Prod.fresh, AlphaEqPred, @and_assoc]
 
 lemma alpha_eq_iff_all {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∀ c, c # x ∧ c # y → ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body := by
   suffices (∀ c, c # x ∧ c # y → ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body) = (∀ c, c # (x, y) → AlphaEqPred c (x, y)) by
     rw [alpha_eq_iff_pred, this]
     apply Equivariance.for_fresh_iff_all
     exact alpha_eq_pred_equivariant
-  simp only [Prod.fresh, AlphaEqPred]
+  simp [Prod.fresh, AlphaEqPred]
 
 lemma alpha_eq_iff_cases {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ (x.atom = y.atom ∧ x.body = y.body) ∨ (x.atom ≠ y.atom ∧ x.atom # y ∧ x.body = ⸨x.atom, y.atom⸩ • y.body) := by sorry
 
diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean
index 577cff8..2786c86 100644
--- a/Nominal/Instances/Basic.lean
+++ b/Nominal/Instances/Basic.lean
@@ -30,12 +30,15 @@ instance : NominalSet 𝔸 𝔸 where
   · apply support_subset_supp 𝔸
     · exact NominalSet.supp_atom' 𝔸
     · exact Set.finite_singleton a
-  · suffices a ∈ supp 𝔸 a by simp; intro h; rwa [h]
+  · suffices a ∈ supp 𝔸 a by
+      simp only [Set.mem_singleton_iff]
+      intro h
+      rwa [h]
     intro S ⟨hsuppS, hfinS⟩
     by_contra ha
     -- Show that we can find a fresh c with (a c) ∈ fix S
     obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset ({a} ∪ hfinS.toFinset)
-    simp at hc
+    simp only [Finset.singleton_union, Finset.mem_insert, Set.Finite.mem_toFinset, not_or] at hc
     have hfix : ⸨a, c⸩ ∈ PermSet.fix 𝔸 S := by
       intro d hd
       apply FPerm.swap_neq (ne_of_mem_of_not_mem hd ha) (ne_of_mem_of_not_mem hd hc.right)
@@ -64,7 +67,7 @@ def NominalSet.discrete (X : Type) : NominalSet.Discrete 𝔸 X where
   fin_supp := by
     intro x; use {}
     constructor
-    · intro π hπ; simp [PermSet.fix']; rfl
+    · intro π hπ; simp only [PermSet.fix', Set.mem_setOf_eq]; rfl
     · exact Set.finite_empty
 
 @[simp] lemma NominalSet.Discrete.supp {X : Type} [NominalSet.Discrete 𝔸 X] {x : X} : supp 𝔸 x = ∅ := by
@@ -118,13 +121,17 @@ instance : NominalSet 𝔸 (X × Y) where
         intro S hS
         suffices PermSet.HasSupport 𝔸 x S by apply hx; exact ⟨this, hS.out.right⟩
         intro π hπ
-        suffices π ∈ PermSet.fix' 𝔸 (x, y) by simp [PermSet.fix'] at this; exact this.left
+        suffices π ∈ PermSet.fix' 𝔸 (x, y) by
+          simp only [PermSet.fix', smul_mk, mk.injEq, Set.mem_setOf_eq] at this
+          exact this.left
         exact (hS.out.left hπ).out
     | inr hy =>
         intro S hS
         suffices PermSet.HasSupport 𝔸 y S by apply hy; exact ⟨this, hS.out.right⟩
         intro π hπ
-        suffices π ∈ PermSet.fix' 𝔸 (x, y) by simp [PermSet.fix'] at this; exact this.right
+        suffices π ∈ PermSet.fix' 𝔸 (x, y) by
+          simp only [PermSet.fix', smul_mk, mk.injEq, Set.mem_setOf_eq] at this
+          exact this.right
         exact (hS.out.left hπ).out
 
 @[simp] lemma fresh {a : 𝔸} {x : X} {y : Y} : a # (x, y) ↔ a # x ∧ a # y := by
@@ -158,12 +165,12 @@ variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y]
 
 private lemma supp_inl' {x : X} : PermSet.HasSupport 𝔸 (.inl x : X ⊕ Y) (NominalSet.supp 𝔸 x) := by
   intro π hπ
-  simp [PermSet.fix']
+  simp only [PermSet.fix', smul_inl, inl.injEq, Set.mem_setOf_eq]
   exact NominalSet.supp_is_support 𝔸 hπ
 
 private lemma supp_inr' {y : Y} : PermSet.HasSupport 𝔸 (.inr y : X ⊕ Y) (NominalSet.supp 𝔸 y) := by
   intro π hπ
-  simp [PermSet.fix']
+  simp only [PermSet.fix', smul_inr, inr.injEq, Set.mem_setOf_eq]
   exact NominalSet.supp_is_support 𝔸 hπ
 
 instance : NominalSet 𝔸 (X ⊕ Y) where
@@ -181,7 +188,9 @@ instance : NominalSet 𝔸 (X ⊕ Y) where
   · intro hb S hS
     suffices PermSet.HasSupport 𝔸 x S by apply hb; exact ⟨this, hS.out.right⟩
     intro π hπ
-    suffices π ∈ PermSet.fix' 𝔸 (.inl x : X ⊕ Y) by simp [PermSet.fix'] at this; exact this
+    suffices π ∈ PermSet.fix' 𝔸 (.inl x : X ⊕ Y) by
+      simp only [PermSet.fix', smul_inl, inl.injEq, Set.mem_setOf_eq] at this
+      exact this
     exact (hS.out.left hπ).out
 
 @[simp] lemma supp_inr {y : Y} : NominalSet.supp 𝔸 (.inr y : X ⊕ Y) = NominalSet.supp 𝔸 y := by
@@ -192,7 +201,9 @@ instance : NominalSet 𝔸 (X ⊕ Y) where
   · intro hb S hS
     suffices PermSet.HasSupport 𝔸 y S by apply hb; exact ⟨this, hS.out.right⟩
     intro π hπ
-    suffices π ∈ PermSet.fix' 𝔸 (.inr y : X ⊕ Y) by simp [PermSet.fix'] at this; exact this
+    suffices π ∈ PermSet.fix' 𝔸 (.inr y : X ⊕ Y) by
+      simp only [PermSet.fix', smul_inr, inr.injEq, Set.mem_setOf_eq] at this
+      exact this
     exact (hS.out.left hπ).out
 
 @[simp] lemma fresh_inl {a : 𝔸} {x : X} : a # (.inl x : X ⊕ Y) ↔ a # x := by