Mathematics in Lean, Release 0.1 p15: example

Stream: new members

[Peter Dolland]

Can anybody help me to solve the example example (h0 : d ≤ e) : c + exp (a + d) ≤ c + exp (a + e) := by sorry?

[Ruben Van de Velde]

How would you solve it on paper?

[Gaëtan Serré]

The first thing I want to do is to get rid of $c$ using the fact that $\forall a b c \in \mathbb{R}, a \le b \implies c + a \le c + b$

[Christian K]

You might want to have a look at Nat.add_lt_add_left in the mathlib...

[Ruben Van de Velde]

Probably not with Nat and not with lt in this case

[Patrick Massot]

All required lemmas should be mentioned in the book, there is no need to guess lemmas here.

[Peter Dolland]

Can anybody help me to solve the example example (h0 : d ≤ e) : c + exp (a + d) ≤ c + exp (a + e) := by sorry?
Okay, after some variations I have a solution:

example (h0 : d ≤ e) : c + exp (a + d) ≤ c + exp (a + e) := by
    apply add_le_add_left
    apply exp_le_exp.mpr
    apply add_le_add_left h0

But I do not understand, why I have to apply exp_le_exp in reverse direction: My manual proof would be: h0 : d ≤ e ~>with add_le_add_left a + d ≤ a + e ~>with exp_le_exp exp (a + d) ≤ exp (a + e) ~>with add_le_add_left c + exp (a + d) ≤ c + exp (a + e).

[Richard Copley]

add_le_add_left might be seen as an abbreviation for add_le_add_left_of_le, and exp_le_exp for exp_le_exp_iff_le. Implication lemmas x → y are given names like "y_of_x", and bi-implication lemmas x ↔ y are given names like "x_iff_y". Mixing the two gives rise to a certain stylistic inconsistency, but I wouldn't worry about it.

Here are some more symmetrical proofs:

import Mathlib.Data.Complex.Exponential

open Real

example (h0 : d ≤ e) : c + exp (a + d) ≤ c + exp (a + e) := by
  apply (add_le_add_iff_left _).mpr
  apply exp_le_exp.mpr
  apply (add_le_add_iff_left _).mpr
  exact h0

example (h0 : d ≤ e) : c + exp (a + d) ≤ c + exp (a + e) := by
  rwa [add_le_add_iff_left, exp_le_exp, add_le_add_iff_left]

example (a c d e : ℝ) : c + exp (a + d) ≤ c + exp (a + e) ↔ d ≤ e :=
  (add_le_add_iff_left _) |>.trans exp_le_exp |>.trans (add_le_add_iff_left _)