awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
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
rw : log (y ^ a) / y ^ a ≤ log (x ^ a) / x ^ a
⊢ log (HPow.hPow (β := ℝ) y 1) / y ^ a ≤ log (HPow.hPow (β := ℝ) x 1) / 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)]

Premises used: Iff.mpr, Real.rpow_pos_of_pos, Real.log_rpow, mul_div_assoc, LT.lt.le, Ne.symm, div_eq_mul_one_div, one_div_pos, Real.rpow_mul, ne_of_lt, div_self, mul_le_mul_iff_right₀
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
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 a⁻¹ ^ a ≤ z ^ a

Tactic:
rpow_le_rpow _ hz (le_of_lt ha)

Premises used: le_of_lt, Real.rpow_le_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
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
convert! : 0 ≤ rexp a⁻¹
⊢ rexp 1 ≤ z ^ a

Tactic:
convert! rpow_le_rpow _ hz (le_of_lt ha) using 1

Premises used: le_of_lt, Real.rpow_le_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
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 = rexp a⁻¹ ^ a

Tactic:
simp only [← exp_mul, Real.exp_eq_exp, field]

Premises used: Real.exp_mul, Real.exp_eq_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
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⁻¹)
⊢ 0 ≤ rexp a⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
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⁻¹)), 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
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
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

Tactic:
log_div_self_antitoneOn (hbound hex) (hbound (hex.trans hxy)) ?_

Premises used: Real.log_div_self_antitoneOn, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
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)
refine : x ^ a ≤ y ^ a
⊢ log (y ^ a) / y ^ a ≤ log (x ^ a) / x ^ a

Tactic:
refine log_div_self_antitoneOn (hbound hex) (hbound (hex.trans hxy)) ?_

Premises used: Real.log_div_self_antitoneOn, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
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
h₂ : 0 ≤ a
⊢ x ^ a ≤ y ^ a

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
Goal:
simp_rw : AntitoneOn (β := ℝ) (fun (x : ℝ) ↦ log x / x ^ (1 / 2)) (Ici (rexp 2))
⊢ AntitoneOn (β := ℝ) (fun (x : ℝ) ↦ log x / √x) (Ici (rexp 2))

Tactic:
simp_rw [sqrt_eq_rpow]

Premises used: Real.sqrt_eq_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
Goal:
⊢ AntitoneOn (β := ℝ) (fun (x : ℝ) ↦ log x / x ^ (1 / 2)) (Ici (rexp (1 / 2)⁻¹))

Tactic:
log_div_self_rpow_antitoneOn one_half_pos

Premises used: one_half_pos, Real.log_div_self_rpow_antitoneOn
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
Goal:
h : 2 = (1 / 2)⁻¹
⊢ AntitoneOn (β := ℝ) (fun (x : ℝ) ↦ log x / x ^ (1 / 2)) (Ici (rexp 2))

Tactic:
convert! log_div_self_rpow_antitoneOn one_half_pos

Premises used: one_half_pos, Real.log_div_self_rpow_antitoneOn
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
Goal:
⊢ 2 = (1 / 2)⁻¹

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
pos : ∀ (hx_pos : 0 < x), x - 1 < x * log x
neg : ∀ (hx_pos : ¬0 < x), x - 1 < x * log x
⊢ x - 1 < x * log x

Tactic:
by_cases hx_pos : 0 < x
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
hx_pos : 0 < x
⊢ x⁻¹ ≠ 1

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
hx_pos : 0 < x
nlinarith : x * log x ≤ x - 1 → HMul.hMul (α := ℝ) 1 1 = 1
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
⊢ x - 1 < x * log x

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']

Premises used: Iff.mpr, mul_inv_cancel₀, inv_pos, Real.log_lt_sub_one_of_pos, LT.lt.ne', Real.log_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
hx_pos : ¬0 < x
neg : 0 < x → x - 1 < x * log x
neg₁ : 0 = x → x - 1 < x * log x
⊢ x - 1 < x * log x

Tactic:
cases lt_or_eq_of_le h0

Premises used: lt_or_eq_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
hx_pos : ¬0 < x
h : 0 < x
⊢ x - 1 < x * log x

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
hx_pos : ¬0 < x
h : 0 = x
⊢ x - 1 < x * log x

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
h0 : 0 ≤ x
inl : ∀ (h0 : LE.le (α := ℝ) 0 1), HSub.hSub (α := ℝ) 1 1 ≤ 1 * log 1
inr : ∀ (h1 : x ≠ 1), x - 1 ≤ x * log x
⊢ x - 1 ≤ x * log x

Tactic:
rcases eq_or_ne x 1 with rfl | h1

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
h0 : LE.le (α := ℝ) 0 1
⊢ HSub.hSub (α := ℝ) 1 1 ≤ 1 * log 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
⊢ x - 1 ≤ x * log x

Tactic:
le_of_lt (self_sub_one_lt_mul_log h0 h1)

Premises used: le_of_lt, Real.self_sub_one_lt_mul_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
⊢ x - 1 ≤ x * log x

Tactic:
exact le_of_lt (self_sub_one_lt_mul_log h0 h1)

Premises used: le_of_lt, Real.self_sub_one_lt_mul_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
rw : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x * log x) x
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ x * log x

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
inl : ∀ (hx : x ≠ 0), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x * log x) x
inr : ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x * log x) 0
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x * log x) x

Tactic:
obtain hx | rfl := ne_or_eq x 0

Premises used: ne_or_eq, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : x ≠ 0
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x * log x) x

Tactic:
(continuous_id'.continuousAt).mul (continuousAt_log hx)

Premises used: continuous_id', Continuous.continuousAt, ContinuousAt.mul, Real.continuousAt_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : x ≠ 0
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x * log x) x

Tactic:
exact (continuous_id'.continuousAt).mul (continuousAt_log hx)

Premises used: continuous_id', Continuous.continuousAt, ContinuousAt.mul, Real.continuousAt_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
inr : Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * log x) (𝓝 0) (𝓝 0)
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x * log x) 0

Tactic:
rw [ContinuousAt, zero_mul]

Premises used: ContinuousAt, MulZeroClass.zero_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
inr : Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝 0) (𝓝 0)
⊢ Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * log x) (𝓝 0) (𝓝 0)

Tactic:
simp_rw [mul_comm _ (log _)]

Premises used: Real.log, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
inr : Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[Set.univ] 0) (𝓝 0)
⊢ Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝 0) (𝓝 0)

Tactic:
nth_rewrite 1 [← nhdsWithin_univ]

Premises used: nhdsWithin_univ
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
h : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) Set.univ x ↔ Membership.mem (γ := Set ℝ) (Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}) x
⊢ Eq (α := Set ℝ) Set.univ (Set.Iio 0 ∪ Set.Ioi 0 ∪ {0})

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
⊢ Membership.mem (γ := Set ℝ) Set.univ x ↔ Membership.mem (γ := Set ℝ) (Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}) x

Tactic:
simp [em]

Premises used: em
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
⊢ 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]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
this : Eq (α := Set ℝ) Set.univ (Set.Iio 0 ∪ Set.Ioi 0 ∪ {0})
inr : Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[<] 0 ⊔ 𝓝[>] 0 ⊔ 𝓝[{0}] 0) (𝓝 0)
⊢ Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[Set.univ] 0) (𝓝 0)

Tactic:
rw [this, nhdsWithin_union, nhdsWithin_union]

Premises used: nhdsWithin_union
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
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) (pure 0) (𝓝 0)
⊢ Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[<] 0 ⊔ 𝓝[>] 0 ⊔ 𝓝[{0}] 0) (𝓝 0)

Tactic:
simp only [nhdsWithin_singleton, Filter.tendsto_sup]

Premises used: nhdsWithin_singleton, Filter.tendsto_sup
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
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)

Tactic:
⟨⟨tendsto_log_mul_self_nhdsLT_zero, ?_⟩, ?_⟩

Premises used: And.intro, tendsto_log_mul_self_nhdsLT_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
this : Eq (α := Set ℝ) Set.univ (Set.Iio 0 ∪ Set.Ioi 0 ∪ {0})
inr : Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)
inr₁ : Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (pure 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)

Tactic:
refine ⟨⟨tendsto_log_mul_self_nhdsLT_zero, ?_⟩, ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
this : Eq (α := Set ℝ) Set.univ (Set.Iio 0 ∪ Set.Ioi 0 ∪ {0})
⊢ Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)

Tactic:
simpa only [rpow_one] using tendsto_log_mul_rpow_nhdsGT_zero zero_lt_one

Premises used: Real.rpow_one, zero_lt_one, tendsto_log_mul_rpow_nhdsGT_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
this : Eq (α := Set ℝ) Set.univ (Set.Iio 0 ∪ Set.Ioi 0 ∪ {0})
⊢ Filter.Tendsto (fun (x : ℝ) ↦ log x * x) (pure 0) (𝓝 (log 0 * 0))

Tactic:
tendsto_pure_nhds (fun x ↦ log x * x) 0

Premises used: HMul.hMul, Real.log, tendsto_pure_nhds, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
this : Eq (α := Set ℝ) Set.univ (Set.Iio 0 ∪ Set.Ioi 0 ∪ {0})
h : 0 = log 0 * 0
⊢ Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (pure 0) (𝓝 0)

Tactic:
convert! tendsto_pure_nhds (fun x ↦ log x * x) 0

Premises used: HMul.hMul, Real.log, tendsto_pure_nhds, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
this : Eq (α := Set ℝ) Set.univ (Set.Iio 0 ∪ Set.Ioi 0 ∪ {0})
⊢ 0 = log 0 * 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℝ
hf : Continuous[inst, _] f
⊢ Continuous[inst, _] fun (a : α) ↦ f a * log (f a)

Tactic:
continuous_mul_log.comp hf

Premises used: Real.continuous_mul_log, Continuous.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
⊢ DifferentiableOn ℝ (F := ℝ) (fun (x : ℝ) ↦ x * log x) {0}ᶜ

Tactic:
differentiable_id.differentiableOn.mul differentiableOn_log

Premises used: Real.differentiableOn_log, DifferentiableOn.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : x ≠ 0
⊢ deriv (fun (x : ℝ) ↦ x * log x) x = log x + 1

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : x ≠ 0
rw : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x * log x) x
⊢ HasDerivAt (fun (x : ℝ) ↦ x * log x) (log x + 1) x

Tactic:
rw [← deriv_mul_log hx, hasDerivAt_deriv_iff]

Premises used: hasDerivAt_deriv_iff, Real.deriv_mul_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : x ≠ 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x * log x) x

Tactic:
DifferentiableOn.differentiableAt differentiableOn_mul_log ?_

Premises used: DifferentiableOn.differentiableAt, Real.differentiableOn_mul_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : x ≠ 0
refine : {0}ᶜ ∈ 𝓝 x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x * log x) x

Tactic:
refine DifferentiableOn.differentiableAt differentiableOn_mul_log ?_

Premises used: DifferentiableOn.differentiableAt, Real.differentiableOn_mul_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : x ≠ 0
⊢ {0}ᶜ ∈ 𝓝 x

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : x ≠ 0
⊢ derivWithin (fun (x : ℝ) ↦ x * log x) (Set.Ioi x) x = log x + 1

Tactic:
(hasDerivAt_mul_log hx).hasDerivWithinAt.derivWithin (uniqueDiffWithinAt_Ioi x)

Premises used: HasDerivAt.hasDerivWithinAt, Real.hasDerivAt_mul_log, HasDerivWithinAt.derivWithin, uniqueDiffWithinAt_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : x ≠ 0
⊢ derivWithin (fun (x : ℝ) ↦ x * log x) (Set.Iio x) x = log x + 1

Tactic:
(hasDerivAt_mul_log hx).hasDerivWithinAt.derivWithin (uniqueDiffWithinAt_Iio x)

Premises used: HasDerivAt.hasDerivWithinAt, Real.hasDerivAt_mul_log, HasDerivWithinAt.derivWithin, uniqueDiffWithinAt_Iio
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
h : Set.EqOn (β := ℝ) (deriv fun (x : ℝ) ↦ x * log x) (fun (x : ℝ) ↦ log x + 1) (Set.Ioi 0)
⊢ EventuallyEq (β := ℝ) (𝓝[>] 0) (deriv fun (x : ℝ) ↦ x * log x) fun (x : ℝ) ↦ log x + 1

Tactic:
apply eventuallyEq_nhdsWithin_of_eqOn

Premises used: eventuallyEq_nhdsWithin_of_eqOn
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioi 0) x
⊢ 0 < x

Tactic:
rw [Set.mem_Ioi] at hx

Premises used: Set.mem_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : 0 < x
⊢ Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ x * log x) x) ((fun (x : ℝ) ↦ log x + 1) x)

Tactic:
deriv_mul_log hx.ne'

Premises used: LT.lt.ne', Real.deriv_mul_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : 0 < x
⊢ Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ x * log x) x) ((fun (x : ℝ) ↦ log x + 1) x)

Tactic:
exact deriv_mul_log hx.ne'

Premises used: LT.lt.ne', Real.deriv_mul_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
⊢ 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'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
this : EventuallyEq (β := ℝ) (𝓝[>] 0) (deriv fun (x : ℝ) ↦ x * log x) fun (x : ℝ) ↦ log x + 1
⊢ Tendsto (α := ℝ) (β := ℝ) (deriv fun (x : ℝ) ↦ x * log x) (𝓝[>] 0) atBot

Tactic:
simp only [tendsto_congr' this, tendsto_atBot_add_const_right, tendsto_log_nhdsGT_zero]

Premises used: Real.tendsto_log_nhdsGT_zero, Filter.tendsto_atBot_add_const_right, Filter.tendsto_congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ deriv (fun (x : ℝ) ↦ x * log x) x) atTop atTop

Tactic:
(tendsto_congr' ?_).mpr (tendsto_log_atTop.atTop_add (tendsto_const_nhds (x := 1)))

Premises used: Iff.mpr, tendsto_const_nhds, Filter.Tendsto.atTop_add, Real.tendsto_log_atTop, Filter.tendsto_congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
refine : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ deriv (fun (x : ℝ) ↦ x * log x) x) fun (x : ℝ) ↦ log x + 1
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ deriv (fun (x : ℝ) ↦ x * log x) x) atTop atTop

Tactic:
refine (tendsto_congr' ?_).mpr (tendsto_log_atTop.atTop_add (tendsto_const_nhds (x := 1)))

Premises used: Iff.mpr, tendsto_const_nhds, Filter.Tendsto.atTop_add, Real.tendsto_log_atTop, Filter.tendsto_congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
rw : ∃ (a : ℝ), ∀ b ≥ a, deriv (fun (x : ℝ) ↦ x * log x) b = log b + 1
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ deriv (fun (x : ℝ) ↦ x * log x) x) fun (x : ℝ) ↦ log x + 1

Tactic:
rw [EventuallyEq, eventually_atTop]

Premises used: Filter.EventuallyEq, Filter.eventually_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
⊢ ∃ (a : ℝ), ∀ b ≥ a, deriv (fun (x : ℝ) ↦ x * log x) b = log b + 1

Tactic:
⟨1, fun _ hx ↦ deriv_mul_log (zero_lt_one.trans_le hx).ne'⟩

Premises used: LT.lt.ne', zero_lt_one, Real.deriv_mul_log, LT.lt.trans_le, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
⊢ ∃ (a : ℝ), ∀ b ≥ a, deriv (fun (x : ℝ) ↦ x * log x) b = log b + 1

Tactic:
exact ⟨1, fun _ hx ↦ deriv_mul_log (zero_lt_one.trans_le hx).ne'⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ derivWithin (fun (x : ℝ) ↦ x * log x) (Set.Ioi x) x) atTop atTop

Tactic:
(tendsto_congr' ?_).mpr (tendsto_log_atTop.atTop_add (tendsto_const_nhds (x := 1)))

Premises used: Iff.mpr, tendsto_const_nhds, Filter.Tendsto.atTop_add, Real.tendsto_log_atTop, Filter.tendsto_congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
refine :
  EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ derivWithin (fun (x : ℝ) ↦ x * log x) (Set.Ioi x) x) fun (x : ℝ) ↦
    log x + 1
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ derivWithin (fun (x : ℝ) ↦ x * log x) (Set.Ioi x) x) atTop atTop

Tactic:
refine (tendsto_congr' ?_).mpr (tendsto_log_atTop.atTop_add (tendsto_const_nhds (x := 1)))

Premises used: Iff.mpr, tendsto_const_nhds, Filter.Tendsto.atTop_add, Real.tendsto_log_atTop, Filter.tendsto_congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
rw : ∃ (a : ℝ), ∀ b ≥ a, derivWithin (fun (x : ℝ) ↦ x * log x) (Set.Ioi b) b = log b + 1
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ derivWithin (fun (x : ℝ) ↦ x * log x) (Set.Ioi x) x) fun (x : ℝ) ↦
    log x + 1

Tactic:
rw [EventuallyEq, eventually_atTop]

Premises used: Filter.EventuallyEq, Filter.eventually_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
⊢ ∃ (a : ℝ), ∀ b ≥ a, derivWithin (fun (x : ℝ) ↦ x * log x) (Set.Ioi b) b = log b + 1

Tactic:
⟨1, fun _ hx ↦ rightDeriv_mul_log (zero_lt_one.trans_le hx).ne'⟩

Premises used: Real.rightDeriv_mul_log, LT.lt.ne', zero_lt_one, LT.lt.trans_le, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
⊢ ∃ (a : ℝ), ∀ b ≥ a, derivWithin (fun (x : ℝ) ↦ x * log x) (Set.Ioi b) b = log b + 1

Tactic:
exact ⟨1, fun _ hx ↦ rightDeriv_mul_log (zero_lt_one.trans_le hx).ne'⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
⊢ ¬DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x * log x) 0

Tactic:
fun h ↦
  (not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi (fun x : ℝ ↦ x * log x) (a := 0))
    tendsto_deriv_mul_log_nhdsWithin_zero
    (h.differentiableWithinAt (s := Set.Ioi 0))

Premises used: HMul.hMul, not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi, DifferentiableAt.differentiableWithinAt, Real.log, Not, _private.0.Real.tendsto_deriv_mul_log_nhdsWithin_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
⊢ Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ x * log x) 0) 0

Tactic:
deriv_zero_of_not_differentiableAt not_DifferentiableAt_log_mul_zero

Premises used: deriv_zero_of_not_differentiableAt, Real.not_DifferentiableAt_log_mul_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
⊢ Disjoint (α := Filter ℝ) (𝓝 (deriv (fun (x : ℝ) ↦ x * log x) 0)) Filter.atBot

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
pos : ∀ (hx : x = 0), deriv (deriv fun (x : ℝ) ↦ x * log x) x = x⁻¹
neg : ∀ (hx : ¬x = 0), deriv (deriv fun (x : ℝ) ↦ x * log x) x = x⁻¹
⊢ deriv (deriv fun (x : ℝ) ↦ x * log x) x = x⁻¹

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : x = 0
pos : Eq (α := ℝ) (deriv (𝕜 := ℝ) (deriv fun (x : ℝ) ↦ x * log x) 0) 0
⊢ deriv (deriv fun (x : ℝ) ↦ x * log x) x = x⁻¹

Tactic:
rw [hx, inv_zero]

Premises used: inv_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : x = 0
⊢ Eq (α := ℝ) (deriv (𝕜 := ℝ) (deriv fun (x : ℝ) ↦ x * log x) 0) 0

Tactic:
deriv_zero_of_not_differentiableAt
      (fun h ↦ not_continuousAt_deriv_mul_log_zero h.continuousAt)

Premises used: deriv_zero_of_not_differentiableAt, Real.not_continuousAt_deriv_mul_log_zero, DifferentiableAt.continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : x = 0
⊢ Eq (α := ℝ) (deriv (𝕜 := ℝ) (deriv fun (x : ℝ) ↦ x * log x) 0) 0

Tactic:
exact deriv_zero_of_not_differentiableAt
      (fun h ↦ not_continuousAt_deriv_mul_log_zero h.continuousAt)

Premises used: deriv_zero_of_not_differentiableAt, Real.not_continuousAt_deriv_mul_log_zero, DifferentiableAt.continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
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⁻¹

Tactic:
(Filter.EventuallyEq.deriv_eq this).trans ?_

Premises used: Filter.EventuallyEq.deriv_eq, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : ¬x = 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, deriv (fun (x : ℝ) ↦ x * log x) y = log y + 1
refine : deriv (fun (x : ℝ) ↦ log x + 1) x = x⁻¹
⊢ deriv (deriv fun (x : ℝ) ↦ x * log x) x = x⁻¹

Tactic:
refine (Filter.EventuallyEq.deriv_eq this).trans ?_

Premises used: Filter.EventuallyEq.deriv_eq, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : ¬x = 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, deriv (fun (x : ℝ) ↦ x * log x) y = log y + 1
rw : deriv log x = x⁻¹
rw₁ rw₂ : x⁻¹ = x⁻¹
⊢ deriv (fun (x : ℝ) ↦ log x + 1) x = x⁻¹

Tactic:
rw [deriv_add_const, deriv_log x]

Premises used: Real.deriv_log, deriv_add_const
-- Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Goal:
x : ℝ
hx : ¬x = 0
neg : ∀ᶠ (y : ℝ) in 𝓝 x, deriv (fun (x : ℝ) ↦ x * log x) y = log y + 1
⊢ deriv (deriv fun (x : ℝ) ↦ x * log x) x = x⁻¹

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]