diff -r d1c26efb7a47 -r 5fd8ba24ca48 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue Oct 11 10:45:42 2022 +0200
+++ b/src/HOL/Fun.thy	Tue Oct 11 12:13:47 2022 +0200
@@ -705,10 +705,6 @@
   "inj_on ((+) a) A"
   by (rule inj_onI) simp
 
-lemma inj_add_left:
-  \<open>inj ((+) a)\<close>
-  by simp
-
 lemma inj_on_add' [simp]:
   "inj_on (\<lambda>b. b + a) A"
   by (rule inj_onI) simp