From 1207e99c440de6af718a7fdef1810b726925cdb9 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Tue, 21 Oct 2025 23:51:23 +0200
Subject: further simplifications

---
 Nominal/Support.lean | 65 ++++++++++++++++++++++------------------------------
 1 file changed, 27 insertions(+), 38 deletions(-)

(limited to 'Nominal/Support.lean')

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
-- 
cgit v1.3.1