Matrix multiplication issue: not quite a diamond

Stream: mathlib4

[Alex Meiburg]

Matrix n n R gets a multiplication structure from two different places, one from docs#Matrix.instRing (for square matrices), one from docs#Matrix.instHMulOfFintypeOfMulOfAddCommMonoid (for rectangular, heterogeneous matrices). As you can imagine, they both occur in the same contexts together ... sometimes I define something for rectangular matrices, but in other applications they happen to be square.

They give defeq instances, so I can unify goals that look the same, but rw doesn't recognize that they're same. So rw [← this] fails, but

conv =>
    enter [1, 1, 1, 2, 1]
    exact this.symm

made it work. (rw inside the conv also didn't work, and this is where I finally covered the issue!)

Is there a good solution to make this better? It's not as bad as a diamond, but it means that many rw's and simp's dont work for hard to understand reasons.

One thing is I could e.g. write a simp lemma (or even a dsimp proc?) that turns the rectangular one into the square one, in the cases where it happens to be applied to square matrices. That works for normalizing to the square case. But then it still means that rewriting a "rectangular" theorem onto a "square" expression still doesn't work so well.

[Ruben Van de Velde]

Sounds like the heterogeneous version should be defined first (if it isn't yet) and the ring instance should use that multiplication rather than defining its own

[Alex Meiburg]

That's actually exactly how it already is done. The issue is that rw can't see that they're the same. I'm not enough of an expert on reducibility / looking through instance / stuff to see what's wrong, though.

[Alex Meiburg]

See docs#Matrix.instMulOfFintypeOfAddCommMonoid for the actual square multiplication (not just the whole Ring), I guess

[Aaron Liu]

can you provide a #mwe

[Jovan Gerbscheid]

I think since unification sets the reducibility to default in instance implicit arguments, this is supposed to work just fine.