Question about Math In Lean tutorial

Stream: lean4

[Mike]

in "S03 Using Theorems and Lemmas" there is an example:

example (h : a ≤ b) : c - exp b ≤ c - exp a := by
  sorry

The solution given is:

-- SOLUTION.
example (h : a ≤ b) : c - exp b ≤ c - exp a := by
  apply sub_le_sub_left
  exact exp_le_exp.mpr h

which uses "sub_le_sub_left", which wasn't introduced above (which is fine, the author wants users to explore mathlib4). However, I wanted to prove it with my own lemma:

lemma neg_flip_sign (h: a ≤ b) : -b ≤ -a :=
  calc
    -b = a - (a + b) := by ring
    _ = a + -(a + b) := by ring
    _ ≤ b + -(a + b) := by
      apply add_le_add_right h
    _ = -a := by ring

Is that doable? To use the lemma (along with exp_le_exp).mpr to prove that: -exp b ≤ -exp a ? and then apply that with add_le_add_left to prove

example (h : a ≤ b) : c - exp b ≤ c - exp a

?

[Kevin Buzzard]

yeah that should work I think? By the way, take a look at the #backticks link, you can edit your original post to make it easier to read.

[Mike]

Thanks Kevin! It does work.

example (h : a ≤ b) : c - exp b ≤ c - exp a := by
  have h₁ : - exp b ≤ - exp a := by
    apply neg_flip_sign
    apply exp_le_exp.mpr h
  apply add_le_add_left h₁

[Kevin Buzzard]

See if exact? proves neg_flip_sign. If it does you'll find out what the official lean name for it is.