Nontrivial typeclass def-eqs

Stream: mathlib4

[Chris Hughes]

I had a go at making a bunch of stuff to do with TensorProduct irreducible to see if it would improve performance in !4#3555 It didn't seem to make much difference, but it did throw up an interesting diamond. If I add the following code here then rfl fails

example : @Units.instSMulUnits (ℕˣ) (M ⊗[R] N) _ _ = TensorProduct.leftHasSMul :=
  rfl --fails

This is not a diamond in current Mathlib4 master, but the commutavity relies on the defeq a • (x ⊗ₜ y) = (a • x) ⊗ₜ y, which itself relies on unfolding everthing to AddCon and then to Quot and using the defeq Quot.lift_mk. I don't know if this is a really bad thing, but it's possible that this sort of thing is behind some of the performance problems we've been having and it's certainly worth being aware that we're doing this if we weren't already.

[Eric Wieser]

I think we're aware of this, it's the same reason that the smul on polynomial can't be irreducible (edit: see #8392)

[Eric Wieser]

If you make it irreducible then all sort of diamonds don't commute any more

[Chris Hughes]

I don't think this is a performance issue having tested it, but it is annoying that we need to think about this

[Eric Wieser]

It would be nice if we could steer defeq testing using higher-level defeqs

[Eric Wieser]

But maybe there's no sensible algorithm for that

[Chris Hughes]

It would be nice to not have to use our current notion of defeq IMO, but that's a gigantic project. I think this is basically a really hard problem.