further simplifications

1 files changed, 19 insertions, 27 deletions

diff --git a/Nominal/Instances.lean b/Nominal/Instances.lean
index 793baa4..bf1d372 100644
--- a/Nominal/Instances.lean
+++ b/Nominal/Instances.lean
@@ -23,34 +23,28 @@ instance : NominalSet 𝔸 𝔸 where
   fin_supp := by
     intro a
     use {a}
-    constructor
-    · exact NominalSet.supp_atoms' 𝔸
-    · simp
+    exact ⟨NominalSet.supp_atoms' 𝔸, Set.finite_singleton a⟩
 
 lemma NominalSet.supp_atoms [Infinite 𝔸] [DecidableEq 𝔸] {a : 𝔸} : supp 𝔸 a = {a} := by
   ext b; constructor
   · apply support_subset_supp
     · apply NominalSet.supp_atoms'
-    · simp
-  · suffices : a ∈ supp 𝔸 a
-    · simp; intro h; rw [h]; assumption
-    · intro S ⟨hsuppS, hfinS⟩
-      by_contra ha
-      obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset ({a} ∪ hfinS.toFinset)
-      simp at hc
-      have hfix : ⸨a, c⸩ ∈ PermSet.fix 𝔸 S := by
-        intro d hd
-        rw [show ⸨a,c⸩ • d = (Equiv.swap a c) d from rfl]
-        apply Equiv.Perm.supp_notin
-        simp [Equiv.Perm.supp_swap, Ne.symm hc.left]
-        exact ⟨ne_of_mem_of_not_mem hd ha, ne_of_mem_of_not_mem hd hc.right⟩
-      have ha₁ : ⸨a, c⸩ • a = c := by
-        simp [show ⸨a,c⸩ • a = (Equiv.swap a c) a from rfl]
-      have ha₂ : ⸨a, c⸩ • a = a := by
-        specialize hsuppS hfix
-        simpa [PermSet.fix']
-      rw [ha₁] at ha₂
-      exact hc.left ha₂
+    · apply Set.finite_singleton
+  · suffices a ∈ supp 𝔸 a by simp; 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
+    have hfix : ⸨a, c⸩ ∈ PermSet.fix 𝔸 S := by
+      intro d hd
+      apply Equiv.Perm.supp_notin
+      simp [FPerm.swap, Equiv.Perm.supp_swap, Ne.symm hc.left]
+      exact ⟨ne_of_mem_of_not_mem hd ha, ne_of_mem_of_not_mem hd hc.right⟩
+    have h₁ : ⸨a, c⸩ • a = c := by simp [show ⸨a,c⸩ • a = (Equiv.swap a c) a from rfl]
+    have h₂ : ⸨a, c⸩ • a = a := by apply hsuppS; assumption
+    rw [h₁] at h₂
+    exact hc.left h₂
 
 end Atoms
 
@@ -71,15 +65,13 @@ def NominalSet.discrete (X : Type) : DiscreteNominalSet 𝔸 X where
     use {}
     constructor
     · intro π hπ; simp [PermSet.fix']; rfl
-    · simp
+    · exact Set.finite_empty
 
 lemma NominalSet.supp_discrete {X : Type} [DiscreteNominalSet 𝔸 X] {x : X} : supp 𝔸 x = ∅ := by
   rw [← Set.subset_empty_iff]
   apply Set.sInter_subset_of_mem
   constructor
-  · intro π hπ
-    simp [PermSet.fix']
-    exact DiscreteNominalSet.is_discrete x π
+  · intro π hπ; simp [PermSet.fix', DiscreteNominalSet.is_discrete]
   · exact Set.finite_empty
 
 /-- We consider Unit a discrete nominal set. -/