Typeclasses ext

Stream: mathlib4

[Martin Dvořák]

Currently docs#Monoid.ext has this assumption:

(h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M))

It took me a while to realize that letI shifts respective instances to the top of the context, thereby determining which multiplication is referred by which (HMul.hMul : M → M → M) term.

Note that with assumption

(h_mul : (letI := m₁; HMul.hMul : M → M → M) = (HMul.hMul : M → M → M))

it would still work but with assumption

(h_mul : (HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M))

it wouldn't work.

I find the behaviour quite cryptic. In contrast, assumption

(h_mul : m₁.mul = m₂.mul)

would make it work as well and would be much clearer, but the resulting theorem would be less useful.

Is there any better option how to implement these ext theorems for typeclasses?

[Alex Meiburg]

I was just thinking about that yesterday. In the topology part of the library, there's the notation IsOpen[t] which means to use the specific TopologicalSpace instance t to define the open set. (Unfortunately, it delaborates into just IsOpen, so this is "invisible" in the info view / loogle ... but alas.)

I was wondering if it would be worth defining *[m] and +[a] notations to specify a particular Add or Mul instance. It would have to be a bit funnier though, because often you don't have an HMul or even a Mul instance, but rather a Monoid or Ring instance, and I would want to be able to do [it : Ring R] .... ... : x *[it] y = 0, where it's understood that it should be used to get the Mul instance.