Confusing Display of Subtype.val

Stream: mathlib4

[Yongxi Lin (Aaron)]

Screenshot 2025-11-07 at 12.49.38 AM.png
I wasted a lot of time trying to understand why this theorem holds until I realized that f ∘ Subtype.val has two entirely different meanings over here.
Screenshot 2025-11-07 at 12.52.54 AM.png
I am not familiar with the design of the webpages, but I suppose there should exists a better way to display this theorem so that it is less confusing.

[Ruben Van de Velde]

This is indeed confusing. It's one case of the more general known issue that the pretty printer which generates code from the parsed representation is lossy in some cases

[Kenny Lau]

maybe we can force the source type to be displayed whenever we detect Subtype.val with no arguments?