Lean fails to apply a `simp` lemma

Stream: general

[Yury G. Kudryashov]

In #10199 I tried to generalize docs#matrix.smul_cons to the case [has_scalar M α]. With this generalization, Lean fails to apply it in data.complex.module. It can't rw [ring.hom id real c] but it can rw [ring.hom id real c z.re]. I don't understand why this happens.

[Eric Wieser]

What is docs#ring.hom?

[Yury G. Kudryashov]

Typo. ring_hom.id (it's in the goal before simp; after simp you have c instead of ring_hom.id real c)