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/Support.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Nominal/Support.lean')

diff --git a/Nominal/Support.lean b/Nominal/Support.lean
index 7888a68..fde20c7 100644
--- a/Nominal/Support.lean
+++ b/Nominal/Support.lean
@@ -79,7 +79,7 @@ lemma support_inter {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S.Finite
       simp)
   let m' := (S \ T).restrict m
   rw [Set.injOn_iff_injective, show (S \ T).restrict m = m' by rfl] at h_m_injective
-  obtain h_m_inv := Function.partialInv_of_injective h_m_injective
+  obtain h_m_inv := h_m_injective.isPartialInv
   have h_m_image : m '' (S \ T) ⊆ (π'.supp ∪ S ∪ T)ᶜ :=
     Set.image_subset_iff.mpr h_m_preimage
 
-- 
cgit v1.3.1