How to find suitable instances?

Stream: new members

[Michał Pacholski]

Hi! I'm just starting with Mathlib, and I'm a bit confused about using instances. For example I want to have topology on a product of unit intervals

import Mathlib.Topology.UnitInterval
import Mathlib.Topology.Constructions.SumProd

def unitSquare := unitInterval × unitInterval

#check instTopologicalSpaceProd
-- instTopologicalSpaceProd.{u, v} {X : Type u} {Y : Type v} [t₁ : TopologicalSpace X] [t₂ : TopologicalSpace Y] : TopologicalSpace (X × Y)

#check IsOpen (Set.univ : Set unitInterval)
-- checks

#check IsOpen (Set.univ : Set unitSquare)
-- failed to synthesize TopologicalSpace unitSquare

Why does it fail to synthesize? I'd expect that having instTopologicalSpaceProd, Lean would find the suitable instance automatically. If not, then how should it be done?

[Aaron Liu]

Make it an abbrev

[Jakub Nowak]

Note that

#check IsOpen (Set.univ : Set (unitInterval × unitInterval))

works.

abbrev makes it so that lean sees past the definition when searching for instances.