## Stream: new members

### Topic: choosing where we rewrite

#### Antoine Labelle (Nov 25 2020 at 22:47):

import data.real.basic

variables a b : ℝ

example : abs a - abs b ≤ abs (a - b) :=
begin
apply (sub_le_sub_iff_right (abs b)).mpr,

end


The rw ← sub_add_cancel a b add a -b+b everywhere there is an a, but I just want to do the rewrite in the abs a on the left hand side. Is the a way to specify this?

#### Adam Topaz (Nov 25 2020 at 22:49):

Take a look at tactic#nth_rewrite

#### Adam Topaz (Nov 25 2020 at 22:49):

import data.real.basic

variables a b : ℝ

example : abs a - abs b ≤ abs (a - b) :=
begin
apply (sub_le_sub_iff_right (abs b)).mpr,
end


#### Antoine Labelle (Nov 25 2020 at 22:54):

Hum I get an unknown identifier 'nth_rewrite' error if I do the same. Do I need to import something?

#### Adam Topaz (Nov 25 2020 at 22:55):

Not sure why... I just copied and pasted the whole contents of the file.

#### Adam Topaz (Nov 25 2020 at 22:55):

Which compiles fine.

#### Adam Topaz (Nov 25 2020 at 23:01):

It should work... your installation might be broken in some way.

#### Adam Topaz (Nov 25 2020 at 23:01):

I just tried that code with a fresh project with the most current mathlib, and it works just fine.

Weird...

#### Floris van Doorn (Nov 25 2020 at 23:26):

Another way to do things like this is conv_lhs { rw ← sub_add_cancel a b }. See https://leanprover-community.github.io/extras/conv.html for more information about conv-mode.

#### Kevin Buzzard (Nov 25 2020 at 23:33):

Yet another way is to work backwards rather than forwards. You're presumably trying to turn your goal into something where you can finish with abs_add (a - b) b. Why not just tell Lean that's how you want to finish with convert and then pick up the pieces afterwards?

import data.real.basic

variables a b : ℝ

example : abs a - abs b ≤ abs (a - b) :=
begin
apply (sub_le_sub_iff_right (abs b)).mpr,
-- ⊢ abs a ≤ abs (a - b) + abs b
convert abs_add (a - b) b,
-- ⊢ a = a - b + b
simp,
end


But I would be more worried that you can't get a proof compiling which works for everyone else. Did you follow the instructions on the community website?

#### Kevin Buzzard (Nov 25 2020 at 23:35):

If you're working in a Lean project (which you should be) then you can perhaps use something like leanproject upgrade-mathlib to upload the copy of mathlib for that project.

#### Antoine Labelle (Nov 26 2020 at 02:01):

Thanks for the tips, I didn't know about conv_lhs and convert. Also leanproject upgrade-mathlib worked, thanks!

Last updated: May 14 2021 at 13:24 UTC