Apply rewrite to only one side of equality?

Stream: new members

[Paul]

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]

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

[Paul]

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]

Also see the nth_rewrite tactic.