## Stream: new members

### Topic: can you limit rewrite tactic

#### Andrew Parr (Jan 31 2021 at 20:24):

Hi I've not posted before so let me first introduce myself. I'm Andrew Parr and I'm currently studying for an MSc in Mathematics at the Open University part time and I'm also trying to learn lean.

I'm been looking at the excellent formalising-mathemtics by @Kevin Buzzard but am currently stuck on proving the lemma inv_inv in tatic mode (found in week_2\Part_A_groups.lean).

After struggling for a while to prove this in tactic mode I found I could prove it in calc mode. I then tried to convert this proof to tactic mode but fail because the rewrite tactic is rewriting both of the a terms. The following extract should help to clarify what I mean.

@[simp] lemma inv_inv : a ⁻¹ ⁻¹ = a :=
begin
calc a⁻¹ ⁻¹ = 1 * a⁻¹ ⁻¹ : by rw one_mul -- after this we have a⁻¹⁻¹ = 1 * a⁻¹⁻¹
... = (a * a⁻¹) * a⁻¹ ⁻¹ : by rw mul_right_inv
... = a * (a⁻¹ * a⁻¹ ⁻¹) : by rw mul_assoc
... = a * 1 : by rw mul_right_inv
... = a : by rw mul_one,
end

-- Trying to convert the above 'calc mode' proof to 'tatic mode'
example : a ⁻¹ ⁻¹ = a :=
begin
rw ← one_mul a, -- this does both sides giving (1 * a)⁻¹ ⁻¹ = 1 * a
-- adding "at |-" to the above also doesn't help
rw ← mul_right_inv a⁻¹, -- again this does both sides
sorry,
end


Is there a way to tell the rw tactic to only work on the right hand side (or something). What I'm I missing here?

#### Patrick Massot (Jan 31 2021 at 20:25):

https://leanprover-community.github.io/extras/conv.html

#### Kevin Buzzard (Jan 31 2021 at 20:26):

Hi! You can tell the rw tactic to only work on the right hand side using the conv_rhs tactic. Try conv_rhs {rw ← one_mul a}.

#### Kevin Buzzard (Jan 31 2021 at 20:27):

You can also cheat and look at how I did it in the kb_solutions subdirectory which I uploaded after the workshop: https://github.com/ImperialCollegeLondon/formalising-mathematics/blob/master/src/week_2/kb_solutions/Part_A_groups_solutions.lean

#### Andrew Parr (Jan 31 2021 at 20:38):

Brilliant, thank you Patrick and Kevin. This is exactly what I was missing.
I did notice there were solutions for week_1, but didn't have them for week_2. I didn't think of doing another git pull.
I have them now.

Last updated: May 18 2021 at 16:25 UTC