# Zulip Chat Archive

## Stream: new members

### Topic: rw not rw'ing

#### Jake Kesinger (Oct 30 2020 at 23:40):

In this code:

```
@[simp]
lemma prod_inv_flip {R:Type*} (a:R) (b:R) [field R] (anz:a≠0)(bnz:b≠0): (a*b)⁻¹ = b⁻¹ * a⁻¹ :=
begin
field_simp,
end
@[simp]
lemma prod_inv_flip_is_inv {R:Type*} (a:R) (b:R) [field R] (anz:a≠0)(bnz:b≠0): (a*b)⁻¹ * b * a = 1 :=
begin
finish
end
@[simp]
lemma prod_inv_cancel_right {R:Type*} (a:R) (b:R) (x:R) [field R] (anz:a≠0)(bnz:b≠0) (xnz: x≠ 0):
x * (a*b)⁻¹*b*a = x :=
begin
rw prod_inv_flip_is_inv a b,
sorry,
end
```

the `rw prod_inv_flip_is_inv a b`

is failing, and I'm not understanding why.

#### Jake Kesinger (Oct 30 2020 at 23:41):

I tried `set option pp.all true`

and got this message:

```
Rewrite tactic failed, did not find instance of the pattern in the target expression
@has_mul.mul.{u_1} R
(@distrib.to_has_mul.{u_1} R
(@ring.to_distrib.{u_1} R (@division_ring.to_ring.{u_1} R (@field.to_division_ring.{u_1} R _inst_1))))
(@has_mul.mul.{u_1} R
(@distrib.to_has_mul.{u_1} R
(@ring.to_distrib.{u_1} R (@division_ring.to_ring.{u_1} R (@field.to_division_ring.{u_1} R _inst_1))))
(@has_inv.inv.{u_1} R (@field.to_has_inv.{u_1} R _inst_1)
(@has_mul.mul.{u_1} R
(@distrib.to_has_mul.{u_1} R
(@ring.to_distrib.{u_1} R (@division_ring.to_ring.{u_1} R (@field.to_division_ring.{u_1} R _inst_1))))
a
b))
b)
a
```

#### Reid Barton (Oct 30 2020 at 23:42):

That's because (despite where you put the spaces :upside_down:) `x * (a*b)⁻¹*b*a`

means `((x * (a*b)⁻¹)*b)*a`

.

#### Reid Barton (Oct 30 2020 at 23:43):

There is actually another tactic for dealing with this exact issue: `assoc_rw`

#### Jake Kesinger (Oct 31 2020 at 00:00):

thanks!

`assoc_rw`

did the trick, and with `ring`

I was able to finish all goals, but I was getting failures saying "result contains meta-variables".

I found in another thread the `recover`

goal, and from that was able to call `exact`

a couple times to clear hypotheses, but the "For debugging only" in the description of `recover`

is making me nervous

#### Kevin Buzzard (Oct 31 2020 at 00:05):

This is normally down to a buggy tactic. Can you post a #mwe?

#### Jake Kesinger (Oct 31 2020 at 00:13):

trying to minimize now

#### Jake Kesinger (Oct 31 2020 at 00:18):

```
import data.real.basic
namespace mwe
@[simp]
lemma abcd_is_adbc {R:Type*} (a:R) (b:R) (c:R) (d:R) [comm_monoid R] : a*b*c*d = a*d*b*c :=
begin
finish
end
@[simp]
lemma prod_inv_flip {R:Type*} (a:R) (b:R) [field R] (anz:a≠0)(bnz:b≠0): (a*b)⁻¹ = b⁻¹ * a⁻¹ :=
by {field_simp}
@[simp]
lemma prod_inv_flip_is_inv {R:Type*} (a:R) (b:R) [field R] (anz:a≠0)(bnz:b≠0): (a*b)⁻¹ * b * a = 1 :=
by {finish}
@[simp]
lemma prod_inv_cancel_right {R:Type*} (a:R) (b:R) (x:R) [field R] (anz:a≠0)(bnz:b≠0) (xnz: x≠ 0):
x * (a*b)⁻¹*b*a = x :=
begin
assoc_rw prod_inv_flip_is_inv a b,
ring,
recover,
exact bnz,
exact anz,
end
end mwe
```

#### Floris van Doorn (Oct 31 2020 at 03:40):

It seems like `assoc_rw`

doesn't handle hypotheses well in a partially applied term. @Simon Hudon

As a workaround, `assoc_rw prod_inv_flip_is_inv a b _ _`

produced 3 goals as expected.

#### Simon Hudon (Oct 31 2020 at 03:50):

Would you mind filing a bug with this information and tagging me?

#### Floris van Doorn (Oct 31 2020 at 03:52):

#### Simon Hudon (Oct 31 2020 at 03:59):

Thanks!

Last updated: May 06 2021 at 22:13 UTC