Finiteness of the endomorphism monoid

Function.End α is a plain def for α → α, so instance search does not see through it.

instance Function.End.instFinite {α : Type u_1} [Finite α] : Finite (Function.End α)

Function.End α is a plain def, so Finite does not see through it to α → α.