From 5dde77b6db9fc78094363f91e0c6643a84be513e Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Wed, 29 Oct 2025 00:40:13 +0100
Subject: refactor equivariance namespaces

---
 Nominal/Instances/Basic.lean | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

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

diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean
index 2ebe9b1..d41e87f 100644
--- a/Nominal/Instances/Basic.lean
+++ b/Nominal/Instances/Basic.lean
@@ -140,11 +140,11 @@ instance : NominalSet 𝔸 (X × Y) where
 lemma supp_comm {x : X} {y : Y} : NominalSet.supp 𝔸 (x, y) = NominalSet.supp 𝔸 (y, x) := by
   simp; apply Set.union_comm
 
-lemma fst_equivariant : Equivariant 𝔸 (Prod.fst : X × Y → X) := by
-  simp [Equivariant]
+lemma fst_equivariant : Function.Equivariant 𝔸 (Prod.fst : X × Y → X) := by
+  simp [Function.Equivariant]
 
-lemma snd_equivariant : Equivariant 𝔸 (Prod.snd : X × Y → Y) := by
-  simp [Equivariant]
+lemma snd_equivariant : Function.Equivariant 𝔸 (Prod.snd : X × Y → Y) := by
+  simp [Function.Equivariant]
 
 end Prod
 
@@ -212,11 +212,11 @@ instance : NominalSet 𝔸 (X ⊕ Y) where
 @[simp] lemma fresh_inr {a : 𝔸} {y : Y} : a # (.inr y : X ⊕ Y) ↔ a # y := by
   simp [NominalSet.IsFresh]
 
-lemma inl_equivariant : Equivariant 𝔸 (Sum.inl : X → X ⊕ Y) := by
-  simp [Equivariant]
+lemma inl_equivariant : Function.Equivariant 𝔸 (Sum.inl : X → X ⊕ Y) := by
+  simp [Function.Equivariant]
 
-lemma inr_equivariant : Equivariant 𝔸 (Sum.inr : Y → X ⊕ Y) := by
-  simp [Equivariant]
+lemma inr_equivariant : Function.Equivariant 𝔸 (Sum.inr : Y → X ⊕ Y) := by
+  simp [Function.Equivariant]
 
 end Sum
 
@@ -251,8 +251,8 @@ instance : PermSet 𝔸 (Quotient setoid.toSetoid) where
     apply Quotient.ind
     simp [mul_smul]
 
-lemma mk_equivariant : Equivariant 𝔸 (Quotient.mk setoid.toSetoid) := by
-  simp [Equivariant]
+lemma mk_equivariant : Function.Equivariant 𝔸 (Quotient.mk setoid.toSetoid) := by
+  simp [Function.Equivariant]
 
 variable {X : Type} [NominalSet 𝔸 X] {setoid : EquivariantSetoid 𝔸 X}
 
@@ -265,7 +265,7 @@ lemma supp {x : X} : NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x) = {a |
   · intro ha x' hx'
     rw [← Quotient.sound hx'] at ha
     have hsub : NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x') ⊆ NominalSet.supp 𝔸 x' :=
-      Equivariant.supp_subset 𝔸 (mk_equivariant 𝔸)
+      Function.Equivariant.supp_subset 𝔸 (mk_equivariant 𝔸)
     exact hsub ha
   · contrapose; intro ha
     simp only [Set.mem_setOf_eq, Classical.not_imp, not_forall]
-- 
cgit v1.3.1