fix: avoid kernel argument comparison in `rfl` proofs of equation lemmas

This PR fixes equation lemmas of structurally recursive functions whose `rfl` proof made the kernel reduce an expensive term, e.g. `f (n+1) x = f n (x * 1103515245 % 5)` failed with kernel deep recursion, and `cbv`, `rw`, and `simp` using such a lemma failed with it.

When both sides of the equation are applications of the function being defined, `tryURefl` now proves it by `Eq.refl` of the left-hand side unfolded once. With `Eq.refl lhs`, the kernel first compares the arguments of the two applications, starting with the last one (`x =?= x * 1103515245 % 5`), a comparison that cannot succeed for a recursive call. The proof is still an `rfl` proof, so the lemma's defeq attributes are unchanged. The duplicate `Lean.Meta.tryURefl` is removed.

Closes #15987

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>