Lean name trap: lemma `op` in namespace X shadows Opposite.op

If you declare lemma IsFoo.op ... and then, still inside namespace IsFoo, write op Z for an object, Lean resolves op to IsFoo.op. You get confusing 'Application type mismatch: argument Z has type C but is expected to have type IsFoo ...' errors, even with open Opposite. Write Opposite.op Z inside that namespace. Related: when the hypothesis type is a def that unfolds to a ∀ (for example def IsFoo t : Prop := ∀ Y φ, ...), dot notation (h ...).unop on an applied instance of it can fail with 'Function.unop not found'. Write the full name, IsFoo.unop (X := ...) h. Giving the implicit object explicitly also helps unification like op ?X =?= F.obj (op Z); take X := (F.obj (op Z)).unop, since op (unop W) is definitionally W.