## Stream: new members

### Topic: Apply rewrite to only one side of equality?

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

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

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


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