--- a/src/HOL/Fun.thy Wed Jul 05 16:50:07 2023 +0100
+++ b/src/HOL/Fun.thy Thu Jul 06 16:59:12 2023 +0100
@@ -218,6 +218,10 @@
lemma inj_onI [intro?]: "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> f x = f y \<Longrightarrow> x = y) \<Longrightarrow> inj_on f A"
by (simp add: inj_on_def)
+text \<open>For those frequent proofs by contradiction\<close>
+lemma inj_onCI: "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> f x = f y \<Longrightarrow> x \<noteq> y \<Longrightarrow> False) \<Longrightarrow> inj_on f A"
+ by (force simp: inj_on_def)
+
lemma inj_on_inverseI: "(\<And>x. x \<in> A \<Longrightarrow> g (f x) = x) \<Longrightarrow> inj_on f A"
by (auto dest: arg_cong [of concl: g] simp add: inj_on_def)