# HG changeset patch
# User nipkow
# Date 1751543594 -7200
# Node ID 547335b410054f9a7dc82d91762fd9d79cd671e1
# Parent  c8d92d4ced73ea76b90b9fc18499d9f183c16b31
removed duplicate lemma; added the notion of the kernel of a function

diff -r c8d92d4ced73 -r 547335b41005 NEWS
--- a/NEWS	Tue Jul 01 20:51:26 2025 +0200
+++ b/NEWS	Thu Jul 03 13:53:14 2025 +0200
@@ -175,6 +175,7 @@
       strict_mono_on_less_eq
   - Removed lemmas. Minor INCOMPATIBILITY.
       mono_on_greaterD (use mono_invE instead)
+      subset_inj_on (use inj_on_subset)
 
 * Theory "HOL.Relation":
   - Changed definition of predicate refl_on to not constrain the domain
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/Algebra/Left_Coset.thy
--- a/src/HOL/Algebra/Left_Coset.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Algebra/Left_Coset.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -95,7 +95,7 @@
 
 lemma (in group) inj_on_f'':
     "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. inv a \<otimes> y) (a <# H)"
-  by (meson inj_on_cmult inv_closed l_coset_subset_G subset_inj_on)
+  by (meson inj_on_cmult inv_closed l_coset_subset_G inj_on_subset)
 
 lemma (in group) inj_on_g':
     "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. a \<otimes> y) H"
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -2997,7 +2997,7 @@
     using S hom homeomorphic_map_interior_of
     unfolding homeomorphic_map_def
     by (metis (no_types, lifting) closure_of_subset_topspace inj_on_image_mem_iff
-        interior_of_subset_closure_of subset_inj_on)
+        interior_of_subset_closure_of inj_on_subset)
 qed
 
 lemma homeomorphic_maps_subtopologies:
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/Analysis/Abstract_Topology_2.thy
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -1384,7 +1384,7 @@
   show "subtopology Y (f ` U) homeomorphic_space subtopology X U"
     using assms unfolding homeomorphic_eq_everything_map
     by (metis Int_absorb1 assms(1) homeomorphic_map_subtopologies homeomorphic_space 
-        homeomorphic_space_sym subset_image_inj subset_inj_on)
+        homeomorphic_space_sym subset_image_inj inj_on_subset)
 qed
 
 lemma homeomorphic_map_path_connectedness_eq:
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/Analysis/Convex_Euclidean_Space.thy
--- 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
 
 
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/Analysis/Determinants.thy
--- a/src/HOL/Analysis/Determinants.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Analysis/Determinants.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -56,7 +56,7 @@
       by (metis sign_inverse fU p mem_Collect_eq permutation_permutes)
     from permutes_inj[OF pU]
     have pi: "inj_on p ?U"
-      by (blast intro: subset_inj_on)
+      by (blast intro: inj_on_subset)
     from permutes_image[OF pU]
     have "prod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U =
       prod (\<lambda>i. ?di (transpose A) i (inv p i)) (p ` ?U)"
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/Analysis/Embed_Measure.thy
--- a/src/HOL/Analysis/Embed_Measure.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Analysis/Embed_Measure.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -132,7 +132,7 @@
 lemma nn_integral_embed_measure:
   "inj f \<Longrightarrow> g \<in> borel_measurable (embed_measure M f) \<Longrightarrow>
   nn_integral (embed_measure M f) g = nn_integral M (\<lambda>x. g (f x))"
-  by(erule nn_integral_embed_measure'[OF subset_inj_on]) simp
+  by(erule nn_integral_embed_measure'[OF inj_on_subset]) simp
 
 lemma emeasure_embed_measure':
     assumes "inj_on f (space M)" "A \<in> sets (embed_measure M f)"
@@ -196,7 +196,7 @@
 
 lemma embed_measure_count_space:
     "inj f \<Longrightarrow> embed_measure (count_space A) f = count_space (f`A)"
-  by(rule embed_measure_count_space')(erule subset_inj_on, simp)
+  by(rule embed_measure_count_space')(erule inj_on_subset, simp)
 
 lemma sets_embed_measure_alt:
     "inj f \<Longrightarrow> sets (embed_measure M f) = ((`) f) ` sets M"
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Analysis/Further_Topology.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -2264,7 +2264,7 @@
   have "DIM(real) \<le> DIM('a)"
     by simp
   then show ?thesis
-    using invariance_of_domain_gen assms continuous_on_subset subset_inj_on by metis
+    using invariance_of_domain_gen assms continuous_on_subset inj_on_subset by metis
 qed
 
 lemma continuous_on_inverse_open:
@@ -2308,7 +2308,7 @@
 proof -
   have "open (f ` interior S)"
     using assms
-    by (intro invariance_of_domain_gen) (auto simp: subset_inj_on interior_subset continuous_on_subset)
+    by (intro invariance_of_domain_gen) (auto simp: inj_on_subset interior_subset continuous_on_subset)
   then show ?thesis
     by (simp add: image_mono interiorI interior_subset)
 qed
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/Analysis/Infinite_Sum.thy
--- a/src/HOL/Analysis/Infinite_Sum.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Analysis/Infinite_Sum.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -1119,7 +1119,7 @@
   also have \<open>\<dots> \<longleftrightarrow> (sum (g \<circ> h) \<longlongrightarrow> x) (finite_subsets_at_top A)\<close>
   proof (intro tendsto_cong eventually_finite_subsets_at_top_weakI sum.reindex)
     show "\<And>X. \<lbrakk>finite X; X \<subseteq> A\<rbrakk> \<Longrightarrow> inj_on h X"
-      using assms subset_inj_on by blast
+      using assms inj_on_subset by blast
   qed
   also have \<open>\<dots> \<longleftrightarrow> ((g \<circ> h) has_sum x) A\<close>
     by (simp add: has_sum_def)
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -2365,7 +2365,7 @@
   moreover have "inj_on (the_inv_into A f) B"
     using X f by (auto simp: bij_betw_def inj_on_the_inv_into)
   with X have "inj_on (the_inv_into A f) X"
-    by (auto intro: subset_inj_on)
+    by (auto intro: inj_on_subset)
   ultimately show "emeasure (distr (count_space A) (count_space B) f) X = emeasure (count_space B) X"
     using f unfolding emeasure_distr[OF f' X]
     by (subst (1 2) emeasure_count_space) (auto simp: card_image dest: finite_imageD)
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/BNF_Wellorder_Constructions.thy
--- a/src/HOL/BNF_Wellorder_Constructions.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/BNF_Wellorder_Constructions.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -1017,7 +1017,7 @@
   unfolding well_order_on_def
   using Linear_order_dir_image[of r f] wf_dir_image[of "r - Id" f]
     dir_image_minus_Id[of f r]
-    subset_inj_on[of f "Field r" "Field(r - Id)"]
+    inj_on_subset[of f "Field r" "Field(r - Id)"]
     mono_Field[of "r - Id" r] by auto
 
 lemma dir_image_bij_betw:
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/BNF_Wellorder_Embedding.thy
--- a/src/HOL/BNF_Wellorder_Embedding.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/BNF_Wellorder_Embedding.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -300,7 +300,7 @@
       (* Main proof *)
   show "bij_betw f (under r a) (under r' (f a))"
   proof(unfold bij_betw_def, auto)
-    show  "inj_on f (under r a)" by (rule subset_inj_on[OF * under_Field])
+    show  "inj_on f (under r a)" by (rule inj_on_subset[OF * under_Field])
   next
     fix b assume "b \<in> under r a"
     thus "f b \<in> under r' (f a)"
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/Cardinals/Ordinal_Arithmetic.thy
--- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -1302,7 +1302,7 @@
         unfolding F_def fun_eq_iff FinFunc_def Func_def Let_def t.ofilter_def under_def by auto
       moreover from gh(2) *(1,3) have "(\<lambda>x. if x \<in> Field s then h (f x) else undefined) \<in> FinFunc r s"
         unfolding FinFunc_def Func_def fin_support_def support_def t.ofilter_def under_def
-        by (auto intro: subset_inj_on elim!: finite_imageD[OF finite_subset[rotated]])
+        by (auto intro: inj_on_subset elim!: finite_imageD[OF finite_subset[rotated]])
       ultimately show "?thesis" by (rule image_eqI)
     qed simp
   qed
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/Combinatorics/Permutations.thy
--- a/src/HOL/Combinatorics/Permutations.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Combinatorics/Permutations.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -797,7 +797,7 @@
   from \<open>p permutes S\<close> have "inj p"
     by (rule permutes_inj)
   then have "inj_on p S"
-    by (auto intro: subset_inj_on)
+    by (auto intro: inj_on_subset)
   then have "F g (p ` S) = F (g \<circ> p) S"
     by (rule reindex)
   moreover from \<open>p permutes S\<close> have "p ` S = S"
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/Complex_Analysis/Riemann_Mapping.thy
--- a/src/HOL/Complex_Analysis/Riemann_Mapping.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Complex_Analysis/Riemann_Mapping.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -295,7 +295,7 @@
       have 2: "\<And>z. z \<in> S \<Longrightarrow> (h \<circ> f) z \<noteq> 0"
         by (metis \<open>h a = 0\<close> a comp_eq_dest_lhs nf1 kh mem_ball_0 that)
       have 3: "inj_on (h \<circ> f) S"
-        by (metis (no_types, lifting) F_def \<open>f \<in> F\<close> comp_inj_on inj_on_inverseI injf kh mem_Collect_eq subset_inj_on)
+        by (metis (no_types, lifting) F_def \<open>f \<in> F\<close> comp_inj_on inj_on_inverseI injf kh mem_Collect_eq inj_on_subset)
       obtain \<psi> where hol\<psi>: "\<psi> holomorphic_on ((h \<circ> f) ` S)"
         and \<psi>2: "\<And>z. z \<in> S  \<Longrightarrow> \<psi>(h (f z)) ^ 2 = h(f z)"
       proof (rule exE [OF prev [OF 1 2 3]], safe)
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Equiv_Relations.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -408,6 +408,30 @@
 qed (use assms in blast)
 
 
+subsection \<open>Kernel of a Function\<close>
+
+definition kernel :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a * 'a) set" where
+"kernel f = {(x,y). f x = f y}"
+
+lemma equiv_kernel: "equiv UNIV (kernel f)"
+unfolding kernel_def equiv_def refl_on_def sym_def trans_def by auto
+
+lemma respects_kernel: "f respects (kernel f)"
+by (simp add: congruent_def kernel_def)
+
+lemma inj_on_vimage_image: "inj_on (\<lambda>b. f -` {b}) (f ` A)"
+using inj_on_def by fastforce
+
+lemma kernel_Image: "kernel f `` A = f -` (f ` A)"
+unfolding kernel_def by (auto simp add: rev_image_eqI)
+
+lemma quotient_kernel_eq_image: "A // kernel f = (\<lambda>b. f -` {b}) ` f ` A"
+by(auto simp: quotient_def kernel_Image)
+
+lemma bij_betw_image_quotient_kernel: "bij_betw (\<lambda>b. f -` {b}) (f ` A) (A // kernel f)"
+by (simp add: bij_betw_def inj_on_vimage_image quotient_kernel_eq_image)
+
+
 subsection \<open>Projection\<close>
 
 definition proj :: "('b \<times> 'a) set \<Rightarrow> 'b \<Rightarrow> 'a set"
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Finite_Set.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -2380,7 +2380,7 @@
 
 lemma card_vimage_inj: "inj f \<Longrightarrow> A \<subseteq> range f \<Longrightarrow> card (f -` A) = card A"
   by (auto 4 3 simp: subset_image_iff inj_vimage_image_eq
-      intro: card_image[symmetric, OF subset_inj_on])
+      intro: card_image[symmetric, OF inj_on_subset])
 
 lemma card_inverse[simp]: "card (R\<inverse>) = card R"
 proof -
@@ -3053,7 +3053,7 @@
 lemma inj_on_image_Fpow:
   assumes "inj_on f A"
   shows "inj_on (image f) (Fpow A)"
-  using assms Fpow_subset_Pow[of A] subset_inj_on[of "image f" "Pow A"]
+  using assms Fpow_subset_Pow[of A] inj_on_subset[of "image f" "Pow A"]
     inj_on_image_Pow by blast
 
 lemma image_Fpow_mono:
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Fun.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -229,18 +229,8 @@
   unfolding inj_on_def by blast
 
 lemma inj_on_subset:
-  assumes "inj_on f A"
-    and "B \<subseteq> A"
-  shows "inj_on f B"
-proof (rule inj_onI)
-  fix a b
-  assume "a \<in> B" and "b \<in> B"
-  with assms have "a \<in> A" and "b \<in> A"
-    by auto
-  moreover assume "f a = f b"
-  ultimately show "a = b"
-    using assms by (auto dest: inj_onD)
-qed
+  "\<lbrakk> inj_on f A; B \<subseteq> A \<rbrakk> \<Longrightarrow> inj_on f B"
+unfolding inj_on_def by blast
 
 lemma comp_inj_on: "inj_on f A \<Longrightarrow> inj_on g (f ` A) \<Longrightarrow> inj_on (g \<circ> f) A"
   by (simp add: comp_def inj_on_def)
@@ -261,9 +251,6 @@
 lemma inj_on_empty[iff]: "inj_on f {}"
   by (simp add: inj_on_def)
 
-lemma subset_inj_on: "inj_on f B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> inj_on f A"
-  unfolding inj_on_def by blast
-
 lemma inj_on_Un: "inj_on f (A \<union> B) \<longleftrightarrow> inj_on f A \<and> inj_on f B \<and> f ` (A - B) \<inter> f ` (B - A) = {}"
   unfolding inj_on_def by (blast intro: sym)
 
@@ -319,6 +306,9 @@
 lemma inj_on_image_Pow: "inj_on f A \<Longrightarrow>inj_on (image f) (Pow A)"
   unfolding Pow_def inj_on_def by blast
 
+lemma inj_on_vimage_image: "inj_on (\<lambda>b. f -` {b}) (f ` A)"
+using inj_on_def by fastforce
+
 lemma bij_betw_image_Pow: "bij_betw f A B \<Longrightarrow> bij_betw (image f) (Pow A) (Pow B)"
   by (auto simp add: bij_betw_def inj_on_image_Pow image_Pow_surj)
 
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/Homology/Invariance_of_Domain.thy
--- a/src/HOL/Homology/Invariance_of_Domain.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Homology/Invariance_of_Domain.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -1863,7 +1863,7 @@
   shows "embedding_map(subtopology (Euclidean_space m) U) (Euclidean_space n) f"
   proof (rule injective_open_imp_embedding_map [OF cmf])
   show "open_map (subtopology (Euclidean_space m) U) (Euclidean_space n) f"
-    by (meson U \<open>n \<le> m\<close> \<open>inj_on f U\<close> cmf continuous_map_from_subtopology_mono invariance_of_domain_Euclidean_space_gen open_map_def openin_open_subtopology subset_inj_on)
+    by (meson U \<open>n \<le> m\<close> \<open>inj_on f U\<close> cmf continuous_map_from_subtopology_mono invariance_of_domain_Euclidean_space_gen open_map_def openin_open_subtopology inj_on_subset)
   show "inj_on f (topspace (subtopology (Euclidean_space m) U))"
     using assms openin_subset topspace_subtopology_subset by fastforce
 qed
@@ -2412,7 +2412,7 @@
   assumes "open T" "continuous_on S f" "inj_on f S" "T \<subseteq> S"
     shows "open (f ` T)"
   apply (rule invariance_of_domain_gen [OF \<open>open T\<close>])
-  using assms apply (auto simp: elim: continuous_on_subset subset_inj_on)
+  using assms apply (auto simp: elim: continuous_on_subset inj_on_subset)
   done
 
 lemma continuous_on_inverse_open:
@@ -2460,7 +2460,7 @@
     by (simp add: image_mono interior_subset)
   show "open (f ` interior S)"
     using assms
-    by (auto simp: subset_inj_on interior_subset continuous_on_subset invariance_of_domain_gen)
+    by (auto simp: inj_on_subset interior_subset continuous_on_subset invariance_of_domain_gen)
 qed
 
 lemma homeomorphic_interiors_same_dimension:
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Inductive.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -467,7 +467,7 @@
   show "inj_on ?h A"
   proof -
     from inj1 X_sub have on_X: "inj_on f X"
-      by (rule subset_inj_on)
+      by (rule inj_on_subset)
 
     have on_X_compl: "inj_on g' (A - X)"
       unfolding g'_def X_compl
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Library/Countable_Set.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -47,7 +47,7 @@
   by (blast intro: countableI_bij1 countableI_bij2)
 
 lemma countable_subset: "A \<subseteq> B \<Longrightarrow> countable B \<Longrightarrow> countable A"
-  by (auto simp: countable_def intro: subset_inj_on)
+  by (auto simp: countable_def intro: inj_on_subset)
 
 lemma countableI_type[intro, simp]: "countable (A:: 'a :: countable set)"
   using countableI[of to_nat A] by auto
@@ -211,7 +211,7 @@
   moreover have "inj_on (inv_into A f) (f`A)" "inv_into A f ` f ` A \<subseteq> A"
     by (auto intro: inj_on_inv_into inv_into_into)
   ultimately show ?thesis
-    by (blast dest: comp_inj_on subset_inj_on intro: countableI)
+    by (blast dest: comp_inj_on inj_on_subset intro: countableI)
 qed
 
 lemma countable_image_inj_on: "countable (f ` A) \<Longrightarrow> inj_on f A \<Longrightarrow> countable A"
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/Library/Groups_Big_Fun.thy
--- a/src/HOL/Library/Groups_Big_Fun.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Library/Groups_Big_Fun.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -74,7 +74,7 @@
 proof -
   from assms have unfold: "h = g \<circ> l" by simp
   from \<open>bij l\<close> have "inj l" by (rule bij_is_inj)
-  then have "inj_on l {a. h a \<noteq> \<^bold>1}" by (rule subset_inj_on) simp
+  then have "inj_on l {a. h a \<noteq> \<^bold>1}" by (rule inj_on_subset) simp
   moreover from \<open>bij l\<close> have "{a. g a \<noteq> \<^bold>1} = l ` {a. h a \<noteq> \<^bold>1}"
     by (auto simp add: image_Collect unfold elim: bij_pointE)
   moreover have "\<And>x. x \<in> {a. h a \<noteq> \<^bold>1} \<Longrightarrow> g (l x) = h x"
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Library/Ramsey.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -194,7 +194,7 @@
   then show "A Int (f -` X) \<in> [A]\<^bsup>k\<^esup>"
     using assms
     unfolding nsets_def mem_Collect_eq
-    by (metis card_image finite_image_iff inf_le1 subset_inj_on)
+    by (metis card_image finite_image_iff inf_le1 inj_on_subset)
 qed
 
 lemma nsets_image_funcset:
@@ -1016,7 +1016,7 @@
       from pg show "?gy ` {n. ?gt n = s'} \<subseteq> YY"
         by (auto simp add: Let_def split_beta)
       from infeqs' show "infinite (?gy ` {n. ?gt n = s'})"
-        by (blast intro: inj_gy [THEN subset_inj_on] dest: finite_imageD)
+        by (blast intro: inj_gy [THEN inj_on_subset] dest: finite_imageD)
       show "s' < s" by (rule less')
       show "\<forall>X. X \<subseteq> ?gy ` {n. ?gt n = s'} \<and> finite X \<and> card X = Suc r \<longrightarrow> f X = s'"
       proof -
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/List.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -4701,7 +4701,7 @@
 
 lemma map_removeAll_inj: "inj f \<Longrightarrow>
   map f (removeAll x xs) = removeAll (f x) (map f xs)"
-by (rule map_removeAll_inj_on, erule subset_inj_on, rule subset_UNIV)
+by (rule map_removeAll_inj_on, erule inj_on_subset, rule subset_UNIV)
 
 lemma length_removeAll_less_eq [simp]:
   "length (removeAll x xs) \<le> length xs"
@@ -6653,7 +6653,7 @@
   case True
   with assms inj_on show ?thesis
     using distinct_card[symmetric, OF distinct_sorted_key_list_of_set]
-    by (auto simp: subset_inj_on intro!: card_image)
+    by (auto simp: inj_on_subset intro!: card_image)
 qed auto
 
 lemmas sorted_key_list_of_set =
@@ -6672,7 +6672,7 @@
 
 lemma strict_sorted_key_list_of_set [simp]:
   "A \<subseteq> S \<Longrightarrow> sorted_wrt (\<prec>) (map f (sorted_key_list_of_set f A))"
-  by (cases "finite A") (auto simp: strict_sorted_iff subset_inj_on[OF inj_on])
+  by (cases "finite A") (auto simp: strict_sorted_iff inj_on_subset[OF inj_on])
 
 lemma finite_set_strict_sorted:
   assumes "A \<subseteq> S" and "finite A"
diff -r c8d92d4ced73 -r 547335b41005 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
 
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -688,7 +688,7 @@
 
 lemma pmf_map_inj': "inj f \<Longrightarrow> pmf (map_pmf f M) (f x) = pmf M x"
 apply(cases "x \<in> set_pmf M")
- apply(simp add: pmf_map_inj[OF subset_inj_on])
+ apply(simp add: pmf_map_inj[OF inj_on_subset])
 apply(simp add: pmf_eq_0_set_pmf[symmetric])
 apply(auto simp add: pmf_eq_0_set_pmf dest: injD)
 done
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/Probability/Projective_Family.thy
--- a/src/HOL/Probability/Projective_Family.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Probability/Projective_Family.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -618,7 +618,7 @@
     have inj_t: "inj_on t (\<Union>i. J i)"
       using count by (auto simp: t_def)
     then have inj_t_J: "inj_on t (J i)" for i
-      by (rule subset_inj_on) auto
+      by (rule inj_on_subset) auto
     interpret IT: Ionescu_Tulcea "\<lambda>i \<omega>. M (f i)" "\<lambda>i. M (f i)"
       by standard auto
     interpret Mf: product_prob_space "\<lambda>x. M (f x)" UNIV
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/Probability/Projective_Limit.thy
--- a/src/HOL/Probability/Projective_Limit.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Probability/Projective_Limit.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -139,7 +139,7 @@
     by unfold_locales (auto simp: Utn_def intro: from_nat_into_to_nat_on[OF countable_UN_J])
   have inj_on_Utn: "inj_on Utn (\<Union>n. J n)"
     unfolding Utn_def using countable_UN_J by (rule inj_on_to_nat_on)
-  hence inj_on_Utn_J: "\<And>n. inj_on Utn (J n)" by (rule subset_inj_on) auto
+  hence inj_on_Utn_J: "\<And>n. inj_on Utn (J n)" by (rule inj_on_subset) auto
   define P' where "P' n = mapmeasure n (P (J n)) (\<lambda>_. borel)" for n
   interpret P': prob_space "P' n" for n
     unfolding P'_def mapmeasure_def using J
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Series.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -1164,7 +1164,7 @@
     and suminf_reindex: "(\<And>x. x \<notin> range g \<Longrightarrow> f x = 0) \<Longrightarrow> suminf (f \<circ> g) = suminf f"
 proof -
   from \<open>inj g\<close> have [simp]: "\<And>A. inj_on g A"
-    by (rule subset_inj_on) simp
+    by (rule inj_on_subset) simp
 
   have smaller: "\<forall>n. (\<Sum>i<n. (f \<circ> g) i) \<le> suminf f"
   proof
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/Vector_Spaces.thy
--- a/src/HOL/Vector_Spaces.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Vector_Spaces.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -1388,7 +1388,7 @@
   then have "vs1.span S = vs1.span B"
     using vs1.span_mono[of B S] vs1.span_mono[of S "vs1.span B"] vs1.span_span[of B] by auto
   moreover have "card (f ` B) = card B"
-    using assms card_image[of f B] subset_inj_on[of f "vs1.span S" B] B vs1.span_superset by auto
+    using assms card_image[of f B] inj_on_subset[of f "vs1.span S" B] B vs1.span_superset by auto
   moreover have "(f ` B) \<subseteq> (f ` S)"
     using B by auto
   ultimately show ?thesis
diff -r c8d92d4ced73 -r 547335b41005 src/HOL/ZF/Zet.thy
--- a/src/HOL/ZF/Zet.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/ZF/Zet.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -54,7 +54,7 @@
   have "inj_on (inv_into A g) (g ` A)" by (simp add: inj_on_inv_into)
   then have injw: "inj_on ?w (g ` A)"
     apply (rule comp_inj_on)
-    apply (rule subset_inj_on[where B=A])
+    apply (rule inj_on_subset[where A=A])
     apply (auto simp add: subset injf)
     done
   show ?thesis