instUniformSpaceProd

Stream: mathlib4

[Matthew Ballard]

Should this be

example [UniformSpace α] [UniformSpace β] :
    (instTopologicalSpaceProd : TopologicalSpace (α × β)) = UniformSpace.toTopologicalSpace := by
 with_reducible_and_instances rfl

?

[Matthew Ballard]

In general these diamond checks at default transparency seem like an anti-pattern when we are worried about passing snuff in simp and type class synthesis

[Anatole Dedecker]

I'm no expert with reducibility, but that makes sense to me.

[Matthew Ballard]

#10010

[Eric Wieser]

It sounds like the reducible non-instances library note could do with an update to reflect the new stuff you're working out