## 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

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