Why does `field_simp` leave this as the goal?

Stream: general

[Keefer Rowan]

Applying field_simp * to the somewhat complicated expression (where we have (innerc y y).re \ne 0 in the local context):

((innerc y y).re)⁻¹ * ∥innerc x y∥ * (((innerc y y).re)⁻¹ * ∥innerc x y∥) * (innerc y y).re =
    ((innerc y y).re)⁻¹ * ∥innerc x y∥ * ∥innerc x y∥

leaves the almost solved goal:

(innerc x y).abs * (innerc x y).abs * (innerc y y).re * (innerc y y).re =
    (innerc x y).abs * (innerc x y).abs * ((innerc y y).re * (innerc y y).re)

A few call to mul_assoc would solve the goal, but for some reason field_simp doesn't finish it. ring does the trick from here, but I'm wondering why field_simp can't just finish it off.

Note that everything has type $\mathbb{R}$.

[Sebastien Gouezel]

The goal of field_simp is to clear off denominators, so that ring can finish it. So the standard invocation is really field_simp [h], ring.

[Bryan Gin-ge Chen]

The fact that field_simp should be used as preparation for ring is mentioned in tactic#field_simp and the docstring, but maybe it needs more emphasis?

[Keefer Rowan]

@Bryan Gin-ge Chen Looking at it now, it's pretty well emphasized. I just didn't look at it well enough.

[Yury G. Kudryashov]

BTW, can we reassign @[simp] tags so that simp works as field_simp?

[Johan Commelin]

I think we can, why not?