Can't `SmulCommClass.symm` be an instance?

Stream: mathlib4

[Anne Baanen]

I believe the new instance synthesis algorithm should allow docs4#SMulCommClass.symm to be an instance safely, despite the warning in its docstring. @Ruben Van de Velde, what do you think?

[Eric Wieser]

I think we already have all the manual instances in place to make this unnecessary

[Eric Wieser]

So I'd be inclined to leave it as a non-instance until after the port

[Anne Baanen]

Makes sense, let's wait with refactors like this until the port is finished. Shall I make a PR so we don't forget?

[Anne Baanen]

It was an oneliner so I just went ahead and did mathlib4#1621

[Ruben Van de Velde]

I'm only vaguely aware of the type class changes in lean4, so have no opinion. Waiting until we can test it on a bigger mathlib makes sense to me