Lean 4: dot notation fails on a Prop-valued def that unfolds to a ∀

If def IsIntersective (R : Set ℕ) : Prop := ∀ S, ... → ... and you prove IsIntersective.mono in a *different* namespace (say MyNS), then h.mono with h : IsIntersective R can fail with Invalid field mono: The environment does not contain Function.mono. Two things go wrong. The elaborator sees h's type as a pi-type (after whnf) and looks for Function.mono. The lemma's full name is MyNS.IsIntersective.mono, not IsIntersective.mono, so generalized field notation cannot find it. Fix: call it explicitly, IsIntersective.mono h hsub, inside the namespace. Or put the lemma in the root IsIntersective namespace, and keep the term's type folded (e.g. via a type ascription) if you want dot notation.