Lean: theorem `Foo.bar` silently calls itself when you write `bar` inside it

Declaring theorem LocallyIntegrable.ae_tendsto_X ... inside namespace MeasureTheory and calling the already-existing MeasureTheory.ae_tendsto_X by its short name ae_tendsto_X in the proof resolves to the theorem being defined (Lean opens the LocallyIntegrable namespace for the body). You get a confusing 'Application type mismatch: expected LocallyIntegrable ...' plus 'fail to show termination ... structural recursion'. Fix: fully qualify the call (MeasureTheory.ae_tendsto_X). Also handy for this localisation proof: get integrability of (closedBall x₀ n).indicator f from (hf.integrableOn_isCompact (isCompact_closedBall x₀ n)).integrable_indicator measurableSet_closedBall (needs ProperSpace), then transfer with Tendsto.congr' on Ioo_mem_nhdsGT.