can't synthesize ContinuousInv₀ ℝ

Stream: general

[Yongxi Lin (Aaron)]

I encountered the following weird issue on https://live.lean-lang.org:

import Mathlib
-- can't synthesize
#synth ContinuousInv₀ ℝ

This should follow from NormedDivisionRing.to_continuousInv₀ right?

[Michael Rothgang]

Yes, it kind of does: here's an #mwe for you

import Mathlib

#synth NormedDivisionRing ℝ

/--
error: failed to synthesize
  ContinuousInv₀ ℝ

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
#guard_msgs in
#synth ContinuousInv₀ ℝ

example : ContinuousInv₀ ℝ := by
  apply NormedDivisionRing.to_continuousInv₀

[Michael Rothgang]

(I'm not sure why this is, and don't have time to debug this right now.)

[Thomas Murrills]

set_option backward.isDefEq.respectTransparency false causes #synth ContinuousInv₀ ℝ to succeed; here's the relevant synthInstance trace:

[Meta.synthInstance] ❌️ ContinuousInv₀ ℝ ▼
  [] new goal ContinuousInv₀ ℝ ▶
  [] ❌️ apply @IsTopologicalDivisionRing.toContinuousInv₀ to ContinuousInv₀ ℝ ▶
  [] ❌️ apply @NormedDivisionRing.to_continuousInv₀ to ContinuousInv₀ ℝ ▼
    [tryResolve] ❌️ ContinuousInv₀ ℝ ≟ ContinuousInv₀ ?m.5
  [] ❌️ apply @IsStrictOrderedRing.toContinuousInv₀ to ContinuousInv₀ ℝ ▶
  [] result <not-available>

[Eric Wieser]

That was going to be my guess. It's still set by default in mathlib, right?

[Eric Wieser]

Perhaps we should set it by default on the web editor too

[Thomas Murrills]

(Also, I should note that the most-nested ≟ failure in full is

@ContinuousInv₀ ℝ Real.instZero Real.instInv PseudoMetricSpace.toUniformSpace.toTopologicalSpace
  ≟
@ContinuousInv₀ ?m.5 Ring.toNonAssocRing.toNonUnitalNonAssocSemiring.toMulZeroClass.toZero
  DivisionMonoid.toDivInvOneMonoid.toInvOneClass.toInv PseudoMetricSpace.toUniformSpace.toTopologicalSpace

I would guess these instances would be defeq if we filled the mvar, but I'm not familiar with the hierarchy here. And also am too busy to debug further :grinning_face_with_smiling_eyes:)

[Snir Broshi]

Eric Wieser said:

Perhaps we should set it by default on the web editor too

https://github.com/leanprover-community/lean4web/issues/89 could be relevant (but won't help new members)

[Eric Wieser]

Or maybe a more global fix; release a Lean 4.28.0rc2 with this option set to false by default, since this kind of thing is just broken for everyone

[Violeta Hernández]

I would hope for rc2 to actually solve the issues with respectTransparency, not just hide them!

[Eric Wieser]

I agree, but an rc2 that hides them might take the pressure off for an rc3 that fixes them!