Easier ways to prove `log(5/2) <= 1`?

Stream: new members

[Walter Moreira]

For our formalization of Euclid numbers (with @Joe Stubbs) we need what it looks like an easy goal: Real.log (5 / 2) <= 1.

This is what we've been able to come out with:

import Mathlib

example : Real.log (5 / 2) ≤ 1 := by
  let u := @Real.quadratic_le_exp_of_nonneg 1 (by positivity)
  norm_num at u
  exact (Real.log_le_iff_le_exp (by positivity)).mpr u

Is there an easier way to close these type of goals that look easy from the computational point of view? In this case, it was lucky that the quadratic lower bound for the exponential gives the exact number we wanted. Are there other tactics that would avoid having to deal with the series defining the exponential?

(The thread #new members > ✔ Logarithmic Functions touches some of these questions, but I thought to ask anyway in cases someone has extra suggestions for our case.)

[Daniel Weber]

You can use docs#Real.exp_one_gt_d9,

example : Real.log (5 / 2) ≤ 1 := by
  rw [Real.log_le_iff_le_exp] <;> linarith [Real.exp_one_gt_d9]

[Walter Moreira]

Thank you! Your proof definitely looks nicer.