1 ≤ Real.log 3

Stream: Is there code for X?

[Michael Stoll]

How do I prove the statement in the title without much fuss?

[Yaël Dillies]

Something like

calc
  1 = log (exp 1) := by rw [log_exp]
  _ ≤ log 3 := Real.log_le_log (by positivity) $ Real.exp_one_lt_d9.le.trans $ by norm_num

[Yaël Dillies]

(untested)

[Michael Stoll]

There was an (...).le missing, but otherwise it works.

[Yaël Dillies]

Edited

[Yury G. Kudryashov]

Should we have Real.exp_one_lt_three?