From 729a15c501ee42a7ed3a4b002d1366bde6406f92 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Tue, 21 Oct 2025 11:38:28 +0200
Subject: simplify some more

---
 Nominal/Basic.lean | 39 ++++++++++++++++++++-------------------
 1 file changed, 20 insertions(+), 19 deletions(-)

diff --git a/Nominal/Basic.lean b/Nominal/Basic.lean
index 1a7f6ac..dde26fc 100644
--- a/Nominal/Basic.lean
+++ b/Nominal/Basic.lean
@@ -76,15 +76,19 @@ def HasSupport (x : X) (S : Set 𝔸) : Prop :=
 lemma support_iff {x : X} {S : Set 𝔸} : HasSupport 𝔸 x S ↔ ∀ (π : FPerm 𝔸), (∀ x ∈ S, π x = x) → π ∈ fix' 𝔸 x := by
   constructor
   · intro hsupp π hπ
-    aesop
+    exact hsupp hπ
   · intro hsupp π hπ
-    aesop
+    exact hsupp π hπ
 
 lemma support_subset {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S ⊆ T → HasSupport 𝔸 x T := by
   intro hS hsub π hπ
   apply hS
-  intro a
-  aesop
+  intro a ha
+  exact hπ a (hsub ha)
+
+#check Set.Finite.exists_injOn_of_encard_le
+#check Set.injOn_iff_injective
+#check Function.partialInv_of_injective
 
 lemma support_inter {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S.Finite → HasSupport 𝔸 x T → T.Finite → HasSupport 𝔸 x (S ∩ T) := by
   sorry
@@ -202,27 +206,24 @@ lemma NominalSet.supp_atoms [Infinite 𝔸] [DecidableEq 𝔸] {a : 𝔸} : supp
     · apply NominalSet.supp_atoms'
     · simp
   · suffices : a ∈ supp 𝔸 a
-    -- TODO: Shorten
     · simp; intro h; rw [h]; assumption
     · intro S ⟨hsuppS, hfinS⟩
-      by_contra
-      have hfin : ({a} ∪ S).Finite := by
-        apply Set.finite_union.mpr; simp [hfinS]
-      obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset hfin.toFinset
-      have h₁ : c ≠ a := by aesop
-      have h₂ : c ∉ S := by aesop
-      have h₃ : ⸨a, c⸩ ∈ PermSet.fix 𝔸 S := by
+      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
-        rw [Equiv.Perm.supp_swap]
-        aesop
-      have h₄ : ⸨a, c⸩ • a = c := by
+        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]
-      unfold PermSet.HasSupport at hsuppS
-      specialize hsuppS h₃
-      simp [PermSet.fix'] at hsuppS
-      aesop
+      have ha₂ : ⸨a, c⸩ • a = a := by
+        specialize hsuppS hfix
+        simpa [PermSet.fix']
+      rw [ha₁] at ha₂
+      exact hc.left ha₂
 
 class DiscreteNominalSet (X : Type) extends NominalSet 𝔸 X, DiscretePermSet 𝔸 X
 
-- 
cgit v1.3.1