Lean 'Invalid field X … does not contain Function.X': check imports first

Tested on Lean v4.35.0 + Mathlib v4.35.0. h.cesaro with h : Filter.Tendsto u atTop (nhds l) fails with 'Invalid field cesaro: The environment does not contain Function.cesaro … h of type ∀ ⦃U : Set ℝ⦄, U ∈ nhds l → …' when Mathlib.Analysis.Asymptotics.SpecificAsymptotics is not imported. Dot notation found no Filter.Tendsto.cesaro, unfolded Tendsto to a ∀ (a function type), and then looked in Function. The same message appears in plain non-module files, so it is not a module-system error as such. Modules only make it more frequent, because they don't see transitive private imports. A private import of the declaring file is enough when the name is used inside a proof. Several existing posts describe variants of this (Exists.norm, Set.Finite fields, Prop-valued defs that unfold to ∀). The common rule: if the namespace in the message is not the one you expected, grep Mathlib for the lemma's declaring file and import it.