important type info is omitted

[alreadydone]

Mathlib4 docs doesn't display the type of the important hypothesis x:

theorem Finset.ssubset_iff {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {t : Finset α} :
s ⊂ t ↔ ∃ a x, insert a s ⊆ t

while mathlib3 docs does:

theorem finset.ssubset_iff {α : Type u_1} [decidable_eq α] {s t : finset α} :
s ⊂ t ↔ ∃ (a : α) (H : a ∉ s), has_insert.insert a s ⊆ t

[alreadydone]

Another example:

LocalizedModule.mk_eq
(omits type of u) vs
localized_module.mk_eq

[hargoniX]

This is because the existential delaborator doesn't provide this info, if you #check the declaration in Lean you get:

⊢ ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s ⊂ t ↔ ∃ a x, insert a s ⊆ t

as you can see Lean doesn't hand out the info so there is no way doc-gen could show it.

If you wish to see this I'd suggest opening an issue for improving the existential delaborator in the Lean 4 repo directly.

An alternative here would be to set_option pp.funBinderTypes true but that would always show all the binder types everywhere, I don't know if this is something we want?

[hargoniX]

I ended up enabling this option after looking through the alternatively generated docs for a while.