issue with `AddGroup R` instance

Stream: mathlib4

[Tomas Skrivan]

There are two ways how to synthesize AddGroup G that are not defeq under reducible transparency. It is causing me issues when using simplifier.

import Mathlib

example {R} [NormedAddCommGroup R] :
  (NormedAddGroup.toAddGroup : AddGroup R)
  =
  (AddCommGroup.toAddGroup : AddGroup R) := by with_reducible rfl

The proof works with plain rfl but not with with_reducible rfl, is this expected behavior or not?

[Matthew Ballard]

Uh oh

[Matthew Ballard]

What is the blocker?

[Tomas Skrivan]

I didn't investigate yet

[Matthew Ballard]

This is intentional by with_reducible_and_instances rfl works

[Tomas Skrivan]

Ohh I'm stupid :man_facepalming: hmm then I do not understand why the (← withReducibleAndInstances <| isDefEq x val) check in simplifier fails on this. I have to investigate more.

[Matthew Ballard]

FWIW, I think it's easy to forget that instance projections are not reducible