refactor equivariant props to use type classes

1 files changed, 124 insertions, 100 deletions

diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean
index 4ba580d..2682a55 100644
--- a/Nominal/Equivariance.lean
+++ b/Nominal/Equivariance.lean
@@ -20,40 +20,42 @@ section Definition
 variable {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y]
 
 /-- A function is equivariant if it is invariant to applying a permutation before or after the function. -/
-def Function.Equivariant (f : X → Y) : Prop :=
-  ∀ (x : X) (π : FPerm 𝔸), f (π • x) = π • f x
+class inductive Function.Equivariant (f : X → Y) : Prop
+  | intro : (∀ (x : X) (π : FPerm 𝔸), f (π • x) = π • f x) → Equivariant f
 
-/-- A set is equivariant if it is closed under permutations. -/
-def Set.Equivariant (S : Set X) : Prop :=
-  ∀ (x : X) (π : FPerm 𝔸), x ∈ S → π • x ∈ S
+lemma Function.equivariant (f : X → Y) [Equivariant 𝔸 f] :
+    ∀ (x : X) (π : FPerm 𝔸), f (π • x) = π • f x := by
+  cases (inferInstanceAs (Equivariant 𝔸 f)); assumption
 
-/-- A binary relation is equivariant if it is closed under permutations. -/
-def Rel.Equivariant (R : Rel X Y) : Prop :=
-  ∀ (x : X) (y : Y) (π : FPerm 𝔸), R x y → R (π • x) (π • y)
+/-- A set is equivariant if it is closed under permutations. -/
+class inductive Set.Equivariant (S : Set X) : Prop
+  | intro : (∀ (x : X) (π : FPerm 𝔸), x ∈ S → π • x ∈ S) → Equivariant S
 
 /-- For equivariant sets, we even have "if and only if". -/
-lemma Set.Equivariant.iff {S : Set X} : Set.Equivariant 𝔸 S ↔ ∀ (x : X) (π : FPerm 𝔸), x ∈ S ↔ π • x ∈ S := by
-  constructor
-  · intro h x π; constructor
-    · intro hx; exact h x π hx
-    · intro hx
-      apply (h (π • x) π⁻¹) at hx
-      simp only [inv_smul_smul] at hx
-      exact hx
-  · intro h x π hx
-    exact (h x π).mp hx
+lemma Set.equivariant (S : Set X) [Equivariant 𝔸 S] :
+    ∀ (x : X) (π : FPerm 𝔸), x ∈ S ↔ π • x ∈ S := by
+  cases (inferInstanceAs (Equivariant 𝔸 S)); rename_i h
+  intro x π; constructor
+  · intro hx; exact h x π hx
+  · intro hx
+    apply (h (π • x) π⁻¹) at hx
+    simp only [inv_smul_smul] at hx
+    exact hx
+
+/-- A binary relation is equivariant if it is closed under permutations. -/
+class inductive Rel.Equivariant (R : Rel X Y) : Prop
+  | intro : (∀ (x : X) (y : Y) (π : FPerm 𝔸), R x y → R (π • x) (π • y)) → Equivariant R
 
 /-- For equivariant relations, we even have "if and only if". -/
-lemma Rel.Equivariant.iff {R : Rel X Y} : Rel.Equivariant 𝔸 R ↔ ∀ (x : X) (y : Y) (π : FPerm 𝔸), R x y ↔ R (π • x) (π • y) := by
-  constructor
-  · intro h x y π; constructor
-    · intro hxy; exact h x y π hxy
-    · intro hxy
-      apply (h (π • x) (π • y) π⁻¹) at hxy
-      simp only [inv_smul_smul] at hxy
-      exact hxy
-  · intro h x y π hxy
-    exact (h x y π).mp hxy
+lemma Rel.equivariant (R : Rel X Y) [Rel.Equivariant 𝔸 R] :
+    ∀ (x : X) (y : Y) (π : FPerm 𝔸), R x y ↔ R (π • x) (π • y) := by
+  cases (inferInstanceAs (Equivariant 𝔸 R)); rename_i h
+  intro x y π; constructor
+  · intro hxy; exact h x y π hxy
+  · intro hxy
+    apply (h (π • x) (π • y) π⁻¹) at hxy
+    simp only [inv_smul_smul] at hxy
+    exact hxy
 
 end Definition
 
@@ -67,25 +69,32 @@ section Trivial
 variable {X Y Z : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] [PermSet 𝔸 Z]
 
 /-- The identity function is equivariant. -/
-lemma id_equivariant : Function.Equivariant 𝔸 (id : X → X) := by
-  simp [Function.Equivariant]
+instance Function.Equivariant.id : Function.Equivariant 𝔸 (id : X → X) := by
+  constructor
+  simp
 
 /-- The composition of two equivariant functions is equivariant. -/
-lemma comp_equivariant {f : Y → Z} {g : X → Y} : Function.Equivariant 𝔸 f → Function.Equivariant 𝔸 g → Function.Equivariant 𝔸 (f ∘ g) := by
-  intro hf hg x π
+instance Function.Equivariant.comp
+    {f : Y → Z} [Function.Equivariant 𝔸 f] {g : X → Y} [Function.Equivariant 𝔸 g] :
+    Function.Equivariant 𝔸 (f ∘ g) := by
+  constructor; intro x π
   calc
-    f (g (π • x)) = f (π • g x)   := by rw [hg]
-    _             = π • (f (g x)) := by rw [hf]
+    f (g (π • x)) = f (π • g x)   := by rw [← Function.equivariant 𝔸 g]
+    _             = π • (f (g x)) := by rw [← Function.equivariant 𝔸 f]
 
 /-- If a function is equivariant, its inverse is also equivariant. -/
-lemma Function.inv_equivariant {f : X → Y} {inv : Y → X} : Function.LeftInverse inv f → Function.RightInverse inv f → Function.Equivariant 𝔸 f → Function.Equivariant 𝔸 inv := by
-  intro hleft hright hequi y π
+def Function.Equivariant.inv
+    {f : X → Y} [Function.Equivariant 𝔸 f] {inv : Y → X}
+    (hleft : Function.LeftInverse inv f)
+    (hright : Function.RightInverse inv f) :
+    Function.Equivariant 𝔸 inv := by
+  constructor; intro y π
   apply hleft.injective
-  rw [hequi, hright, hright]
+  rw [Function.equivariant 𝔸 f, hright, hright]
 
 /-- The subset relation is equivariant. -/
-lemma Set.subset_equivariant : Rel.Equivariant 𝔸 (Set.Subset : Set X → Set X → Prop) := by
-  intro S T π hST x hx
+instance Set.Equivariant.subset : Rel.Equivariant 𝔸 (Set.Subset : Set X → Set X → Prop) := by
+  constructor; intro S T π hST x hx
   rw [Set.mem_smul_set_iff_inv_smul_mem] at hx
   rw [Set.mem_smul_set_iff_inv_smul_mem]
   exact hST hx
@@ -104,27 +113,29 @@ variable {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y]
 namespace Function.Equivariant
 
 /-- Equivariant functions preserve supports. -/
-lemma preserve_support {x : X} {f : X → Y} {S : Set 𝔸} : Equivariant 𝔸 f → PermSet.HasSupport 𝔸 x S → PermSet.HasSupport 𝔸 (f x) S := by
-  intro hequi hsupp π hπ
+lemma preserve_support {x : X} {f : X → Y} [Equivariant 𝔸 f] {S : Set 𝔸} :
+    PermSet.HasSupport 𝔸 x S → PermSet.HasSupport 𝔸 (f x) S := by
+  intro hsupp π hπ
   calc
-    π • f x = f (π • x) := by rw [← hequi]
+    π • f x = f (π • x) := by rw [← equivariant 𝔸 f]
     _       = f x       := by rw [hsupp hπ]
 
 /-- Equivariant injective functions exactly preserve supports. -/
-lemma preserve_support_inj {x : X} {f : X → Y} {S : Set 𝔸} : Equivariant 𝔸 f → f.Injective → (PermSet.HasSupport 𝔸 x S ↔ PermSet.HasSupport 𝔸 (f x) S) := by
-  intro hequi hinj; constructor
-  · exact preserve_support 𝔸 hequi
+lemma preserve_support_inj {x : X} {f : X → Y} [Equivariant 𝔸 f] {S : Set 𝔸} :
+    f.Injective → (PermSet.HasSupport 𝔸 x S ↔ PermSet.HasSupport 𝔸 (f x) S) := by
+  intro hinj; constructor
+  · exact preserve_support 𝔸
   · intro hsupp π hπ
     by_contra h
-    have : π • f x ≠ f x := by rw [← hequi]; exact fun a => h (hinj a)
+    have : π • f x ≠ f x := by rw [← equivariant 𝔸 f]; intro hcontra; exact h (hinj hcontra)
     have : π • f x = f x := hsupp hπ
     contradiction
 
 end Function.Equivariant
 
 /-- HasSupport is an equivariant relation. -/
-lemma PermSet.support_equivariant : Rel.Equivariant 𝔸 (HasSupport 𝔸 : X → Set 𝔸 → Prop) := by
-  intro x S π hS σ hσ
+instance PermSet.instHasSupportEquivariant : Rel.Equivariant 𝔸 (HasSupport 𝔸 : X → Set 𝔸 → Prop) := by
+  constructor; intro x S π hS σ hσ
   have hfix : (π⁻¹ * σ * π) ∈ fix 𝔸 S := by
     intro a ha
     calc
@@ -154,52 +165,58 @@ variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y]
 namespace Function.Equivariant
 
 /-- If f is equivariant, then supp (f x) ⊆ supp x. -/
-lemma supp_subset {x : X} {f : X → Y} : Equivariant 𝔸 f → NominalSet.supp 𝔸 (f x) ⊆ NominalSet.supp 𝔸 x := by
-  intro hequi
+lemma supp_subset {x : X} {f : X → Y} [Equivariant 𝔸 f] :
+    NominalSet.supp 𝔸 (f x) ⊆ NominalSet.supp 𝔸 x := by
   apply NominalSet.support_subset_supp
-  · exact preserve_support 𝔸 hequi (NominalSet.supp_is_support 𝔸)
+  · exact preserve_support 𝔸 (NominalSet.supp_is_support 𝔸)
   · exact NominalSet.supp_finite 𝔸
 
 /-- If f is equivariant and injective, then supp (f x) = supp x. -/
-lemma supp_eq_if_inj {x : X} {f : X → Y} : Equivariant 𝔸 f → Function.Injective f → NominalSet.supp 𝔸 (f x) = NominalSet.supp 𝔸 x := by
-  intro hequi hinj
-  simp [NominalSet.supp, preserve_support_inj 𝔸 hequi hinj]
+lemma supp_eq_if_inj {x : X} {f : X → Y} [Equivariant 𝔸 f] :
+    Function.Injective f → NominalSet.supp 𝔸 (f x) = NominalSet.supp 𝔸 x := by
+  intro hinj
+  simp [NominalSet.supp, preserve_support_inj 𝔸 hinj]
 
 /-- If f is equivariant and a # x, then a # f x. -/
-lemma preserve_fresh {a : 𝔸} {x : X} {f : X → Y} : Equivariant 𝔸 f → a # x → a # f x := by
-  intro hequi hx ha
-  exact hx ((supp_subset 𝔸 hequi) ha)
+lemma preserve_fresh {a : 𝔸} {x : X} {f : X → Y} [Equivariant 𝔸 f] : a # x → a # f x := by
+  intro hx ha
+  exact hx (supp_subset 𝔸 ha)
 
 /-- If f is equivariant and injective, then a # x iff a # f x. -/
-lemma preserve_fresh_inj {a : 𝔸} {x : X} {f : X → Y} : Equivariant 𝔸 f → Function.Injective f → (a # x ↔ a # f x) := by
-  intro hequi hinj
-  rw [NominalSet.IsFresh, NominalSet.IsFresh, supp_eq_if_inj 𝔸 hequi hinj]
+lemma preserve_fresh_inj {a : 𝔸} {x : X} {f : X → Y} [Equivariant 𝔸 f] :
+    Function.Injective f → (a # x ↔ a # f x) := by
+  intro hinj
+  rw [NominalSet.IsFresh, NominalSet.IsFresh, supp_eq_if_inj 𝔸 hinj]
 
 end Function.Equivariant
 
 /-- If there is an equivariant surjection from a nominal set into an (FPerm 𝔸)-Set, then that set is nominal. -/
-def NominalSet.fromEquivariantSurjective {X Y : Type} [NominalSet 𝔸 X] [PermSet 𝔸 Y] (f : X → Y) (hequi : Function.Equivariant 𝔸 f) (hsurj : Function.Surjective f) : NominalSet 𝔸 Y where
+def NominalSet.ofEquivariantSurjective
+    {X Y : Type} [NominalSet 𝔸 X] [PermSet 𝔸 Y]
+    (f : X → Y) [Function.Equivariant 𝔸 f] (hsurj : Function.Surjective f) :
+    NominalSet 𝔸 Y where
   fin_supp := by
     intro y
     obtain ⟨x, hx⟩ := hsurj y
     use (NominalSet.supp 𝔸 x)
     constructor
     · rw [← hx]
-      exact Function.Equivariant.preserve_support 𝔸 hequi (supp_is_support 𝔸)
+      exact Function.Equivariant.preserve_support 𝔸 (supp_is_support 𝔸)
     · exact supp_finite 𝔸
 
 /-- supp is an equivariant function. -/
-lemma NominalSet.supp_equivariant : Function.Equivariant 𝔸 (supp 𝔸 : X → Set 𝔸) := by
-  intro x π; ext a; constructor
+instance NominalSet.instSuppEquivariant : Function.Equivariant 𝔸 (supp 𝔸 : X → Set 𝔸) := by
+  constructor; intro x π
+  ext a; constructor
   · apply support_subset_supp 𝔸
-    · apply PermSet.support_equivariant
+    · rw [← Rel.equivariant 𝔸 (PermSet.HasSupport 𝔸)]
       exact supp_is_support 𝔸
     · apply Set.Finite.smul_set
       exact supp_finite 𝔸
   · intro ha S hS
     have hsupp : PermSet.HasSupport 𝔸 x (π⁻¹ • S) := by
       rw [show x = π⁻¹ • π • x by exact eq_inv_smul_iff.mpr rfl]
-      apply PermSet.support_equivariant
+      rw [← Rel.equivariant 𝔸 (PermSet.HasSupport 𝔸)]
       exact hS.out.left
     rw [Set.mem_smul_set_iff_inv_smul_mem] at ha
     suffices π⁻¹ • a ∈ π⁻¹ • S by rw [Set.smul_mem_smul_set_iff] at this; assumption
@@ -210,9 +227,9 @@ lemma NominalSet.supp_equivariant : Function.Equivariant 𝔸 (supp 𝔸 : X →
       exact hS.out.right
 
 /-- Freshness is an equivariant relation. -/
-lemma NominalSet.fresh_equivariant : Rel.Equivariant 𝔸 (NominalSet.IsFresh : 𝔸 → X → Prop) := by
-  intro x y π h
-  rwa [IsFresh, supp_equivariant, Set.smul_mem_smul_set_iff]
+instance NominalSet.instFreshEquivariant : Rel.Equivariant 𝔸 (NominalSet.IsFresh : 𝔸 → X → Prop) := by
+  constructor; intro x y π h
+  rwa [IsFresh, Function.equivariant 𝔸 (supp 𝔸), Set.smul_mem_smul_set_iff]
 
 end Nominal
 
@@ -229,8 +246,8 @@ variable {X : Type} [NominalSet 𝔸 X] {R: Rel 𝔸 X} {x : X}
 
 -- We continue with a circular implication chain argument to show these equivalences.
 
-private lemma for_fresh_iff₁ : Equivariant 𝔸 R → (И a, R a x) → (∃ a, a # x ∧ R a x) := by
-  intro hequi h
+private lemma for_fresh_iff₁ : (И a, R a x) → (∃ a, a # x ∧ R a x) := by
+  intro h
   apply Set.Finite.infinite_compl at h
   simp at h
   have hinf : ({a | R a x} \ NominalSet.supp 𝔸 x).Infinite := Set.Infinite.diff h (NominalSet.supp_finite 𝔸)
@@ -238,17 +255,16 @@ private lemma for_fresh_iff₁ : Equivariant 𝔸 R → (И a, R a x) → (∃ a
   simp only [Set.mem_diff, Set.mem_setOf_eq] at ha
   use a; exact ha.symm
 
-private lemma for_fresh_iff₂ : Equivariant 𝔸 R → (∃ a, a # x ∧ R a x) → (∀ a, a # x → R a x) := by
-  intro hequi h
+private lemma for_fresh_iff₂ [Rel.Equivariant 𝔸 R] : (∃ a, a # x ∧ R a x) → (∀ a, a # x → R a x) := by
+  intro h
   obtain ⟨a, ⟨hfresha, ha⟩⟩ := h
   intro b hfreshb
-  have hmem := hequi a x ⸨a, b⸩ ha
-  rw [PermSet.atom_swap, Equiv.swap_apply_left] at hmem
-  rw [NominalSet.fresh_swap_fix 𝔸 hfresha hfreshb] at hmem
-  exact hmem
+  rw [Rel.equivariant 𝔸 R b x ⸨a, b⸩]
+  rw [PermSet.atom_swap, Equiv.swap_apply_right, NominalSet.fresh_swap_fix 𝔸 hfresha hfreshb]
+  exact ha
 
-private lemma for_fresh_iff₃ : Equivariant 𝔸 R → (∀ a, a # x → R a x) → (И a, R a x) := by
-  intro hequi h
+private lemma for_fresh_iff₃ : (∀ a, a # x → R a x) → (И a, R a x) := by
+  intro h
   have hsub : {a : 𝔸 | R a x}ᶜ ⊆ NominalSet.supp 𝔸 x := by
     rw [Set.compl_subset_comm]
     intro a ha
@@ -258,25 +274,25 @@ private lemma for_fresh_iff₃ : Equivariant 𝔸 R → (∀ a, a # x → R a x)
   apply Set.Finite.subset (NominalSet.supp_finite 𝔸) hsub
 
 /-- The quantifier in `И a, a R x` is equivalent to "for any fresh `a`". -/
-lemma for_fresh_iff_exists : Equivariant 𝔸 R → ((И a, R a x) ↔ (∃ a, a # x ∧ R a x)) := by
-  intro hequi; constructor
+lemma for_fresh_iff_exists [Rel.Equivariant 𝔸 R] : ((И a, R a x) ↔ (∃ a, a # x ∧ R a x)) := by
+  constructor
   · intro h
-    apply for_fresh_iff₁ 𝔸 hequi
+    apply for_fresh_iff₁
     exact h
   · intro h
-    apply for_fresh_iff₃ 𝔸 hequi
-    apply for_fresh_iff₂ 𝔸 hequi
+    apply for_fresh_iff₃
+    apply for_fresh_iff₂
     exact h
 
 /-- The quantifier in `И a, a R x` is equivalent to "for all fresh `a`". -/
-lemma for_fresh_iff_all : Equivariant 𝔸 R → ((И a, R a x) ↔ (∀ a, a # x → R a x)) := by
-  intro hequi; constructor
+lemma for_fresh_iff_all [Rel.Equivariant 𝔸 R] : ((И a, R a x) ↔ (∀ a, a # x → R a x)) := by
+  constructor
   · intro h
-    apply for_fresh_iff₂ 𝔸 hequi
-    apply for_fresh_iff₁ 𝔸 hequi
+    apply for_fresh_iff₂
+    apply for_fresh_iff₁
     exact h
   · intro h
-    apply for_fresh_iff₃ 𝔸 hequi
+    apply for_fresh_iff₃
     exact h
 
 end Rel.Equivariant
@@ -305,6 +321,9 @@ notation:25 X " →ₑ[" A "] " Y => EquivariantMap A X Y
 
 variable {X Y Z : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] [PermSet 𝔸 Z]
 
+instance EquivariantMap.toFunEquivariant (f : X →ₑ[𝔸] Y) : Function.Equivariant 𝔸 f.toFun :=
+  f.equivariant
+
 instance : FunLike (X →ₑ[𝔸] Y) X Y where
   coe := EquivariantMap.toFun
   coe_injective' f g h := by cases f; cases g; congr
@@ -312,10 +331,10 @@ instance : FunLike (X →ₑ[𝔸] Y) X Y where
 namespace EquivariantMap
 
 /-- The identity function. -/
-def id : X →ₑ[𝔸] X := ⟨_root_.id, id_equivariant 𝔸⟩
+def id : X →ₑ[𝔸] X := ⟨_root_.id, inferInstance⟩
 
 /-- Function composition. -/
-def comp (f : Y →ₑ[𝔸] Z) (g : X →ₑ[𝔸] Y) : X →ₑ[𝔸] Z := ⟨f ∘ g, comp_equivariant 𝔸 f.equivariant g.equivariant⟩
+def comp (f : Y →ₑ[𝔸] Z) (g : X →ₑ[𝔸] Y) : X →ₑ[𝔸] Z := ⟨f.toFun ∘ g.toFun, inferInstance⟩
 
 @[simp]
 lemma id_app (x : X) : id 𝔸 x = x := rfl
@@ -333,10 +352,6 @@ lemma ext {f g : X →ₑ[𝔸] Y} (h : ∀ a, f a = g a) : f = g :=
 
 end EquivariantMap
 
-/-- Extended setoid definition that also requires the relation to be equivariant. -/
-class EquivariantSetoid (X : Type) [PermSet 𝔸 X] extends Setoid X where
-  equivariant : Rel.Equivariant 𝔸 r
-
 end BundledFunction
 
 /-!
@@ -349,7 +364,7 @@ section Equivalence
 /-- An equivalence where the function is equivariant. -/
 structure EquivariantEquiv (X Y : Type) [PermSet 𝔸 X] [PermSet 𝔸 Y] extends Equiv X Y where
   toFun_equivariant : Function.Equivariant 𝔸 toFun
-  invFun_equivariant : Function.Equivariant 𝔸 invFun := Function.inv_equivariant 𝔸 left_inv right_inv toFun_equivariant
+  invFun_equivariant : Function.Equivariant 𝔸 invFun := Function.Equivariant.inv 𝔸 left_inv right_inv
 
 def Equivariant.Equiv.symm {𝔸 X Y : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] [PermSet 𝔸 X] [PermSet 𝔸 Y] (equiv : EquivariantEquiv 𝔸 X Y) : EquivariantEquiv 𝔸 Y X :=
   { toFun := equiv.invFun
@@ -359,15 +374,24 @@ def Equivariant.Equiv.symm {𝔸 X Y : Type} [Infinite 𝔸] [Countable 𝔸] [D
     right_inv := equiv.left_inv
   }
 
+instance EquivariantEquiv.toFunEquivariant
+    {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y]
+    (equiv : EquivariantEquiv 𝔸 X Y) : Function.Equivariant 𝔸 equiv.toFun :=
+  equiv.toFun_equivariant
+
+instance EquivariantEquiv.invFunEquivariant
+    {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y]
+    (equiv : EquivariantEquiv 𝔸 X Y) : Function.Equivariant 𝔸 equiv.invFun :=
+  equiv.invFun_equivariant
+
 /-- If an (FPerm 𝔸)-Set is equivalent to a nominal set, it is also a nominal set. -/
-def NominalSet.fromEquivariantEquiv {X Y : Type} [PermSet 𝔸 X] [NominalSet 𝔸 Y] (equiv : EquivariantEquiv 𝔸 X Y) : NominalSet 𝔸 X :=
-  NominalSet.fromEquivariantSurjective 𝔸 equiv.invFun equiv.invFun_equivariant equiv.symm.surjective
+def NominalSet.ofEquivariantEquiv {X Y : Type} [PermSet 𝔸 X] [NominalSet 𝔸 Y] (equiv : EquivariantEquiv 𝔸 X Y) : NominalSet 𝔸 X :=
+  NominalSet.ofEquivariantSurjective 𝔸 equiv.invFun equiv.symm.surjective
 
 /-- If two nominal sets are equivalent, the corresponding least supports are equal. -/
 lemma EquivariantEquiv.supp_eq {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y] (equiv : EquivariantEquiv 𝔸 X Y) (x : X) : NominalSet.supp 𝔸 x = NominalSet.supp 𝔸 (equiv.toFun x) := by
   symm
   apply Function.Equivariant.supp_eq_if_inj
-  · exact equiv.toFun_equivariant
-  · exact equiv.injective
+  exact equiv.injective
 
 end Equivalence