From a5ff8efe5b5e314e0aa759318e5fb194e066f612 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <contact@haschu.me>
Date: Tue, 14 Apr 2026 16:04:44 +0200
Subject: update lean

---
 Nominal/Equivariance.lean | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'Nominal/Equivariance.lean')

diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean
index 2682a55..e9bd850 100644
--- a/Nominal/Equivariance.lean
+++ b/Nominal/Equivariance.lean
@@ -25,7 +25,7 @@ class inductive Function.Equivariant (f : X → Y) : Prop
 
 lemma Function.equivariant (f : X → Y) [Equivariant 𝔸 f] :
     ∀ (x : X) (π : FPerm 𝔸), f (π • x) = π • f x := by
-  cases (inferInstanceAs (Equivariant 𝔸 f)); assumption
+  cases (inferInstance : Equivariant 𝔸 f); assumption
 
 /-- A set is equivariant if it is closed under permutations. -/
 class inductive Set.Equivariant (S : Set X) : Prop
@@ -34,7 +34,7 @@ class inductive Set.Equivariant (S : Set X) : Prop
 /-- For equivariant sets, we even have "if and only if". -/
 lemma Set.equivariant (S : Set X) [Equivariant 𝔸 S] :
     ∀ (x : X) (π : FPerm 𝔸), x ∈ S ↔ π • x ∈ S := by
-  cases (inferInstanceAs (Equivariant 𝔸 S)); rename_i h
+  cases (inferInstance : Equivariant 𝔸 S); rename_i h
   intro x π; constructor
   · intro hx; exact h x π hx
   · intro hx
@@ -49,7 +49,7 @@ class inductive Rel.Equivariant (R : Rel X Y) : Prop
 /-- For equivariant relations, we even have "if and only if". -/
 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
+  cases (inferInstance : Equivariant 𝔸 R); rename_i h
   intro x y π; constructor
   · intro hxy; exact h x y π hxy
   · intro hxy
@@ -83,6 +83,7 @@ instance Function.Equivariant.comp
     _             = π • (f (g x)) := by rw [← Function.equivariant 𝔸 f]
 
 /-- If a function is equivariant, its inverse is also equivariant. -/
+@[reducible]
 def Function.Equivariant.inv
     {f : X → Y} [Function.Equivariant 𝔸 f] {inv : Y → X}
     (hleft : Function.LeftInverse inv f)
@@ -191,6 +192,7 @@ lemma preserve_fresh_inj {a : 𝔸} {x : X} {f : X → Y} [Equivariant 𝔸 f] :
 end Function.Equivariant
 
 /-- If there is an equivariant surjection from a nominal set into an (FPerm 𝔸)-Set, then that set is nominal. -/
+@[reducible]
 def NominalSet.ofEquivariantSurjective
     {X Y : Type} [NominalSet 𝔸 X] [PermSet 𝔸 Y]
     (f : X → Y) [Function.Equivariant 𝔸 f] (hsurj : Function.Surjective f) :
@@ -385,6 +387,7 @@ instance EquivariantEquiv.invFunEquivariant
   equiv.invFun_equivariant
 
 /-- If an (FPerm 𝔸)-Set is equivalent to a nominal set, it is also a nominal set. -/
+@[reducible]
 def NominalSet.ofEquivariantEquiv {X Y : Type} [PermSet 𝔸 X] [NominalSet 𝔸 Y] (equiv : EquivariantEquiv 𝔸 X Y) : NominalSet 𝔸 X :=
   NominalSet.ofEquivariantSurjective 𝔸 equiv.invFun equiv.symm.surjective
 
-- 
cgit v1.3.1