-- Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean
theorem log_div_self_antitoneOn : AntitoneOn (fun x : ℝ => log x / x) { x | exp 1 ≤ x }

Proof state:
x : ℝ
hex : rexp 1 ≤ x
y : ℝ
hey : rexp 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ 1 ≤ log x

Tactic:
rwa [le_log_iff_exp_le x_pos]

Result:
no goals

Proof state:
x : ℝ
hex : rexp 1 ≤ x
y : ℝ
hey : rexp 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
⊢ log y / y ≤ log x / x

Tactic:
have y_pos : 0 < y := (exp_pos 1).trans_le hey

Result:
x : ℝ
hex : rexp 1 ≤ x
y : ℝ
hey : rexp 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ log y / y ≤ log x / x

Proof state:
x : ℝ
hex : rexp 1 ≤ x
y : ℝ
hey : rexp 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
⊢ 0 ≤ y / x - 1

Tactic:
rwa [le_sub_iff_add_le, le_div_iff₀ x_pos, zero_add, one_mul]

Result:
no goals

Proof state:
⊢ ∀ ⦃a : ℝ⦄, rexp 1 ≤ a → ∀ ⦃b : ℝ⦄, rexp 1 ≤ b → a ≤ b → log b / b ≤ log a / a

Tactic:
intro x hex y hey hxy

Result:
x : ℝ
hex : rexp 1 ≤ x
y : ℝ
hey : rexp 1 ≤ y
hxy : x ≤ y
⊢ log y / y ≤ log x / x

Proof state:
x : ℝ
hex : rexp 1 ≤ x
y : ℝ
hey : rexp 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
hyx : 0 ≤ y / x - 1
⊢ log x * (y / x - 1) = log x / x * y - log x

Tactic:
ring

Result:
no goals

Proof state:
⊢ AntitoneOn (fun x => log x / x) {x | rexp 1 ≤ x}

Tactic:
simp only [AntitoneOn, mem_setOf_eq]

Result:
⊢ ∀ ⦃a : ℝ⦄, rexp 1 ≤ a → ∀ ⦃b : ℝ⦄, rexp 1 ≤ b → a ≤ b → log b / b ≤ log a / a

Proof state:
x : ℝ
hex : rexp 1 ≤ x
y : ℝ
hey : rexp 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
hyx : 0 ≤ y / x - 1
⊢ log y - log x = log (y / x)

Tactic:
rw [log_div y_pos.ne' x_pos.ne']

Result:
no goals

Proof state:
x : ℝ
hex : rexp 1 ≤ x
y : ℝ
hey : rexp 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
⊢ log y / y ≤ log x / x

Tactic:
have hyx : 0 ≤ y / x - 1 := by rwa [le_sub_iff_add_le, le_div_iff₀ x_pos, zero_add, one_mul]

Result:
x : ℝ
hex : rexp 1 ≤ x
y : ℝ
hey : rexp 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
hyx : 0 ≤ y / x - 1
⊢ log y / y ≤ log x / x

Proof state:
x : ℝ
hex : rexp 1 ≤ x
y : ℝ
hey : rexp 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
hyx : 0 ≤ y / x - 1
⊢ log y / y ≤ log x / x

Tactic:
rw [div_le_iff₀ y_pos, ← sub_le_sub_iff_right (log x)]

Result:
x : ℝ
hex : rexp 1 ≤ x
y : ℝ
hey : rexp 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
hyx : 0 ≤ y / x - 1
⊢ log y - log x ≤ log x / x * y - log x

Proof state:
x : ℝ
hex : rexp 1 ≤ x
y : ℝ
hey : rexp 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
hyx : 0 ≤ y / x - 1
⊢ log y - log x ≤ log x / x * y - log x

Tactic:
calc
  log y - log x = log (y / x) := by rw [log_div y_pos.ne' x_pos.ne']
  _ ≤ y / x - 1 := log_le_sub_one_of_pos (div_pos y_pos x_pos)
  _ ≤ log x * (y / x - 1) := le_mul_of_one_le_left hyx hlogx
  _ = log x / x * y - log x := by ring

Result:
no goals

Proof state:
x : ℝ
hex : rexp 1 ≤ x
y : ℝ
hey : rexp 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ log y / y ≤ log x / x

Tactic:
have hlogx : 1 ≤ log x := by rwa [le_log_iff_exp_le x_pos]

Result:
x : ℝ
hex : rexp 1 ≤ x
y : ℝ
hey : rexp 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
⊢ log y / y ≤ log x / x

Proof state:
x : ℝ
hex : rexp 1 ≤ x
y : ℝ
hey : rexp 1 ≤ y
hxy : x ≤ y
⊢ log y / y ≤ log x / x

Tactic:
have x_pos : 0 < x := (exp_pos 1).trans_le hex

Result:
x : ℝ
hex : rexp 1 ≤ x
y : ℝ
hey : rexp 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
⊢ log y / y ≤ log x / x