From 80b248c5be656dd2b3ba753871aeeb7102e92ff8 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Thu, 30 Oct 2025 13:11:43 +0100
Subject: prove supp of preterms

---
 Nominal/Instances/Abstraction.lean | 30 +++++++++---------------------
 1 file changed, 9 insertions(+), 21 deletions(-)

(limited to 'Nominal/Instances/Abstraction.lean')

diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean
index ba2fbf9..052f604 100644
--- a/Nominal/Instances/Abstraction.lean
+++ b/Nominal/Instances/Abstraction.lean
@@ -46,31 +46,19 @@ instance : PermSet 𝔸 (NameAbstraction' 𝔸 X) where
   one_smul := by intro _; ext <;> simp [one_smul]
   mul_smul := by intro _ _ _; ext <;> simp [mul_smul]
 
-private def ofPair (x : (𝔸 × X)) : NameAbstraction' 𝔸 X := ⟨x.fst, x.snd⟩
-
-private lemma ofPair_injective : Function.Injective (ofPair 𝔸 X) := by
-  intro x y hxy
-  simp only [ofPair, mk.injEq] at hxy
-  ext
-  · exact hxy.left
-  · exact hxy.right
-
-private lemma ofPair_surjective : Function.Surjective (ofPair 𝔸 X) := by
-  intro x
-  use ⟨x.atom, x.body⟩
-  simp [ofPair]
-
-private lemma ofPair_equivariant : Function.Equivariant 𝔸 (ofPair 𝔸 X) := by
-  intro x π
-  ext <;> simp [ofPair]
+private def equiv : EquivariantEquiv 𝔸 (NameAbstraction' 𝔸 X) (𝔸 × X) :=
+  { toFun x := ⟨x.atom, x.body⟩
+    invFun x := ⟨x.fst, x.snd⟩
+    toFun_equivariant := by intro x π; ext <;> simp
+  }
 
 instance : NominalSet 𝔸 (NameAbstraction' 𝔸 X) :=
-  NominalSet.fromEquivariantSurjective 𝔸 (ofPair 𝔸 X) (ofPair_equivariant 𝔸 X) (ofPair_surjective 𝔸 X)
+  NominalSet.fromEquivariantEquiv 𝔸 (equiv 𝔸 X)
 
 @[simp] lemma supp {x : NameAbstraction' 𝔸 X} : NominalSet.supp 𝔸 x = NominalSet.supp 𝔸 x.body ∪ {x.atom} := by
-  have h : NominalSet.supp 𝔸 (ofPair 𝔸 X (x.atom, x.body)) = NominalSet.supp 𝔸 (x.atom, x.body) :=
-    Function.Equivariant.supp_eq_if_inj 𝔸 (ofPair_equivariant 𝔸 X) (ofPair_injective 𝔸 X)
-  simp only [Prod.supp, NominalSet.supp_atom, ofPair] at h
+  have h : NominalSet.supp 𝔸 x = NominalSet.supp 𝔸 (x.atom, x.body) :=
+    EquivariantEquiv.supp_eq 𝔸 (equiv 𝔸 X) x
+  simp only [Prod.supp, NominalSet.supp_atom] at h
   rwa [Set.union_comm] at h
 
 @[simp] lemma fresh {a : 𝔸} {x : NameAbstraction' 𝔸 X} : a # x ↔ a ≠ x.atom ∧ a # x.body := by
-- 
cgit v1.3.1