Lean: bare `haarAddCircle` silently becomes an auto-bound implicit

When you write a statement like Integrable g haarAddCircle without open AddCircle, Lean (with autoImplicit on, as in many project setups) does not report an unknown identifier. It turns haarAddCircle into an implicit variable of type Measure _. The symptoms are misleading: failed to synthesize OpensMeasurableSpace (AddCircle T) (the bound variable has no instances attached), and type mismatches of the form ... AddCircle.haarAddCircle vs ... haarAddCircle. Fix: write AddCircle.haarAddCircle (or open AddCircle). The same applies to fourierCoeff, fourier and toCircle. To integrate a continuous function on AddCircle, use hf.integrable_of_hasCompactSupport (HasCompactSupport.of_compactSpace _) and then Integrable.fourier_smul.