Curiosity about class instances in mathlib docs

Stream: new members

[Pedro Minicz]

Shouldn't [topological_space (subtype p)] be required by this definition?
tmp.png

[Pedro Minicz]

I am not with Lean right now, but I feel like it should be in the context, otherwise how would is be able to make sense of is_closed for subtype p?

[Heather Macbeth]

I believe it's inferred automatically, docs#subtype.topological_space

[Pedro Minicz]

Definition is here. It may also be just that the docs aren't showing the instance.

[Pedro Minicz]

Yes, it should be inferred automatically. Therefore it should be included in the type full type signature as a hidden argument, right?

[Heather Macbeth]

Rather, I believe the classes that appear in the full type signature are those that are not inferred automatically.

[Johan Commelin]

@Pedro Minicz Luckily not... otherwise everything that uses a little bit of ring theory would show an insane amount of type class arguments.

[Pedro Minicz]

:thinking:

[Pedro Minicz]

It makes sense. That had never occurred to me.

[Yury G. Kudryashov]

This lemma doesn't take an instance of [topological_space (subtype p)] with some unknown properties. Instead, there is subtype.topological_space hidden in the implicit arguments of t1_space (subtype p). Actually, it is something like @t1_space (subtype p) (@subtype.topological_space α p t), where [t : topological_space α].