Beginner question about cases and existential hypotheses

Stream: new members

[Ryan Smith]

I am learning lean still and working on one of the basic examples in the Mathematics in Lean repo: C02_Basics/S03_Using_Theorems_and_Lemmas.lean, specifically

example (h₀ : d ≤ e) : c + exp (a + d) ≤ c + exp (a + e) := by
  apply add_le_add_left
  rw [exp_le_exp]
  sorry

At this point in my proof I have
h₀ : d ≤ e
⊢ a + d ≤ a + e

Seems pretty straightforward, so far so good. Ideally we would apply a theorem to add the variable a to both sides of my hypothesis but since I don't seem to have such a theorem at this point I figured I could use cases on h\0 to transform the existential quantified from \le to something like e = d + x for some x I introduce. I am probably misunderstanding something basic since lean complains when I try cases h\0 that

tactic 'cases' failed, major premise type is not an inductive type
  Real.le✝ d e

Climbing the learning curve on lean is certainly interesting :)

[Aaron Liu]

The problem is that d ≤ e is not defined as an exists

[Ryan Smith]

Is that a difference from the natural number game for introducing lean for the first time then?

[Aaron Liu]

Yes

[Aaron Liu]

I think linarith will solve this one

[Ryan Smith]

Thank you, and so it does.

[Kevin Buzzard]

You can't define d<=e to mean "exists c such that d+c=e" for reals, because negative reals exist :-) (in contrast to negative naturals, which don't exist).