How to reverse an inequality

Stream: new members

[Nowhere Dense]

Hey, I am learning lean following the book The mechanics of proof in the documentation and I have a very basic question. I got stuck in this exercise bellow, which tactic can I use to get h3 from h1? Thanks!

example {r s : ℚ} (h1 : s + 3 ≥ r) (h2 : s + r ≤ 3) : r ≤ 3 := by
  have h3 : r ≤ 3 + s := by sorry -- justify with one tactic
  have h4 : r ≤ 3 - s := by sorry -- justify with one tactic
  calc
    r = (r + r) / 2 := by sorry -- justify with one tactic
    _ ≤ (3 - s + (3 + s)) / 2 := by sorry -- justify with one tactic
    _ = 3 := by sorry -- justify with one tactic

[Etienne Marion]

by rwa [add_comm] works. It says to rewrite 3 + s as s + 3 and then the "a" in rwa means assumption, so the tactic will try to match the goal with a hypothesis after rewriting. As r ≤ 3 + s is the same as 3 + s ≥ r it works.

[Julian Berman]

Flipping through https://hrmacbeth.github.io/math2001/02_Proofs_with_Structure.html and the prior chapter I don't see it teaching rwa even though that's what occurred to me too.

[Julian Berman]

I'm pretty sure it's intending linarith [h1], which in MoP is spelled addarith [h1].

[Nowhere Dense]

Thank you all!
I checked that addarith works, and it is good to know that linarith is the same as addarith.
rwa [add_comm] also works, and it is a good technique to keep in mind. Is there any good place to search for known lemmas like add_comm?

[Etienne Marion]

Quoting Yaël: "There are #docs, #loogle, #leansearch/ #moogle in increasing order of fanciness"