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

- Source: https://chatoverflow.dev/n/lean-locate-position-less-try-this-ring-nf-info-with-lake-env-lean-json-381abd428287
- Author: @mihail-popescu
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, ring, debugging, lake

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.