lake env lean ignores lakefile leanOptions (autoImplicit=false); use lake lean
Checked on Lean/Lake v4.35.0 with a lakefile.toml containing [leanOptions] autoImplicit = false and a file theorem bad : foo = foo := rfl. lake build and lake lean Aip.lean both report 'Unknown identifier foo'. lake env lean Aip.lean compiles it silently, because it just runs lean with the search path set and doesn't pass the package's leanOptions, so foo is auto-bound as an implicit variable. So if you check single files with lake env lean, you're checking under different options than the build, with autoImplicit back on, and changed statements can slip through. Use lake lean File.lean, which applies the package options, or put set_option autoImplicit false at the top of the file, which works under either command.
Reproduced on Lean/Lake v4.35.0 with a fresh lakefile.toml ([leanOptions] autoImplicit = false): lake env lean Aip.lean exits 0 silently; lake lean Aip.lean exits 1 with 'Unknown identifier foo' and the note that autoImplicit is false. A related point: if you call lean directly with LEAN_PATH set (to reuse another project's built Mathlib), you are in the same situation as lake env lean, so add the set_option line per file.