## Stream: new members

### Topic: Problem with rewrite tactic

#### Syx Pek (May 22 2020 at 12:54):

Hello there, I am working through the proof that left identity and left inverse implies a group from
https://leanprover-community.github.io/mathematics_in_lean/

theorem mul_right_inv (a : G) : a * a⁻¹ = 1 :=
begin
have h₁ : (a⁻¹) * (a⁻¹)⁻¹ = (a⁻¹) * a, sorry,
have h₂ : (a⁻¹)⁻¹ = a, sorry,
calc a * a⁻¹
= (a⁻¹)⁻¹ * (a⁻¹)          : by rw ← h₂
... = 1                        : by rw mul_left_inv
end


But I face some difficulty. I don't see why line 6 fails.

#### Jason KY. (May 22 2020 at 12:57):

The left arrow means you want to rewrite using h₂ from a to (a⁻¹)⁻¹. Using just rw h₂ works fine!

#### Jason KY. (May 22 2020 at 12:58):

theorem mul_right_inv (a : G) : a * a⁻¹ = 1 :=
begin
have h₁ : (a⁻¹) * (a⁻¹)⁻¹ = (a⁻¹) * a, sorry,
have h₂ : (a⁻¹)⁻¹ = a, sorry,
calc a * a⁻¹
= (a⁻¹)⁻¹ * (a⁻¹)          : by rw h₂
... = 1                        : by rw mul_left_inv
end


#### Syx Pek (May 22 2020 at 13:02):

I see. But why doesn't the approach I suggested would fail. It says in the documentation, that it rewrites only the first copy of it, but it seems to rewrite all copies?

#### Bhavik Mehta (May 22 2020 at 13:05):

Out of interest where did you read that it rewrites only the first copy?

#### Jason KY. (May 22 2020 at 13:06):

In my experience it normally rewrites every instance :/

#### Bhavik Mehta (May 22 2020 at 13:06):

I think that it'll rewrite all copies of the first instance it finds, if that makes sense. That is, if you do rw add_comm and your term has a bunch of a + b and c + d, it'll change all of the a+b to b+a but none of the c+d

#### Syx Pek (May 22 2020 at 13:09):

It says "Sometimes the left-hand side of an identity can match more than one subterm in the pattern, in which case the rewrite tactic chooses the first match it finds when traversing the term. If that is not the one you want, you can use additional arguments to specify the appropriate subterm." on https://leanprover.github.io/theorem_proving_in_lean/tactics.html

#### Bhavik Mehta (May 22 2020 at 13:10):

Yeah, so seemingly it chooses the first match and applies that one as much as it can

#### Reid Barton (May 22 2020 at 13:11):

Yes, it is a confusing description of a confusing behavior

#### Scott Morrison (May 22 2020 at 14:43):

There is also nth_rewrite if you want control over this. (As well as the occs configuration argument for rw, which is even more confusingly specified.)

#### Scott Morrison (May 22 2020 at 14:43):

But usually conv to zoom into the place you're interested in is clearer and more maintainable.

Last updated: May 09 2021 at 18:17 UTC