feat: `Simp.Config.implicitDefEqProofs`

[leodemoura]

This PR implements Simp.Config.implicitDefEqsProofs. When true (default: false), simp will not create a proof for a rewriting rule associated with an rfl-theorem. Rewriting rules are provided by users by annotating theorems with the attribute @[simp]. If the proof of the theorem is just rfl (reflexivity), and implicitDefEqProofs := true, simp will not create a proof term which is an application of the annotated theorem.

Users can use simp (config := { implicitDefEqProofs := true }) to restore old behavior.

This PR also fixes an issue in the split tactic that has been exposed by this feature. It was looking for split candidates in proofs and implicit arguments. See new test for issue exposed by the previous feature.