Question about implicit coercions and the linter

Stream: mathlib4

[zbatt]

In this PR I was having some issues with the linter. As mo271 pointer out, if you don't rely on implicit coercion and change f x to f.toRingEquiv x you can solve the issues. That being said, using .toRingEquiv is a bit uglier in my opinion, and neither of us are sure how to go about handling this issue. Does anyone have any advice?

[Eric Wieser]

The solution here is to implement the docs#fun_like boilerplate in Lean3 first

[Eric Wieser]

I think we should do a cleanup pass of every docs#has_coe_to_fun instance in Lean 3 and create the docs#fun_like instances

[zbatt]

In the meantime, is there a way I should handle this PR (either adding a type class to fix this specifically or something else) or should I wait until what you suggested happens?

[Lukas Miaskiwskyi]

Of course if you want to move PRs like this forward, you can always try to construct the necessary stuff to lean3 yourself first :) But I understand that this is difficult here. I myself have tried to understand how Homs should be coerced in the last days, and it has been a path of learning, but mostly a path of suffering.

But if I now have a somewhat reliable picture about this (big if!), I think this is close to the issues we've been having with Algebra.Hom.GroupAction. As I understand, the preferred way to implement coercions for Hom structures is by extending them together with their corresponding HomClass classes, defining a HomClass.toHom function, implementing an instance of Homs as HomClasses, and finally implementing a CoeTC instance that handles coercion from instances of HomClass (Look at Algebra.Ring.Equiv with HomClass = RingEquivClass for a close example of this). But, eh, yeah, this is complicated.

Regardless, I think a first step is creating a ring_invo_class class in mathlib3 first, which does not exist, even though it should, since every time ring_equiv is extended, ring_equiv_class should be, too. I pushed a PR for this in #18175. I'll also push some changes which I think are good for the mathlib4 file.

[zbatt]

Thanks so much!! This is a bit confusing, but at least big picture I have a much better idea of what's to happen. Out of curiosity, since your changes will enable RingInvo to be ported to mathlib4 successfully, will anything need to happen with the changes you made in mathlib3 in terms of "re-porting" to mathlib4, or do we now just consider RingInvo done with the PR you put to mathlib3 "back-ported" so to speak

[Lukas Miaskiwskyi]

I think it's good to first wait for the PR to mathlib3 to be merged, and then we can see how to process with the mathlib4 file. That being said, my changes have reintroduced another #lint error, which has problems with RingInvo.map_eq_zero_iff being @[simp]. So we're not done either way :D

[zbatt]

oops I fixed the lint issue, I can unfix it if you want to mark it as not ready to merge until the mathlib3 PR is done