src/HOL/Modules.thy

--- a/src/HOL/Modules.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Modules.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -872,7 +872,7 @@
 
 lemma independent_inj_image:
   "m1.independent S \<Longrightarrow> inj f \<Longrightarrow> m2.independent (f ` S)"
-  using independent_inj_on_image[of S] by (auto simp: subset_inj_on)
+  using independent_inj_on_image[of S] by (auto simp: inj_on_subset)
 
 end