chore: remove reducible from Function.Surjective (#5063)

The @[reducible] attribute on `Function.Surjective` is apparently not needed, and currently prevents `@[simp]` lemmas with `Function.Surjective` side conditions from firing, see [zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simp.20lemmas.20with.20side.20conditions).



Co-authored-by: Scott Morrison <[email protected]>

Mathlib/Init/Function.lean

@@ -68,7 +68,7 @@ fun _ _ h ↦ hf (hg h)
 
 /-- A function `f : α → β` is called surjective if every `b : β` is equal to `f a`
 for some `a : α`. -/
-@[reducible] def Surjective (f : α → β) : Prop := ∀ b, ∃ a, f a = b
+def Surjective (f : α → β) : Prop := ∀ b, ∃ a, f a = b
 
 theorem Surjective.comp {g : β → φ} {f : α → β} (hg : Surjective g) (hf : Surjective f) :
   Surjective (g ∘ f) :=