# Zulip Chat Archive

## Stream: new members

### Topic: Simplifying inverses in ring

#### Laurent Bartholdi (Mar 22 2021 at 20:51):

Still working on @Kevin Buzzard 's homework, I stumbled on the following problem: how to simplify `A*A⁻¹*B`

in a ring? I tried everything I could, with library_search, but got nowhere. First, a version that works:

```
lemma xxx (A B C ε : ℝ) (h0 : A ≠ 0) (h1 : C-0 = ε/A) (h2 : B = A) : B*C = ε := begin
rw sub_zero at h1,
calc B*C = A*(ε/A) : by rw [h1,h2]
... = ε : mul_div_cancel' ε h0
end
```

Now let's say I didn't care to use `sub_zero`

but just hit it with `ring`

(which is how my trouble started): `ring`

will replace `ε/A`

by `A⁻¹*ε`

, thus

```
lemma xxx_fail (A B C ε : ℝ) (h0 : A ≠ 0) (h1 : C-0 = ε/A) (h2 : B = A) : B*C = ε := begin
ring at h1,
calc B*C = A*(A⁻¹*ε) : by rw [h1,h2]
... = (A*A⁻¹)*ε : by rw mul_assoc -- fails
... = ε : by rw mul_cancel_right -- fails
end
```

Again, I have a question and metaquestion: (1) can someone who reached enlightenment show me the way in xxx_fail? (2) I tried a lot of `library_search`

, which did help a little (though it gave long-to-type suggestions of the form tactic.ring.xxxx). I also tried `hint`

which waited for a long time without returning anything. Is there something like Isabelle's "sledgehammer", or a more efficient way of finding lemmas?

#### Patrick Massot (Mar 22 2021 at 21:09):

The mul_assoc rewrite is not failing

#### Patrick Massot (Mar 22 2021 at 21:10):

And `mul_cancel_right`

doesn't seem to exist. The naming convention here would have `mul_inv_cancel`

, not `mul_cancel`

alone

#### Patrick Massot (Mar 22 2021 at 21:11):

```
import data.real.basic
lemma xxx_fail (A B C ε : ℝ) (h0 : A ≠ 0) (h1 : C-0 = ε/A) (h2 : B = A) : B*C = ε := begin
ring at h1,
calc B*C = A*(A⁻¹*ε) : by rw [h1,h2]
... = (A*A⁻¹)*ε : by rw mul_assoc
... = ε : by rw [mul_inv_cancel h0, one_mul]
end
```

#### Patrick Massot (Mar 22 2021 at 21:12):

But you don't need to know all those names:

```
import data.real.basic
lemma xxx_fail (A B C ε : ℝ) (h0 : A ≠ 0) (h1 : C-0 = ε/A) (h2 : B = A) : B*C = ε := begin
ring at h1,
calc B*C = A*(A⁻¹*ε) : by rw [h1,h2]
... = (A*A⁻¹)*ε : by ring
... = ε : by field_simp [h0]
end
```

#### Patrick Massot (Mar 22 2021 at 21:13):

And `library_search`

does know it:

```
example (A : ℝ)(h0 : A ≠ 0) : A*A⁻¹ = 1 :=
by library_search
```

Last updated: May 15 2021 at 02:11 UTC