# Zulip Chat Archive

## Stream: new members

### Topic: mul_left_cancel for integral domains

#### Damiano Testa (Sep 21 2020 at 11:46):

Dear All,

I would like to use the fact that in an integral domain, every non-zero element is left-cancellable (see the #mwe below). Is this lemma already in mathlib and I have simply been unable to find it?

Thank you!

```
import tactic
lemma xxv {R : Type*} [comm_ring R] [is_integral_domain R] {x y z : R} {h : x ≠ 0} : x*y=x*z → y=z :=
begin
sorry,
end
```

#### Johan Commelin (Sep 21 2020 at 11:47):

`mul_left_cancel`

hopefully?

#### Johan Commelin (Sep 21 2020 at 11:48):

Maybe with a `'`

, if the other version is for groups

#### Damiano Testa (Sep 21 2020 at 11:50):

I tried, but I was unable to make it work...

#### Kevin Buzzard (Sep 21 2020 at 11:51):

I'll give it a go

#### Shing Tak Lam (Sep 21 2020 at 11:52):

If you change `is_integral_domain`

to `integral_domain`

, then `mul_left_cancel'`

works btw

#### Kevin Buzzard (Sep 21 2020 at 11:52):

Aah, that's the issue: `is_integral_domain`

isn't the way to say an integral domain.

#### Damiano Testa (Sep 21 2020 at 11:52):

Shing Tak Lam said:

If you change

`is_integral_domain`

to`integral_domain, then`

mul_left_cancel'` works btw

Ah, this might fix it for me, then!

#### Kevin Buzzard (Sep 21 2020 at 11:52):

You should delete `comm_ring R`

and use `integral_domain R`

#### Damiano Testa (Sep 21 2020 at 11:52):

Let me try!

#### Damiano Testa (Sep 21 2020 at 11:56):

I am trying

```
lemma xxv [integral_domain R] {x y z : R} {h : x ≠ 0} : x*y=x*z → y=z :=
begin
apply mul_left_cancel',
exact h,
end
```

but I get this error:

```
invalid type ascription, term has type
x ≠ 0
but is expected to have type
x ≠ 0
state:
R : Type u_1,
_inst_1 : semiring R,
_inst_2 : integral_domain R,
x y z : R,
h : x ≠ 0
⊢ x ≠ 0
```

#### Kevin Buzzard (Sep 21 2020 at 11:58):

```
import tactic
lemma xxv (R : Type) [integral_domain R] {x y z : R} {h : x ≠ 0} : x*y=x*z → y=z :=
begin
apply mul_left_cancel',
exact h,
end
```

works for me.

#### Shing Tak Lam (Sep 21 2020 at 11:59):

I'm not sure why, but I think the `semiring R`

instance is affecting things

#### Shing Tak Lam (Sep 21 2020 at 11:59):

you probably have `variable [semiring R]`

somewhere? I can reproduce the error if I add a `semiring R`

typeclass

```
import tactic
lemma xxv {R : Type*} [semiring R] [integral_domain R] {x y z : R} {h : x ≠ 0} : x*y=x*z → y=z :=
begin
apply mul_left_cancel',
exact h, -- Same error
end
```

#### Damiano Testa (Sep 21 2020 at 12:00):

Yes, my standing assumption is that `R`

is a semiring

#### Kevin Buzzard (Sep 21 2020 at 12:00):

Interesting

#### Reid Barton (Sep 21 2020 at 12:01):

I wonder if it's worth trying to improve these error messages, or we should just wait for :four_leaf_clover:

#### Kevin Buzzard (Sep 21 2020 at 12:01):

But an integral domain is a semiring so you should maybe just start afresh with some new variable which is an integral domain

#### Damiano Testa (Sep 21 2020 at 12:01):

I will remove this assumption now. In case someone is further interested, here is what happens if I try to `convert h`

. Lean wants me to prove:

```
⊢ cancel_monoid_with_zero.to_monoid_with_zero R = semiring.to_monoid_with_zero R
```

#### Johan Commelin (Sep 21 2020 at 12:01):

Yup, but those are two completely different `0`

s (-;

#### Kevin Buzzard (Sep 21 2020 at 12:02):

You can't prove this, because one has come from `[semiring R]`

and one has come from `[integral_domain R]`

. That's exactly the difference between `integral_domain`

and `is_integral_domain`

#### Johan Commelin (Sep 21 2020 at 12:02):

You assumed two semiring instances (one coming from the integral domain) but Lean doesn't know any compatibility between them.

#### Damiano Testa (Sep 21 2020 at 12:02):

Ok, I will remove the semiring assumption

#### Kevin Buzzard (Sep 21 2020 at 12:02):

You should remove the `[semiring R]`

assumption because type class inference knows that an integral domain is a semiring

#### Kevin Buzzard (Sep 21 2020 at 12:03):

so all the stuff you just proved about semirings will all work fine when you're rewriting it in some lemmas about integral domains

#### Damiano Testa (Sep 21 2020 at 12:04):

Thank you all for the help! For the record, this now is a working lemma:

```
lemma xxv {RR : Type*} [integral_domain RR] {x y z : RR} {h : x ≠ 0} : x*y=x*z → y=z :=
begin
apply mul_left_cancel' h,
end
```

#### Kevin Buzzard (Sep 21 2020 at 12:04):

now see if you can do it in term mode :-)

#### Damiano Testa (Sep 21 2020 at 12:06):

I would love to, but I would need to learn how to communicate to Lean in term mode... Ahahaha

#### Reid Barton (Sep 21 2020 at 12:07):

hint: the term-mode proof is a substring of the tactic proof

#### Damiano Testa (Sep 21 2020 at 12:10):

Ok, I am making the guess that I should remove characters from `apply `

, since I imagine that the name of the lemmas in mathlib appear identically in term mode!

#### Johan Commelin (Sep 21 2020 at 12:10):

`begin`

means entering tactic mode

#### Johan Commelin (Sep 21 2020 at 12:10):

and `end`

stops it.

#### Johan Commelin (Sep 21 2020 at 12:11):

Indeed, `apply`

takes a little bit of term mode as argument, and does something useful with it.

#### Damiano Testa (Sep 21 2020 at 12:11):

ah, so i should remove from `begin apply [] end`

I will keep `by`

! Ahahaha

#### Johan Commelin (Sep 21 2020 at 12:11):

No `by`

also enters tactic mode

#### Reid Barton (Sep 21 2020 at 12:12):

To be more specific, a consecutive substring :upside_down:

#### Kevin Buzzard (Sep 21 2020 at 12:12):

`by {...}`

and `begin ... end`

are the two ways to enter tactic mode from term mode. `exact ...`

is the way to enter term mode from tactic mode.

#### Johan Commelin (Sep 21 2020 at 12:13):

@Damiano Testa Did you know that `mul_left_cancel'`

is a function?

#### Johan Commelin (Sep 21 2020 at 12:13):

Your lemma `xxv`

is also a function

#### Reid Barton (Sep 21 2020 at 12:21):

Regarding the error, if you `set_option pp.numerals false`

, then you get an error which shows the issue:

```
error: invalid type ascription, term has type
x ≠
@has_zero.zero R
(@mul_zero_class.to_has_zero R (@monoid_with_zero.to_mul_zero_class R (@semiring.to_monoid_with_zero R _inst_1)))
but is expected to have type
x ≠
@has_zero.zero R
(@mul_zero_class.to_has_zero R
(@monoid_with_zero.to_mul_zero_class R
(@cancel_monoid_with_zero.to_monoid_with_zero R
(@domain.to_cancel_monoid_with_zero R (@integral_domain.to_domain R _inst_2)))))
```

#### Reid Barton (Sep 21 2020 at 12:22):

showing that Lean already has some logic to help identify the issue,

but to make it work you have to (1) guess it's an issue with `0`

, (2) know (or guess) that `pp.numerals`

exists, (3) turn it on and understand the resulting message

#### Damiano Testa (Sep 21 2020 at 12:23):

I managed the term mode proof!

```
mul_left_cancel' h
```

I got stuck this whole time with the comma at the end...

#### Damiano Testa (Sep 21 2020 at 12:25):

Reid Barton said:

Regarding the error, if you

`set_option pp.numerals false`

, then you get an error which shows the issue:`error: invalid type ascription, term has type x ≠ @has_zero.zero R (@mul_zero_class.to_has_zero R (@monoid_with_zero.to_mul_zero_class R (@semiring.to_monoid_with_zero R _inst_1))) but is expected to have type x ≠ @has_zero.zero R (@mul_zero_class.to_has_zero R (@monoid_with_zero.to_mul_zero_class R (@cancel_monoid_with_zero.to_monoid_with_zero R (@domain.to_cancel_monoid_with_zero R (@integral_domain.to_domain R _inst_2)))))`

I see: one appears to go by `semiring`

, the other by `cancel_monoid`

.

Thanks for the explanation!

#### Johan Commelin (Sep 21 2020 at 12:26):

Nasty commas are nasty

#### Reid Barton (Sep 21 2020 at 12:26):

The main point is buried though: one is ultimately built from `_inst_1`

and the other from `_inst_2`

. So the error message could still use some work.

#### Kevin Buzzard (Sep 21 2020 at 12:35):

"Don't forget the comma!"

Last updated: May 08 2021 at 19:11 UTC