Instance argument seems to come from nowhere

Stream: general

[Eric Wieser]

In the code annotated in this PR comment, I'm seeing some very strange behavior. The smul_tmul lemma requires an instance argument and succeeds, yet nothing is in scope to construct such an instance. If I explicitly fill out the arguments to smul_tmul (even as smul_tmul _), then lean complains about this missing instance; but if I don't, it seems to conjure it out of thin air.

[Eric Wieser]

#check @tensor_product.has_scalar' confirms the instance is not an argument

[Eric Wieser]

Ah mystery solved, this is another case of docs#mul_action.regular not being an instance, meaning it can be found via implicit arguments but not typeclass search.