Missing definitional theorems

Currently Function.Surjective is defined to be a Prop, but there is no Function.surjective_def or Function.surjective_iff, which makes it impossible to unfold it using rw. Now there is the auto-generated Function.Surjective.eq_def which works in this case, but I think it's bad to rely on an auto-generated name, and Loogle currently cannot discover such lemmas.

Here's a script to find the 1398 definitions currently in Mathlib without a def lemma:

import Mathlib

def Test (f : Nat → Nat) : Prop := f 3 = 4

open Lean Elab Command

/-- `Foo.Bar` => `Foo.bar_def` -/
def Lean.Name.to_def : Name → Name
  | .str n s => n.str <| String.Pos.Raw.modify s 0 Char.toLower ++ "_def"
  | x => x

/-- `Foo.Bar` => `Foo.bar_iff` -/
def Lean.Name.to_iff : Name → Name
  | .str n s => n.str <| String.Pos.Raw.modify s 0 Char.toLower ++ "_iff"
  | x => x

#eval (`Foo.Bar).to_iff
#eval (`Foo.Bar).to_def

#eval show CommandElabM Unit from do
  let env ← getEnv
  let mut output := ""
  let mut i := 0
  for (name, val) in env.constants.toList do
    let .defnInfo val := val | continue
    let .regular _ := val.hints | continue
    let .safe := val.safety | continue
    if val.type.getForallBodyMaxDepth 100 == .sort 0 then
      if env.constants.contains name.to_def then continue
      if env.constants.contains name.to_iff then continue
      i := i + 1
      output := output ++ s!"{name}\n"
  IO.println s!"{i} definitions found:"
  IO.println output

Start by inspecting the definition of Function.Surjective and the supplied Lean script that scans for definitions without _def or _iff lemmas. Determine the intended scope from the reported 1398 definitions, then verify that the affected definitions have discoverable named definitional theorems rather than relying on generated eq_def names.