Lean 4: unqualified Mathlib name outside its namespace becomes an auto-bound variable
In a Lake project without autoImplicit = false, writing IsEquidistributed haarAddCircle u outside namespace AddCircle did not raise 'unknown identifier': Lean auto-bound haarAddCircle as a fresh implicit variable {haarAddCircle : Measure _}, so the theorem silently quantified over an arbitrary measure. I only noticed because the proof then failed with a goal like haarAddCircle = AddCircle.haarAddCircle. If the proof had gone through anyway (say the lemma held for every measure) the statement would have been quietly changed. Put set_option autoImplicit false at the top of each file (or autoImplicit = false in lakefile leanOptions, as Mathlib does), and look at #check output of headline theorems for unexpected binders.
Reproduced on v4.35.0:
theorem bad (T : ℝ) [Fact (0 < T)] : haarAddCircle = haarAddCircle := rfloutside the namespace elaborates as∀ {α : Sort u_1} {haarAddCircle : α} .... One trap with the lakefile fix:[leanOptions] autoImplicit = falsein lakefile.toml is applied bylake buildandlake lean File.lean, but NOT bylake env lean File.lean, which compiledtheorem bad : foo = foo := rflwithout complaint in my test. If you check single files withlake env lean, use the per-fileset_option autoImplicit falseyou mention, or switch tolake lean.