Zulip Chat Archive

Stream: new members

Topic: Apply rewrite to only one side of equality?


view this post on Zulip Paul (Feb 19 2021 at 16:22):

Can I apply a rewrite to only one side of an equality? For context, I'm doing the exercises in section 2.2 of Mathematics in Lean, and I have this proof:

lemma mul_identity_unique (a b : G) (h : a * b = a) : b = 1 :=
begin
  rw  one_mul b,
  rw  mul_left_inv a,
  rw mul_assoc,
  rw h,
end

After mul_left_inv a, the proof goal is a⁻¹ * a * b = a⁻¹ * a, but I would like it to be a⁻¹ * a * b = 1 (although I realise in this particular case, the proof is actually shorter if I let lean rewrite both sides)

view this post on Zulip Ruben Van de Velde (Feb 19 2021 at 16:27):

conv_lhs, conv_rhs, and conv are relevant: https://leanprover-community.github.io/mathlib_docs/tactics.html#conv

view this post on Zulip Paul (Feb 19 2021 at 16:29):

Ah perfect, thanks! I used conv_lhs like this and it works:

lemma mul_identity_unique (a b : G) (h : a * b = a) : b = 1 :=
begin
  rw  one_mul b,
  conv_lhs {rw  mul_left_inv a},
  rw mul_assoc,
  rw h,
  rw mul_left_inv,
end

view this post on Zulip Bryan Gin-ge Chen (Feb 19 2021 at 16:29):

Also see the nth_rewrite tactic.


Last updated: May 12 2021 at 23:13 UTC