refactor: move Function.id_def from mathlib (#755)

* Move the theorem from `Mathlib.Logic.Function.Basic` to Std.
* We need this theorem to prove `String.splitOn_of_valid`.

Author: chabulhwi

Diff for: Std/Logic.lean

@@ -12,6 +12,10 @@ instance {f : α → β} [DecidablePred p] : DecidablePred (p ∘ f) :=
 
 @[deprecated] alias proofIrrel := proof_irrel
 
+/-! ## id -/
+
+theorem Function.id_def : @id α = fun x => x := rfl
+
 /-! ## exists and forall -/
 
 alias ⟨forall_not_of_not_exists, not_exists_of_forall_not⟩ := not_exists