x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : 0 < 1 / x
⊢ abs (log x * x) < 1
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
⊢ abs (log x * x) < 1
have : 0 < 1 / x := by simpa only [one_div, inv_pos] using h1
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : log (1 / x) ≤ 1 / x - 1
⊢ abs (log x * x) < 1
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : 0 < 1 / x
⊢ abs (log x * x) < 1
replace := log_le_sub_one_of_pos this
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : log (1 / x) < 1 / x
⊢ abs (log x * x) < 1
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : log (1 / x) ≤ 1 / x - 1
⊢ abs (log x * x) < 1
replace : log (1 / x) < 1 / x := by linarith
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ abs (log x * x) < 1
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : log (1 / x) < 1 / x
⊢ abs (log x * x) < 1
rw [log_div one_ne_zero h1.ne', log_one, zero_sub, lt_div_iff h1] at this
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
aux : 0 ≤ -log x * x
⊢ abs (log x * x) < 1
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ abs (log x * x) < 1
have aux : 0 ≤ -log x * x := by
  refine' mul_nonneg _ h1.le
  rw [← log_inv]
  apply log_nonneg
  rw [← le_inv h1 zero_lt_one, inv_one]
  exact h2
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : abs (log x * x) < 1
aux : 0 ≤ -log x * x
⊢ abs (log x * x) < 1
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
aux : 0 ≤ -log x * x
⊢ abs (log x * x) < 1
rw [← abs_of_nonneg aux, neg_mul, abs_neg] at this
no goals
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : abs (log x * x) < 1
aux : 0 ≤ -log x * x
⊢ abs (log x * x) < 1
exact this
no goals
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
⊢ 0 < 1 / x
simpa only [one_div, inv_pos] using h1
no goals
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : log (1 / x) ≤ 1 / x - 1
⊢ log (1 / x) < 1 / x
linarith
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ -log x
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ -log x * x
refine' mul_nonneg _ h1.le
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ log x⁻¹
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ -log x
rw [← log_inv]
case hx
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 1 ≤ x⁻¹
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ log x⁻¹
apply log_nonneg
case hx
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ x ≤ 1
case hx
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 1 ≤ x⁻¹
rw [← le_inv h1 zero_lt_one, inv_one]
no goals
case hx
x✝ y x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ x ≤ 1
exact h2