Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Groups_Big_Fun.thy
changeset 82802 547335b41005
parent 81142 6ad2c917dd2e 
--- 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"
isabelle