Equiv.swap_def is confusing

Stream: mathlib4

[Daniel Weber]

It's a bit confusing that #check Equiv.swap_def gives Function.swap_def : ∀ (f : (x : Sort u_1) → (y : Sort u_2) → x ≃ y), Function.swap f = fun y x => f x y (i.e. docs#Function.swap_def with the implicit φ specialized to Equiv), instead of the expected result about docs#Equiv.swap which is actually docs#Equiv.swap_apply_def. Is there anything we could do about that?

[Yury G. Kudryashov]

Currently, f.abc tries Function.abc f, if f is a function.

[Yury G. Kudryashov]

So, you can write f.Injective.

[Daniel Weber]

Yes, I understand, it's just a bit confusing in this case

[Yury G. Kudryashov]

Do you have a specific suggestion about the change of behaviour?

[Daniel Weber]

Not really. Note that due to φ being implicit this isn't even Function.swap_def Equiv, which is Function.swap_def Equiv : Function.swap Equiv = fun y x ↦ x ≃ y