lookup3 alias issue?

Stream: mathlib4

[Patrick Massot]

I'm surprised by

#lookup3 function.comp_app

which says

Function.comp_apply (aliases [function.comp_app, function.comp_apply])

It seems to suggests function.comp_app and function.comp_apply exist in Lean 4, but they are in Lean 3.

[Jireh Loreaux]

Isn't that just saying that both of those Lean 3 declarations are aligned to Function.comp_apply in Lean 4?

[Patrick Massot]

That's clearly what it's trying to say, but I wanted to point out I find this confusing.

[Jireh Loreaux]

aha, maybe it could say aligned from instead of aliases.