implement derivable equality

1 files changed, 15 insertions, 0 deletions

diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean
index dcca75b..64b6425 100644
--- a/Nominal/Instances/Basic.lean
+++ b/Nominal/Instances/Basic.lean
@@ -70,6 +70,21 @@ def NominalSet.mkDiscrete (X : Type) : NominalSet.Discrete 𝔸 X where
     · intro π hπ; simp only [PermSet.fix', Set.mem_setOf_eq]; rfl
     · exact Set.finite_empty
 
+instance {X : Type} [NominalSet.Discrete 𝔸 X] [Finite X] : OrbitFinite 𝔸 X where
+  fin_orbits := Finite.of_equiv X
+    { toFun x := Quotient.mk _ x
+      invFun x := x.out
+      left_inv x := by
+        suffices ∀ (x y : X), MulAction.orbitRel (FPerm 𝔸) X x y → x = y by
+          apply this
+          rw [← Quotient.eq]
+          apply Quotient.out_eq
+        intro x y ⟨π, hπ⟩
+        simp only [NominalSet.Discrete.is_discrete] at hπ
+        exact hπ.symm
+      right_inv x := by simp
+    }
+
 @[simp] lemma NominalSet.Discrete.supp {X : Type} [NominalSet.Discrete 𝔸 X] {x : X} : supp 𝔸 x = ∅ := by
   rw [← Set.subset_empty_iff]
   apply Set.sInter_subset_of_mem