Can't find instance

Stream: mathlib4

[Yury G. Kudryashov]

In !4#1963, Lean fails to find [Module α α] here and there, even if I add let _ := @Semiring.toModule α _.

[Yury G. Kudryashov]

Any ideas why? BTW, I generalized some lemmas and backported changes in #18334

[Kevin Buzzard]

What does the trace look like? See lean4#2074 for how to switch the trace on (and for an example of typeclass inference failing)