update lean

2 files changed, 10 insertions, 12 deletions

diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean
index e03d67a..f1a711b 100644
--- a/Nominal/Instances/Abstraction.lean
+++ b/Nominal/Instances/Abstraction.lean
@@ -225,16 +225,12 @@ instance NameAbstraction.setoid_equivariant : Rel.Equivariant 𝔸 (setoid 𝔸
   instAlphaEqEquivariant
 
 /-- Define name abstractions as the quotient set (𝔸 × X)/≈. -/
-def NameAbstraction := Quotient (NameAbstraction.setoid 𝔸 X)
+abbrev NameAbstraction := Quotient (NameAbstraction.setoid 𝔸 X)
 
 namespace NameAbstraction
 
-/-- The equivalence class of a name abstraction (a, x), often written `⟪a⟫ x` -/
-abbrev mk {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {X : Type} [NominalSet 𝔸 X] (a : 𝔸) (x : X) : NameAbstraction 𝔸 X :=
-  Quotient.mk (setoid 𝔸 X) (.mk a x)
-
 /-- We write `⟪a⟫ x` instead of the usual `⟨a⟩ x` because `⟨⟩` is already heavily used in Lean for constructors. -/
-notation "⟪" a "⟫ " x:60 => mk a x
+notation "⟪" a "⟫ " x:60 => (⟦⟨a, x⟩⟧ : NameAbstraction _ _)
 
 instance : NominalSet 𝔸 (NameAbstraction 𝔸 X) := Quotient.instNominalSet 𝔸
 
@@ -390,13 +386,13 @@ private lemma map_id : map 𝔸 (EquivariantMap.id 𝔸 : X →ₑ[𝔸] X) = Eq
   suffices ∀ (x : NameAbstraction 𝔸 X), map' 𝔸 (EquivariantMap.id 𝔸) x = x by ext x; exact this x
   apply Quotient.ind
   intro x
-  simp [map', NameAbstraction.mk]
+  simp [map']
 
 private lemma map_comp (f : Y →ₑ[𝔸] Z) (g : X →ₑ[𝔸] Y) : map 𝔸 (EquivariantMap.comp 𝔸 f g) = EquivariantMap.comp 𝔸 (map 𝔸 f) (map 𝔸 g) := by
   suffices ∀ (x : NameAbstraction 𝔸 X), map' 𝔸 (EquivariantMap.comp 𝔸 f g) x = (map' 𝔸 f) ((map' 𝔸 g) x) by ext x; exact this x
   apply Quotient.ind
   intro x
-  simp [map', NameAbstraction.mk]
+  simp [map']
 
 /-- Name abstractions form a functor `Nom ⥤ Nom`. -/
 def Functor : Nom 𝔸 ⥤ Nom 𝔸 :=
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 𝔸