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`.
leanprover-community · May 3, 2024 · aec9cad · aec9cad
1 parent 3025cb1
commit aec9cad
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/Std/Logic.lean b/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