diff --git a/Mathlib/Logic/Function/Basic.lean b/Mathlib/Logic/Function/Basic.lean
index e01b7d06369839..02ab41cca58393 100644
--- a/Mathlib/Logic/Function/Basic.lean
+++ b/Mathlib/Logic/Function/Basic.lean
@@ -13,6 +13,7 @@ public import Mathlib.Logic.Nonempty
 public import Mathlib.Logic.Nontrivial.Defs
 public import Batteries.Tactic.Init
 public import Mathlib.Order.Defs.Unbundled
+public import Mathlib.Tactic.FunProp
 
 import Mathlib.Tactic.Attr.Register
 
diff --git a/Mathlib/Tactic/FunProp.lean b/Mathlib/Tactic/FunProp.lean
index 7a8c80711d7c59..2e50a1bff26c8c 100644
--- a/Mathlib/Tactic/FunProp.lean
+++ b/Mathlib/Tactic/FunProp.lean
@@ -353,4 +353,18 @@ There are four types of theorems that are used a bit differently.
 
 -/
 
-public meta section
+public section
+
+/-!
+### fun_prop attributes for injectivity and surhjectivity
+
+We add these here as injectivity and the associated basic results are defined in Init.
+-/
+
+open Function
+
+attribute [fun_prop] Injective injective_id Injective.comp Option.map_injective
+
+attribute [fun_prop] Surjective surjective_id Surjective.comp
+
+end
diff --git a/MathlibTest/FunPropMinimal.lean b/MathlibTest/FunPropMinimal.lean
index 72a15b155c0aa3..7e48b5ff2997d7 100644
--- a/MathlibTest/FunPropMinimal.lean
+++ b/MathlibTest/FunPropMinimal.lean
@@ -397,8 +397,12 @@ end MultipleLambdaTheorems
 #guard_msgs in
 #check_failure ((by fun_prop) : ?m)
 
-/-- error: `Injective Nat.succ` is not a `fun_prop` goal!
-Consider marking `Function.Injective` with `@[fun_prop]`. -/
+/--
+error: `fun_prop` was unable to prove `Injective Nat.succ`
+
+Issues:
+  No theorems found for `Nat.succ` in order to prove `Injective fun n => n.succ`
+-/
 #guard_msgs in
 example : Nat.succ.Injective := by fun_prop