Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Dec 24 2020 at 17:32):

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

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Dec 24 2020 at 18:29):

conv at h1

view this post on Zulip Eric Wieser (Dec 24 2020 at 18:29):

tactic#conv should cover this

view this post on Zulip Lars Ericson (Dec 24 2020 at 18:29):

Thanks!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Dec 24 2020 at 19:02):

I edited my post above to include a shorter proof.

view this post on Zulip Yakov Pechersky (Dec 24 2020 at 19:05):

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

view this post on Zulip 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]

view this post on Zulip 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]

view this post on Zulip 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