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.