SimpNF applies scoped instance

Stream: mathlib4

[Anatole Dedecker]

The linting error in !4#3790 (on docs#affine_segment_const_vadd_image) is a bit annoying. The linter says that (v +ᵥ ·) '' affineSegment R x y can be simp-ed to v +ᵥ affineSegment R x y, but that only works when we open Pointwise, otherwise this doesn't typecheck. Nevertheless, simp seems to be able to do this simplification without the locale open (using docs4#Set.image_vadd), thus introducing in the goal view a notation that doesn't typecheck :face_with_diagonal_mouth:
Is there a known fix (except disabling the linter) ?

[Alex J. Best]

Well the goal view typechecks surely, just doesn't paste back into the goal view without opening the locale?
I think the correct fix is to make Set.image_smul and add have scoped simp attributes. I pushed this to the branch so we can see if mathlib builds. I'm not sure yet if there are other examples where this should be done, or we could lint for this.