!4#2821

Stream: mathlib4

[Jeremy Tan]

In the last theorem

@[simps!]
def Functor.toOplaxFunctor (F : I ⥤ B) : OplaxFunctor (LocallyDiscrete I) B where
  obj := F.obj
  map X Y f := F.map f.as
  map₂ i j f g η := eqToHom (congr_arg _ (eq_of_hom η))
  mapId i := eqToHom (F.map_id i)
  mapComp i j k f g := eqToHom (F.map_comp f.as g.as)
#align category_theory.functor.to_oplax_functor CategoryTheory.Functor.toOplaxFunctor

how can this kind of error message pop up?

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  CategoryStruct.toQuiver
inferred
  CategoryStruct.toQuiver

And how do I fix the "failed to synthesize instance" errors further up?

[Kevin Buzzard]

What does the error look like with set_option pp.all true on? (put it on a line of its own before the declaration)

[Eric Wieser]

This error usually means you can't use the where syntax and have to use @SomeStructure.mk (field := val) instead

[Eric Wieser]

Though that depends which line the error appears on

[Adam Topaz]

I think you need to fix the errors in the beginning of the file before worrying about the error in the last definition.

[Adam Topaz]

I only took a quick look at this file, but it seems that there are some subtle points that will show up in porting this file due to some type synonyms being used (and possibly abused in mathlib3).

[Adam Topaz]

I got the file to build (and pushed).

[Jeremy Tan]

!4#2821 the mathlib3 proof almost works perfectly in mathlib4, but at the very start the coercion is applied too strongly resulting in a rewrite failure.

I could split into cases based on the comparison between 1, a and b but that would look a bit ungainly.

Should I rewrite the proof like that or is there a more elegant way around this?

[Eric Wieser]

I will take a look today

[Jeremy Tan]

Specifically ↑(a - (b - 1)) gets reduced to (↑a - (↑b - 1)) at the start and it can't be restored without introducing assumptions (new goals) on a and b

[Jeremy Tan]

The thing is, since the overarching field is now a division ring K instead of only a semiring S, I should be able to rewrite (↑a - (↑b - 1)) back to ↑(a - (b - 1)) without generating assumptions since all elements now have additive inverses, but I can't see a function to do that

[Yaël Dillies]

Insert brackets and coercion arrows so that Lean reads it as the intended thing again.

[Jeremy Tan]

is there any other kind of coercion arrow other than ↑?

[Jeremy Tan]

Also this is not about introducing a coercion, but more about preventing one from rewriting the intended term

[Jeremy Tan]

(I am AFK right now for dinner)

[Yaël Dillies]

Yes there are other kinds of coercion, but here it's just a matter of writing ↑(a - (b - 1)) instead of a - (b - 1).

[Jeremy Tan]

whee, pushed the hotfix on mobile and the build succeeded! Thank you

[Eric Wieser]

I pushed some more fixes; there was no need to rewrite the proofs; one error was caused by implicit argument changes, and the other was a name clash