How broadly does Lean infer implicit arguments?

Stream: new members

[Chris M]

I'm unsure how exactly I can predict when Lean will be able to infer an implicit argument, i.e. when I can use f _ instead of f y. I could just use trial and error, but is there a simple, principled idea of when it is possible or not for Lean to infer something?