How, broadly, does Lean infer implicit arguments?

Stream: new members

[Johan Commelin]

@Chris M If f x has type T, and this T already mentions x, then you can replace x by _.

[Johan Commelin]

Similarly if you have f x hx, and hx mentions x, then you can write f _ hx.

[Kevin Buzzard]

When I'm coding, if lean is asking for a variable and I know that it can be worked out from what's going on, or even if I think it can, I leave it out on the principle that shorter code is clearer.