Add mechanism for retrieving the original `simp` theorems.

[leodemoura]

simp currently preprocess theorems marked with [simp], and may create auxiliary theorems. For example, it will use propext for converting a <-> b into a = b. Mathlib 4 currently has to "reverse engineer" the process to find the name of the original theorems. See https://github.com/leanprover-community/mathlib4/blob/90004fda28ba90e80c9930d1bacf2aeaf28bc3a5/Mathlib/Tactic/Lint/Simp.lean#L81-L111

simp should provide this information.

See discussion at https://github.com/leanprover/lean4/pull/1544