!4#2763 RingTheory.Localization.FractionRing

Stream: mathlib4

[Matej Penciak]

Porting this file was generally uneventful, except at the end the last couple instances were having a hard time with deterministic timeouts unifying some of the _'s.

After filling them in by hand, almost everything works except the last instance which doesn't compile because Lean is unable to synthesize NoZeroSMulDivisors A (FractionRing A), whereas Lean 3 had no issues.

Any help would be appreciated!

[Eric Wieser]

Is this lean4#2074 causing issues?

[Matej Penciak]

I'm not sure, adding set_option synthInstance.etaExperiment true actually makes things worse! :grimacing:

[Jeremy Tan]

Then it's not 2074

[Eric Wieser]

Matej Penciak said:

I'm not sure, adding set_option synthInstance.etaExperiment true actually makes things worse! :grimacing:

I think it's possible to set it for a very small part of the file

[Kevin Buzzard]

set_option ... in lemma ...