docs dont show type for existential quantifiers

Stream: general

[Felix Weilacher]

I think the appearance of theorems like the following is pretty bad. I believe in the mathlib 3 docs the types of s and f were shown.
Screenshot-2023-09-08-at-8.31.58-PM.png

[Bhavik Mehta]

image.png
Here's the mathlib3 version

[Eric Wieser]

Note that this isn't just the docs, but also the info view when using lean