Problem with rewrite tactic

Stream: new members

[Syx Pek]

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.]

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

[Jason KY.]

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]

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]

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

[Jason KY.]

In my experience it normally rewrites every instance :/

[Bhavik Mehta]

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]

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]

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

[Reid Barton]

Yes, it is a confusing description of a confusing behavior

[Scott Morrison]

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]

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