See Mathlib.Data.Set.Image, _root_.function.injective.mem_set_image is defined under the namespace set, but is translated to Function.Injective.mem_set_image without the _root_ prefix, thus causing the definition to become Set.Function.Injective.mem_set_image.
See
Mathlib.Data.Set.Image,_root_.function.injective.mem_set_imageis defined under the namespaceset, but is translated toFunction.Injective.mem_set_imagewithout the_root_prefix, thus causing the definition to becomeSet.Function.Injective.mem_set_image.