OrderTop (Opens X) won't synthesize

Stream: general

[Brian Nugent]

Here is a #mwe

import Mathlib

open TopologicalSpace

variable (X : Type) [TopologicalSpace X]

#synth OrderTop (Opens X)

When I run it on https://live.lean-lang.org/ using Latest Mathlib I get a "can't synthesize" error but when I run it on stable Mathlib it work's fine.

[Brian Nugent]

On stable mathlib it synthesizes using
Opens.instCompleteLattice.toOrderTop so I'm not sure if its toOrderTop or Opens.instCompleteLattice that's failing.

[Weiyi Wang]

The latest Mathlib (4.29.0-rc1) is slightly "broken" (See #announce > releases of new Lean versions @ 💬 )
You can add set_option backward.isDefEq.respectTransparency false on the top to fix this

[Brian Nugent]

Ok, thank you!

[Eric Wieser]

Weiyi Wang said:

The latest Mathlib (4.29.0-rc1) is slightly "broken" (See #announce > releases of new Lean versions @ 💬 )
You can add set_option backward.isDefEq.respectTransparency false on the top to fix this

I suspect it is not mathlib that is broken here, but (the release candidate of) Lean