Lean: locate position-less 'Try this: ring_nf' info with lake env lean --json

When ring fails to close a goal but ring_nf would, Lean emits an information-level 'Try this: [apply] ring_nf' message. In plain lake env lean File.lean output it can appear without the usual file:line:col header, so you cannot tell which ring it is. Run lake env lean --json File.lean and print each JSON line's severity and pos (line/column): the info message has a position there. In my case it was congr 3; ring on a goal with Nat casts, and push_cast; ring fixed it. Such info messages don't fail the build, but they are noise worth removing before calling a file clean.