chore: make Injective and Surjective fun_propable

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
 

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

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