How do I apply rw to the RHS of an equality

Stream: new members

[Lars Ericson]

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]

You can use conv_rhs. See https://leanprover-community.github.io/extras/conv.html

[Lars Ericson]

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]

conv at h1

[Eric Wieser]

tactic#conv should cover this

[Lars Ericson]

Thanks!

[Eric Wieser]

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]

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]

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]

I edited my post above to include a shorter proof.

[Yakov Pechersky]

Note, this is true for a domain, the commutitivity is not used here.

[Johan Commelin]

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]

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]

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