--- a/src/HOL/Fun.thy Mon Dec 19 14:09:37 2022 +0100
+++ b/src/HOL/Fun.thy Tue Dec 20 17:59:44 2022 +0000
@@ -300,11 +300,17 @@
using lin [of x y] ne by (force simp: dual_order.order_iff_strict)
qed
+lemma linorder_inj_onI':
+ fixes A :: "'a :: linorder set"
+ assumes "\<And>i j. i \<in> A \<Longrightarrow> j \<in> A \<Longrightarrow> i < j \<Longrightarrow> f i \<noteq> f j"
+ shows "inj_on f A"
+ by (intro linorder_inj_onI) (auto simp add: assms)
+
lemma linorder_injI:
assumes "\<And>x y::'a::linorder. x < y \<Longrightarrow> f x \<noteq> f y"
shows "inj f"
\<comment> \<open>Courtesy of Stephan Merz\<close>
-using assms by (auto intro: linorder_inj_onI linear)
+using assms by (simp add: linorder_inj_onI')
lemma inj_on_image_Pow: "inj_on f A \<Longrightarrow>inj_on (image f) (Pow A)"
unfolding Pow_def inj_on_def by blast