update lean

1 files changed, 6 insertions, 4 deletions

diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean
index b627c1b..7a88eeb 100644
--- a/Nominal/Instances/Basic.lean
+++ b/Nominal/Instances/Basic.lean
@@ -59,6 +59,7 @@ Every set can be made into a discrete nominal set, where supp x = ∅.
 -/
 section Discrete
 
+@[reducible]
 def NominalSet.mkDiscrete (X : Type) : NominalSet.Discrete 𝔸 X where
   smul π x := x
   one_smul := by intro; rfl
@@ -330,6 +331,7 @@ instance : PermSet 𝔸 (Quotient setoid) where
 instance instMkEquivariant : Function.Equivariant 𝔸 (Quotient.mk setoid) := by
   constructor; simp
 
+@[reducible]
 def lift_equivariant
     {Y : Type} [PermSet 𝔸 Y] (f : X → Y) [Function.Equivariant 𝔸 f]
     (h : ∀ (a b : X), a ≈ b → f a = f b) :
@@ -392,11 +394,11 @@ instance : PermSet 𝔸 S where
     rw [← Set.equivariant 𝔸 S]
     exact x.prop⟩
   one_smul x := by
-    apply Subtype.eq
+    apply Subtype.ext
     exact MulAction.one_smul x.val
   mul_smul π τ x := by
-    apply Subtype.eq
-    exact MulAction.mul_smul π τ x.val
+    apply Subtype.ext
+    exact SemigroupAction.mul_smul π τ x.val
 
 @[simp] lemma smul_val (π : FPerm 𝔸) (x : S) : (π • x).val = π • x.val := rfl
 
@@ -410,7 +412,7 @@ instance : NominalSet 𝔸 S where
     use NominalSet.supp 𝔸 x.val
     constructor
     · intro π hπ
-      apply Subtype.eq
+      apply Subtype.ext
       exact NominalSet.supp_is_support 𝔸 hπ
     · exact NominalSet.supp_finite 𝔸