--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -746,7 +746,7 @@
     and "inj f"
   shows "rel_interior (f ` S) = f ` (rel_interior S)"
   using assms rel_interior_injective_on_span_linear_image[of f S]
-    subset_inj_on[of f "UNIV" "span S"]
+    inj_on_subset[of f "UNIV" "span S"]
   by auto