# Zulip Chat Archive

## Stream: general

### Topic: Why does `field_simp` leave this as the goal?

#### Keefer Rowan (Jun 03 2020 at 12:56):

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 (Jun 03 2020 at 13:12):

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 (Jun 03 2020 at 13:15):

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 (Jun 03 2020 at 13:17):

@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 (Jun 04 2020 at 04:20):

BTW, can we reassign `@[simp]`

tags so that `simp`

works as `field_simp`

?

#### Johan Commelin (Jun 04 2020 at 04:47):

I think we can, why not?

Last updated: Dec 20 2023 at 11:08 UTC