awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Monotone (hypothesis)
Goal:
x : ℝ
hex : x ∈ Ici (rexp 1)
y : ℝ
hey : y ∈ Ici (rexp 1)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
⊢ LE.le (α := ℝ) ((fun (x : ℝ) ↦ log x / x) y) ((fun (x : ℝ) ↦ log x / x) x)
have hyx : 0 ≤ y / x - 1
Tactic: have hyx : 0 ≤ y / x - 1 := by rwa [le_sub_iff_add_le, le_div_iff₀ x_pos, zero_add, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Monotone (goal)
Goal:
x : ℝ
hex : x ∈ Ici (rexp 1)
y : ℝ
hey : y ∈ Ici (rexp 1)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
hyx : 0 ≤ y / x - 1
⊢ LE.le (α := ℝ) ((fun (x : ℝ) ↦ log x / x) y) ((fun (x : ℝ) ↦ log x / x) x)
have rw : log y - log x ≤ (fun (x : ℝ) ↦ log x / x) x * y - log x
Tactic: rw [div_le_iff₀ y_pos, ← sub_le_sub_iff_right (log x)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Monotone (goal)
Goal:
x : ℝ
hex : x ∈ Ici (rexp 1)
y : ℝ
hey : y ∈ Ici (rexp 1)
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)
have rw : log y - log x = log y - log x
Tactic: rw [log_div y_pos.ne' x_pos.ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Monotone (goal)
Goal:
x : ℝ
hex : x ∈ Ici (rexp 1)
y : ℝ
hey : y ∈ Ici (rexp 1)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
hyx : 0 ≤ y / x - 1
⊢ log y - log x ≤ (fun (x : ℝ) ↦ log x / x) x * y - log x
have log : log y - log x = log (y / 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Monotone (goal)
Goal:
x : ℝ
hex : x ∈ Ici (rexp 1)
y : ℝ
hey : y ∈ Ici (rexp 1)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ Real.log x
hyx : 0 ≤ y / x - 1
log : Real.log y - Real.log x = Real.log (y / x)
⊢ Real.log y - Real.log x ≤ (fun (x : ℝ) ↦ Real.log x / x) x * y - Real.log x
have log₁ : Real.log x * (y / x - 1) = Real.log x / x * y - Real.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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Monotone (hypothesis)
Goal:
a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
h : y ∈ Ici (rexp a⁻¹)
hxy : x ≤ y
⊢ log y / y ^ a ≤ log x / x ^ a
have x_pos : 0 < x
Tactic: have x_pos : 0 < x := lt_of_lt_of_le (exp_pos a⁻¹) (le_of_le_of_eq hex rfl)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Monotone (goal)
Goal:
a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
h : y ∈ Ici (rexp a⁻¹)
hxy : x ≤ y
x_pos : 0 < x
⊢ 0 < y
have linarith : y ≤ 0 → x - y + (0 - x) + (y - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Monotone (hypothesis)
Goal:
a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
h : y ∈ Ici (rexp a⁻¹)
hxy : x ≤ y
x_pos : 0 < x
⊢ log y / y ^ a ≤ log x / x ^ a
have y_pos : 0 < y
Tactic: have y_pos : 0 < y := by linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Monotone (goal)
Goal:
a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
h : y ∈ Ici (rexp a⁻¹)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ log y / y ^ a ≤ log x / x ^ a
have nth_rw : log (HPow.hPow (β := ℝ) y 1) / y ^ a ≤ log (HPow.hPow (β := ℝ) x 1) / x ^ a
Tactic: nth_rw 1 [← rpow_one y, ← rpow_one x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Monotone (goal)
Goal:
a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
h : y ∈ Ici (rexp a⁻¹)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ log (HPow.hPow (β := ℝ) y 1) / y ^ a ≤ log (HPow.hPow (β := ℝ) x 1) / x ^ a
have rw : log (y ^ a) / y ^ a ≤ log (x ^ a) / x ^ a
Tactic: rw [← div_self (ne_of_lt ha).symm, div_eq_mul_one_div a a, rpow_mul y_pos.le, rpow_mul x_pos.le,
    log_rpow (rpow_pos_of_pos y_pos a), log_rpow (rpow_pos_of_pos x_pos a), mul_div_assoc,
    mul_div_assoc, mul_le_mul_iff_right₀ (one_div_pos.mpr ha)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Monotone (goal)
Goal:
a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
h : y ∈ Ici (rexp a⁻¹)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
z : ℝ
hz : z ∈ Ici (rexp a⁻¹)
⊢ rexp 1 ≤ z ^ a
have h : rexp 1 = rexp a⁻¹ ^ a
Tactic: convert! rpow_le_rpow _ hz (le_of_lt ha) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Monotone (goal)
Goal:
a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
h_1 : y ∈ Ici (rexp a⁻¹)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
z : ℝ
hz : z ∈ Ici (rexp a⁻¹)
h : rexp 1 = rexp a⁻¹ ^ a
⊢ rexp 1 ≤ z ^ a
have convert! : 0 ≤ rexp a⁻¹
Tactic: convert! rpow_le_rpow _ hz (le_of_lt ha) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Monotone (hypothesis)
Goal:
a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
h : y ∈ Ici (rexp a⁻¹)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ log (y ^ a) / y ^ a ≤ log (x ^ a) / x ^ a
have hbound : ∀ {z : ℝ} (hz : z ∈ Ici (rexp a⁻¹)), Membership.mem (γ := Set ℝ) {b : ℝ | rexp 1 ≤ b} (z ^ a)
Tactic: have hbound {z : ℝ} (hz : z ∈ Ici (rexp a⁻¹)) : z ^ a ∈ {b | rexp 1 ≤ b} := by
    rw [mem_setOf_eq]
    convert! rpow_le_rpow _ hz (le_of_lt ha) using 1
    · simp only [← exp_mul, Real.exp_eq_exp, field]
    positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Monotone (goal)
Goal:
a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
h : y ∈ Ici (rexp a⁻¹)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hbound : ∀ {z : ℝ} (hz : z ∈ Ici (rexp a⁻¹)), Membership.mem (γ := Set ℝ) {b : ℝ | rexp 1 ≤ b} (z ^ a)
⊢ log (y ^ a) / y ^ a ≤ log (x ^ a) / x ^ a
have refine : x ^ a ≤ y ^ a
Tactic: refine log_div_self_antitoneOn (hbound hex) (hbound (hex.trans hxy)) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Monotone (goal)
Goal:
a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
h : y ∈ Ici (rexp a⁻¹)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hbound : ∀ {z : ℝ} (hz : z ∈ Ici (rexp a⁻¹)), Membership.mem (γ := Set ℝ) {b : ℝ | rexp 1 ≤ b} (z ^ a)
⊢ x ^ a ≤ y ^ a
have h : 0 ≤ x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Monotone (goal)
Goal:
a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
h_1 : y ∈ Ici (rexp a⁻¹)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hbound : ∀ {z : ℝ} (hz : z ∈ Ici (rexp a⁻¹)), Membership.mem (γ := Set ℝ) {b : ℝ | rexp 1 ≤ b} (z ^ a)
h : 0 ≤ x
⊢ x ^ a ≤ y ^ a
have h₂ : 0 ≤ a
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Monotone (goal)
Goal:
⊢ AntitoneOn (β := ℝ) (fun (x : ℝ) ↦ log x / √x) (Ici (rexp 2))
have simp_rw : AntitoneOn (β := ℝ) (fun (x : ℝ) ↦ log x / x ^ (1 / 2)) (Ici (rexp 2))
Tactic: simp_rw [sqrt_eq_rpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Monotone (goal)
Goal:
⊢ AntitoneOn (β := ℝ) (fun (x : ℝ) ↦ log x / x ^ (1 / 2)) (Ici (rexp 2))
have h : 2 = (1 / 2)⁻¹
Tactic: convert! log_div_self_rpow_antitoneOn one_half_pos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
⊢ x - 1 < x * log x
have pos : ∀ (hx_pos : 0 < x), x - 1 < x * log x
Tactic: by_cases hx_pos : 0 < x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
pos : ∀ (hx_pos : 0 < x), x - 1 < x * log x
⊢ x - 1 < x * log x
have neg : ∀ (hx_pos : ¬0 < x), x - 1 < x * log x
Tactic: by_cases hx_pos : 0 < x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
hx_pos : 0 < x
⊢ x - 1 < x * log x
have nlinarith : x * log x ≤ x - 1 → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: nlinarith [Real.log_inv x, Real.log_lt_sub_one_of_pos (inv_pos.mpr hx_pos) (by aesop),
      mul_inv_cancel₀ hx_pos.ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
hx_pos : 0 < x
nlinarith : x * log x ≤ x - 1 → HMul.hMul (α := ℝ) 1 1 = 1
⊢ x - 1 < x * log x
have nlinarith₁ : x * log x ≤ x - 1 →
  x * log x - (x - 1) + (1 * x * (1 * x⁻¹) - HMul.hMul (α := ℝ) 1 1) + ((0 - x) * (1 * log x⁻¹ - -(1 * log x)) - 0) +
      (0 - (0 - x) * (1 * log x⁻¹ - (1 * x⁻¹ - HMul.hMul (α := ℝ) 1 1))) =
    0
Tactic: nlinarith [Real.log_inv x, Real.log_lt_sub_one_of_pos (inv_pos.mpr hx_pos) (by aesop),
      mul_inv_cancel₀ hx_pos.ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
hx_pos : ¬0 < x
⊢ x - 1 < x * log x
have neg : 0 < x → x - 1 < x * log x
Tactic: cases lt_or_eq_of_le h0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
hx_pos : ¬0 < x
neg : 0 < x → x - 1 < x * log x
⊢ x - 1 < x * log x
have neg₁ : 0 = x → x - 1 < x * log x
Tactic: cases lt_or_eq_of_le h0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
h0 : 0 ≤ x
⊢ x - 1 ≤ x * log x
have inl : ∀ (h0 : LE.le (α := ℝ) 0 1), HSub.hSub (α := ℝ) 1 1 ≤ 1 * log 1
Tactic: rcases eq_or_ne x 1 with rfl | h1
Cleared hypotheses: x, h0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
h0 : 0 ≤ x
inl : ∀ (h0 : LE.le (α := ℝ) 0 1), HSub.hSub (α := ℝ) 1 1 ≤ 1 * log 1
⊢ x - 1 ≤ x * log x
have inr : ∀ (h1 : x ≠ 1), x - 1 ≤ x * log x
Tactic: rcases eq_or_ne x 1 with rfl | h1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ x * log x
have rw : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x * log x) x
Tactic: rw [continuous_iff_continuousAt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x * log x) x
have inl : ∀ (hx : x ≠ 0), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x * log x) x
Tactic: obtain hx | rfl := ne_or_eq x 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
inl : ∀ (hx : x ≠ 0), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x * log x) x
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x * log x) x
have inr : ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x * log x) 0
Tactic: obtain hx | rfl := ne_or_eq x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x * log x) 0
have inr : Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * log x) (𝓝 0) (𝓝 0)
Tactic: rw [ContinuousAt, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
⊢ Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * log x) (𝓝 0) (𝓝 0)
have inr : Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝 0) (𝓝 0)
Tactic: simp_rw [mul_comm _ (log _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
⊢ Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝 0) (𝓝 0)
have inr : Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[Set.univ] 0) (𝓝 0)
Tactic: nth_rewrite 1 [← nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
⊢ Eq (α := Set ℝ) Set.univ (Set.Iio 0 ∪ Set.Ioi 0 ∪ {0})
have h : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) Set.univ x ↔ Membership.mem (γ := Set ℝ) (Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (hypothesis)
Goal:
⊢ Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[Set.univ] 0) (𝓝 0)
have this : Eq (α := Set ℝ) Set.univ (Set.Iio 0 ∪ Set.Ioi 0 ∪ {0})
Tactic: have : (Set.univ : Set ℝ) = Set.Iio 0 ∪ Set.Ioi 0 ∪ {0} := by ext; simp [em]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
this : Eq (α := Set ℝ) Set.univ (Set.Iio 0 ∪ Set.Ioi 0 ∪ {0})
⊢ Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[Set.univ] 0) (𝓝 0)
have inr : Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[<] 0 ⊔ 𝓝[>] 0 ⊔ 𝓝[{0}] 0) (𝓝 0)
Tactic: rw [this, nhdsWithin_union, nhdsWithin_union]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
this : Eq (α := Set ℝ) Set.univ (Set.Iio 0 ∪ Set.Ioi 0 ∪ {0})
⊢ Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[<] 0 ⊔ 𝓝[>] 0 ⊔ 𝓝[{0}] 0) (𝓝 0)
have inr : (Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[<] 0) (𝓝 0) ∧
    Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)) ∧
  Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (pure 0) (𝓝 0)
Tactic: simp only [nhdsWithin_singleton, Filter.tendsto_sup]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
this : Eq (α := Set ℝ) Set.univ (Set.Iio 0 ∪ Set.Ioi 0 ∪ {0})
⊢ (Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[<] 0) (𝓝 0) ∧
      Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)) ∧
    Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (pure 0) (𝓝 0)
have inr : Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)
Tactic: refine ⟨⟨tendsto_log_mul_self_nhdsLT_zero, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
this : Eq (α := Set ℝ) Set.univ (Set.Iio 0 ∪ Set.Ioi 0 ∪ {0})
inr : Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)
⊢ (Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[<] 0) (𝓝 0) ∧
      Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)) ∧
    Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (pure 0) (𝓝 0)
have inr₁ : Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (pure 0) (𝓝 0)
Tactic: refine ⟨⟨tendsto_log_mul_self_nhdsLT_zero, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
this : Eq (α := Set ℝ) Set.univ (Set.Iio 0 ∪ Set.Ioi 0 ∪ {0})
⊢ Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (pure 0) (𝓝 0)
have h : 0 = log 0 * 0
Tactic: convert! tendsto_pure_nhds (fun x ↦ log x * x) 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
hx : x ≠ 0
⊢ HasDerivAt (fun (x : ℝ) ↦ x * log x) (log x + 1) x
have rw : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x * log x) x
Tactic: rw [← deriv_mul_log hx, hasDerivAt_deriv_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
hx : x ≠ 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x * log x) x
have refine : {0}ᶜ ∈ 𝓝 x
Tactic: refine DifferentiableOn.differentiableAt differentiableOn_mul_log ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
⊢ EventuallyEq (β := ℝ) (𝓝[>] 0) (deriv fun (x : ℝ) ↦ x * log x) fun (x : ℝ) ↦ log x + 1
have h : Set.EqOn (β := ℝ) (deriv fun (x : ℝ) ↦ x * log x) (fun (x : ℝ) ↦ log x + 1) (Set.Ioi 0)
Tactic: apply eventuallyEq_nhdsWithin_of_eqOn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (hypothesis)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioi 0) x
⊢ Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ x * log x) x) ((fun (x : ℝ) ↦ log x + 1) x)
have hx₁ : 0 < x
Tactic: rw [Set.mem_Ioi] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (hypothesis)
Goal:
⊢ Tendsto (α := ℝ) (β := ℝ) (deriv fun (x : ℝ) ↦ x * log x) (𝓝[>] 0) atBot
have this : EventuallyEq (β := ℝ) (𝓝[>] 0) (deriv fun (x : ℝ) ↦ x * log x) fun (x : ℝ) ↦ log x + 1
Tactic: have : (deriv (fun x ↦ x * log x)) =ᶠ[𝓝[>] 0] (fun x ↦ log x + 1) := by
    apply eventuallyEq_nhdsWithin_of_eqOn
    intro x hx
    rw [Set.mem_Ioi] at hx
    exact deriv_mul_log hx.ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ deriv (fun (x : ℝ) ↦ x * log x) x) atTop atTop
have refine : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ deriv (fun (x : ℝ) ↦ x * log x) x) fun (x : ℝ) ↦ log x + 1
Tactic: refine (tendsto_congr' ?_).mpr (tendsto_log_atTop.atTop_add (tendsto_const_nhds (x := 1)))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ deriv (fun (x : ℝ) ↦ x * log x) x) fun (x : ℝ) ↦ log x + 1
have rw : ∃ (a : ℝ), ∀ b ≥ a, deriv (fun (x : ℝ) ↦ x * log x) b = log b + 1
Tactic: rw [EventuallyEq, eventually_atTop]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ derivWithin (fun (x : ℝ) ↦ x * log x) (Set.Ioi x) x) atTop atTop
have refine : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ derivWithin (fun (x : ℝ) ↦ x * log x) (Set.Ioi x) x) fun (x : ℝ) ↦ log x + 1
Tactic: refine (tendsto_congr' ?_).mpr (tendsto_log_atTop.atTop_add (tendsto_const_nhds (x := 1)))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ derivWithin (fun (x : ℝ) ↦ x * log x) (Set.Ioi x) x) fun (x : ℝ) ↦
    log x + 1
have rw : ∃ (a : ℝ), ∀ b ≥ a, derivWithin (fun (x : ℝ) ↦ x * log x) (Set.Ioi b) b = log b + 1
Tactic: rw [EventuallyEq, eventually_atTop]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
⊢ deriv (deriv fun (x : ℝ) ↦ x * log x) x = x⁻¹
have pos : ∀ (hx : x = 0), deriv (deriv fun (x : ℝ) ↦ x * log x) x = x⁻¹
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
pos : ∀ (hx : x = 0), deriv (deriv fun (x : ℝ) ↦ x * log x) x = x⁻¹
⊢ deriv (deriv fun (x : ℝ) ↦ x * log x) x = x⁻¹
have neg : ∀ (hx : ¬x = 0), deriv (deriv fun (x : ℝ) ↦ x * log x) x = x⁻¹
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
hx : x = 0
⊢ deriv (deriv fun (x : ℝ) ↦ x * log x) x = x⁻¹
have pos : Eq (α := ℝ) (deriv (𝕜 := ℝ) (deriv fun (x : ℝ) ↦ x * log x) 0) 0
Tactic: rw [hx, inv_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
hx : ¬x = 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, deriv (fun (x : ℝ) ↦ x * log x) y = log y + 1
⊢ deriv (deriv fun (x : ℝ) ↦ x * log x) x = x⁻¹
have refine : deriv (fun (x : ℝ) ↦ log x + 1) x = x⁻¹
Tactic: refine (Filter.EventuallyEq.deriv_eq this).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
hx : ¬x = 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, deriv (fun (x : ℝ) ↦ x * log x) y = log y + 1
⊢ deriv (fun (x : ℝ) ↦ log x + 1) x = x⁻¹
have rw : deriv log x = x⁻¹
Tactic: rw [deriv_add_const, deriv_log x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
hx : ¬x = 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, deriv (fun (x : ℝ) ↦ x * log x) y = log y + 1
rw : deriv log x = x⁻¹
⊢ deriv (fun (x : ℝ) ↦ log x + 1) x = x⁻¹
have rw₁ : x⁻¹ = x⁻¹
Tactic: rw [deriv_add_const, deriv_log x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
hx : ¬x = 0
⊢ deriv (deriv fun (x : ℝ) ↦ x * log x) x = x⁻¹
have neg : ∀ᶠ (y : ℝ) in 𝓝 x, deriv (fun (x : ℝ) ↦ x * log x) y = log y + 1
Tactic: suffices ∀ᶠ y in (𝓝 x), deriv (fun x ↦ x * log x) y = log y + 1 by
      refine (Filter.EventuallyEq.deriv_eq this).trans ?_
      rw [deriv_add_const, deriv_log x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
hx : ¬x = 0
⊢ ∀ᶠ (y : ℝ) in 𝓝 x, deriv (fun (x : ℝ) ↦ x * log x) y = log y + 1
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ≠ 0) x} x →
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (y : ℝ) ↦ deriv (fun (x : ℝ) ↦ x * log x) y = log y + 1) x} x}
    a
Tactic: filter_upwards [eventually_ne_nhds hx] with y hy using deriv_mul_log hy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
hx : ¬x = 0
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ≠ 0) x} x →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (y : ℝ) ↦ deriv (fun (x : ℝ) ↦ x * log x) y = log y + 1) x} x}
      a
⊢ ∀ᶠ (y : ℝ) in 𝓝 x, deriv (fun (x : ℝ) ↦ x * log x) y = log y + 1
have h₁ : ∀ (a : ℝ), a ≠ 0 → deriv (fun (x : ℝ) ↦ x * log x) a = log a + 1
Tactic: filter_upwards [eventually_ne_nhds hx] with y hy using deriv_mul_log hy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
⊢ StrictConvexOn ℝ (β := ℝ) (Set.Ici 0) fun (x : ℝ) ↦ x * log x
have refine : ∀ (x : ℝ),
  Membership.mem (γ := Set ℝ) (interior (Set.Ici 0)) x →
    LT.lt (α := ℝ) (0 : ℝ) (deriv^[2] (fun (x : ℝ) ↦ x * log x) x : ℝ)
Tactic: refine strictConvexOn_of_deriv2_pos (convex_Ici 0) (continuous_mul_log.continuousOn) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (hypothesis)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (interior (Set.Ici 0)) x
⊢ LT.lt (α := ℝ) (0 : ℝ) (deriv^[2] (fun (x : ℝ) ↦ x * log x) x : ℝ)
have hx₁ : 0 < x
Tactic: simp only [Set.nonempty_Iio, interior_Ici', Set.mem_Ioi] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
hx : 0 < x
⊢ LT.lt (α := ℝ) (0 : ℝ) (deriv^[2] (fun (x : ℝ) ↦ x * log x) x : ℝ)
have rw : 0 < x⁻¹
Tactic: rw [deriv2_mul_log]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x y : ℝ
⊢ (x * y).negMulLog = y * x.negMulLog + x * y.negMulLog
have simp : -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)
Tactic: simp only [negMulLog, neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x y : ℝ
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)
have pos : ∀ (hx : x = 0), -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x y : ℝ
pos : ∀ (hx : x = 0), -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)
have neg : ∀ (hx : ¬x = 0), -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x y : ℝ
hx : ¬x = 0
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)
have pos : ∀ (hy : y = 0), -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x y : ℝ
hx : ¬x = 0
pos : ∀ (hy : y = 0), -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)
have neg : ∀ (hy : ¬y = 0), -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x y : ℝ
hx : ¬x = 0
hy : ¬y = 0
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)
have neg : -(x * y * (log x + log y)) = y * -(x * log x) + x * -(y * log y)
Tactic: rw [log_mul hx hy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
⊢ DifferentiableAt ℝ negMulLog x ↔ x ≠ 0
have mp : DifferentiableAt ℝ negMulLog x → x ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (goal)
Goal:
x : ℝ
mp : DifferentiableAt ℝ negMulLog x → x ≠ 0
⊢ DifferentiableAt ℝ negMulLog x ↔ x ≠ 0
have mpr : x ≠ 0 → DifferentiableAt ℝ negMulLog x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (hypothesis)
Goal:
x : ℝ
h : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ -x * log x) x
eq0 : x = 0
⊢ False
have h₁ : DifferentiableAt ℝ (F := ℝ) (fun (y : ℝ) ↦ y * log y) 0
Tactic: simp only [neg_mul, differentiableAt_fun_neg_iff, eq0] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (hypothesis)
Goal:
x : ℝ
hx : x ≠ 0
⊢ DifferentiableAt ℝ negMulLog x
have this : Membership.mem (γ := Set ℝ) {0}ᶜ x
Tactic: have : x ∈ ({0} : Set ℝ)ᶜ := by
      simp_all only [ne_eq, Set.mem_compl_iff, Set.mem_singleton_iff, not_false_eq_true]