This PR removes the obsolete `Lean.Environment.replay` from
`src/Lean/Replay.lean` and replaces it with the improved version from
`src/LeanChecker/Replay.lean`, which includes fixes for duplicate
theorem handling and Quot/Eq dependency ordering. The primed names
(`Replay'`, `replay'`) are renamed back to `Replay` and `replay`.
A test for the original issue (nested inductives failing with `replay`)
is added as `tests/elab/issue12819.lean`.
Closes#12819🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
