Is x^(1/x) \leq e^(1/e) in Mathlib?

Stream: Is there code for X?

[Terence Tao]

Is the inequality

example {x:ℝ} (h: x > 0) : x^(x⁻¹) ≤ Real.exp Real.exp (Real.exp 1)⁻¹

already in Mathlib? An equivalent form is

example {x:ℝ} (h: x > 0) : (Real.exp 1) * Real.log x ≤ x

It's not too hard to prove (e.g., from the mean value theorem applied to Real.log at Real.exp 1 and x), but I wonder if it (or something close to it) already in Mathlib.

EDIT: Okay, I can get it from applying Real.log_le_sub_one_of_pos to x / Real.exp 1 in a few lines. I guess that's good enough for me.