further simplifications

2 files changed, 46 insertions, 65 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. -/
diff --git a/Nominal/Support.lean b/Nominal/Support.lean
index 6a1d4d9..d8058e0 100644
--- a/Nominal/Support.lean
+++ b/Nominal/Support.lean
@@ -35,11 +35,7 @@ def HasSupport (x : X) (S : Set 𝔸) : Prop :=
 
 /-- Alternative definition with fix 𝔸 S unfolded. -/
 lemma support_iff {x : X} {S : Set 𝔸} : HasSupport 𝔸 x S ↔ ∀ (π : FPerm 𝔸), (∀ x ∈ S, π x = x) → π ∈ fix' 𝔸 x := by
-  constructor
-  · intro hsupp π hπ
-    exact hsupp hπ
-  · intro hsupp π hπ
-    exact hsupp π hπ
+  simp [HasSupport, fix, fix']
 
 /-- If a support is a subset of another set, that set is also a support.  -/
 lemma support_superset {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S ⊆ T → HasSupport 𝔸 x T := by
@@ -155,21 +151,15 @@ lemma support_sInter [Infinite 𝔸] {x : X} {C : Set (Set 𝔸)}: C.Finite →
   · have : DecidableEq (Set 𝔸) := Classical.typeDecidableEq (Set 𝔸)
     apply Finset.Nonempty.induction
     · intro S hS
-      rw [show ⋂₀ ({S} : Finset (Set 𝔸)).toSet = S by simp]
-      apply hS
-      simp
+      rw [Finset.coe_singleton S, Set.sInter_singleton S]
+      apply hS S (Finset.mem_singleton.mpr rfl)
     · intro S C' hS hC' hsing
       rw [Finset.coe_insert S C', Set.sInter_insert S ↑C']
-      have hother : (∀ S ∈ C', HasSupport 𝔸 x S ∧ S.Finite) := by
-        intro S' hS'
-        apply hsing
-        exact Finset.mem_insert_of_mem hS'
-      specialize hC' hother
-      specialize hsing S (by simp)
+      specialize hC' (fun S' hS' => hsing S' (Finset.mem_insert_of_mem hS'))
+      specialize hsing S (Finset.mem_insert_self S C')
       constructor
-      · apply support_inter 𝔸 hsing.left hsing.right hC'.left hC'.right
-      · apply Set.Finite.inter_of_left
-        exact hsing.right
+      · exact support_inter 𝔸 hsing.left hsing.right hC'.left hC'.right
+      · apply Set.Finite.inter_of_left hsing.right
 
 end PermSet
 
@@ -182,8 +172,6 @@ Nominal sets are then just (FPerm 𝔸)-Sets where all elements are finitely sup
 -/
 section NominalSet
 
-variable (𝔸 : Type)
-
 /-- An (FPerm 𝔸)-Set X is nominal if every x ∈ X is finitely supported. -/
 class NominalSet (X : Type) extends PermSet 𝔸 X where
   fin_supp : ∀ (x : X), ∃ (S : Set 𝔸), PermSet.HasSupport 𝔸 x S ∧ S.Finite
@@ -206,31 +194,32 @@ lemma supp_finite {x : X} : (supp 𝔸 x).Finite := by
   obtain ⟨S, ⟨hsuppS, hfinS⟩⟩ := nom.fin_supp x
   apply Set.Finite.subset
   · exact hfinS
-  · grind
+  · apply Set.sInter_subset_of_mem
+    exact Set.mem_sep hsuppS hfinS
+
+/-- We can restrict the supp definition to subsets of a single finite support. -/
+private lemma supp_equiv_finite [Infinite 𝔸] {x : X} {S : Set 𝔸} : PermSet.HasSupport 𝔸 x S → S.Finite → supp 𝔸 x = ⋂₀ { T : Set 𝔸 | T ⊆ S ∧ PermSet.HasSupport 𝔸 x T ∧ T.Finite } := by
+  intro hsuppS hfinS
+  unfold supp; ext a
+  constructor
+  · intro h T hT
+    exact h T hT.out.right
+  · intro h T hT
+    suffices a ∈ S ∩ T by apply Set.mem_of_mem_inter_right; assumption
+    apply h
+    constructor
+    · exact Set.inter_subset_left
+    · constructor
+      · exact PermSet.support_inter 𝔸 hsuppS hfinS hT.out.left hT.out.right
+      · exact Set.Finite.inter_of_left hfinS T
 
 /-- The least finite support is itself a support. -/
 lemma supp_is_support [Infinite 𝔸] {x : X} : PermSet.HasSupport 𝔸 x (supp 𝔸 x) := by
   obtain ⟨S, ⟨hsuppS, hfinS⟩⟩ := nom.fin_supp x
-  have suppf : (supp 𝔸 x = ⋂₀ { T : Set 𝔸 | T ⊆ S ∧ PermSet.HasSupport 𝔸 x T ∧ T.Finite }) := by
-    unfold supp; ext a
-    constructor
-    · intro h T hT
-      apply h
-      exact hT.out.right
-    · intro h T hT
-      suffices : a ∈ S ∩ T
-      · apply Set.mem_of_mem_inter_right; assumption
-      · apply h
-        constructor
-        · exact Set.inter_subset_left
-        · constructor
-          · exact PermSet.support_inter 𝔸 hsuppS hfinS hT.out.left hT.out.right
-          · apply Set.Finite.inter_of_left; assumption
-  rw [suppf]
+  rw [supp_equiv_finite 𝔸 hsuppS hfinS]
   apply PermSet.support_sInter
   · apply Set.Finite.subset
-    · apply Set.Finite.powerset
-      exact hfinS
+    · exact Set.Finite.powerset hfinS
     · intro T hT
       exact hT.out.left
   · use S