# Zulip Chat Archive

## Stream: new members

### Topic: How do I apply rw to the RHS of an equality

#### Lars Ericson (Dec 24 2020 at 17:31):

Is there way to apply `rw`

to the right hand side of an equation only? This doesn't work (unknown `h1.right`

):

```
rw ← (mul_one x) at h1.right,
```

where

```
h1 : x * x = x
```

I want to get `x*x =x*1`

.

#### Bryan Gin-ge Chen (Dec 24 2020 at 17:32):

You can use `conv_rhs`

. See https://leanprover-community.github.io/extras/conv.html

#### Lars Ericson (Dec 24 2020 at 18:28):

Actually I don't know how to make `conv`

work on a hypothesis. The article shows how to operate only on the goal state. I am in this situation:

```
import algebra.ring.basic
import tactic
universe u
variables {β : Type u} [integral_domain β]
variable x : β
#check mul_one x
lemma ex2c : ∀ (x : β), x*x = x → (x = 0 ∨ x = 1) :=
begin
intro x,
intro h1,
conv
begin
end
end
```

The tactic state after the `conv begin`

is

```
1 goal
β : Type u,
_inst_1 : integral_domain β,
x : β,
h1 : x * x = x
| x = 0 ∨ x = 1
```

I want to apply `mul_one`

to the right hand side of `h1`

to get `x*x =x*1`

. `conv`

mode only lets me operate on `| x = 0 ∨ x = 1`

.

#### Eric Wieser (Dec 24 2020 at 18:29):

`conv at h1`

#### Eric Wieser (Dec 24 2020 at 18:29):

tactic#conv should cover this

#### Lars Ericson (Dec 24 2020 at 18:29):

Thanks!

#### Eric Wieser (Dec 24 2020 at 18:30):

As should the hover text for `conv`

in vs-code, unless it's one of those tactics where the help formatter crashes.

#### Bryan Gin-ge Chen (Dec 24 2020 at 18:32):

```
import algebra.ring.basic
import tactic
universe u
variables {β : Type u} [integral_domain β]
variable x : β
#check mul_one x
lemma ex2c (h1 : x * x = x) : x = 0 ∨ x = 1 :=
begin
conv_rhs at h1 { rw ← mul_one x, },
rwa [← sub_eq_zero, ←mul_sub, mul_eq_zero, sub_eq_zero] at h1,
end
```

#### Lars Ericson (Dec 24 2020 at 19:00):

DONE. This was hard for me. There's probably a 2-liner for this in Lean. I'm just happy it works:

```
import algebra.ring.basic
import tactic
universe u
variables {β : Type u} [integral_domain β]
lemma integral_domain.only_idempotents_are_0_and_1 : ∀ (x : β), x*x = x → (x = 0 ∨ x = 1) :=
begin
intro x,
intro h1,
conv_rhs at h1 { rw ← mul_one x, },
have h2 := sub_eq_zero.mpr h1,
rw (mul_sub x x 1).symm at h2,
have h3 := mul_eq_zero.mp h2,
by_cases h4 : x = 0,
by_cases h5 : x-1 = 0,
exact or.inl h4,
exact or.inl h4,
refine or.inr _,
exact (mul_right_inj' h4).mp h1,
end
```

#### Bryan Gin-ge Chen (Dec 24 2020 at 19:02):

I edited my post above to include a shorter proof.

#### Yakov Pechersky (Dec 24 2020 at 19:05):

Note, this is true for a `domain`

, the commutitivity is not used here.

#### Johan Commelin (Dec 24 2020 at 19:22):

Compressed version of Bryan's solution

```
lemma ex2c (h1 : x * x = x) : x = 0 ∨ x = 1 :=
by rw [← @sub_eq_zero β _ _ 1, ← mul_eq_zero, mul_sub, h1, mul_one, sub_self]
```

#### Johan Commelin (Dec 24 2020 at 19:24):

simp ftw:

```
lemma ex2c (h1 : x * x = x) : x = 0 ∨ x = 1 :=
by simp [← @sub_eq_zero β _ _ 1, ← mul_eq_zero, mul_sub, h1]
```

#### Kenny Lau (Dec 24 2020 at 19:28):

term mode:

```
lemma ex2c {x : β} (h1 : x * x = x) : x = 0 ∨ x = 1 :=
or_iff_not_imp_left.2 $ λ hx, mul_left_cancel' hx $ h1.trans (mul_one x).symm
```

Last updated: May 12 2021 at 04:19 UTC