awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
a b : EReal
⊢ a.exp ≤ b.exp ↔ a ≤ b

Tactic:
exp_strictMono.le_iff_le

Premises used: EReal.exp_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
a : EReal
⊢ a.exp ≤ 1 ↔ a ≤ 0

Tactic:
exp_zero ▸ @exp_le_exp_iff a 0

Premises used: Eq.rec, EReal.exp_zero, EReal.exp_le_exp_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
a : EReal
⊢ 1 ≤ a.exp ↔ 0 ≤ a

Tactic:
exp_zero ▸ @exp_le_exp_iff 0 a

Premises used: Eq.rec, EReal.exp_zero, EReal.exp_le_exp_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
x : EReal
bot : exp (-⊥) = (exp ⊥)⁻¹
coe : ∀ (a : ℝ), (-(↑a : EReal)).exp = (↑a : EReal).exp⁻¹
top : exp (-⊤) = (exp ⊤)⁻¹
⊢ (-x).exp = x.exp⁻¹

Tactic:
induction x
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
⊢ exp (-⊥) = (exp ⊥)⁻¹

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
a : ℝ
coe : (-(↑a : EReal)).exp = (ENNReal.ofReal (Real.exp a))⁻¹
coe₁ : (↑(-a) : EReal).exp = (ENNReal.ofReal (Real.exp a))⁻¹
coe₂ : ENNReal.ofReal (Real.exp (-a)) = (ENNReal.ofReal (Real.exp a))⁻¹
coe₃ : ENNReal.ofReal (Real.exp (-a)) = ENNReal.ofReal (Real.exp a)⁻¹
coe₄ coe₅ : ENNReal.ofReal (Real.exp a)⁻¹ = ENNReal.ofReal (Real.exp a)⁻¹
⊢ (-(↑a : EReal)).exp = (↑a : EReal).exp⁻¹

Tactic:
rw [exp_coe, ← EReal.coe_neg, exp_coe, ← ENNReal.ofReal_inv_of_pos (Real.exp_pos _),
      Real.exp_neg]

Premises used: EReal.coe_neg, EReal.exp_coe, ENNReal.ofReal_inv_of_pos, Real.exp_neg, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
⊢ exp (-⊤) = (exp ⊤)⁻¹

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
x y : EReal
bot : (⊥ + y).exp = exp ⊥ * y.exp
coe : ∀ (a : ℝ), ((↑a : EReal) + y).exp = (↑a : EReal).exp * y.exp
top : (⊤ + y).exp = exp ⊤ * y.exp
⊢ (x + y).exp = x.exp * y.exp

Tactic:
induction x
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
y : EReal
⊢ (⊥ + y).exp = exp ⊥ * y.exp

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
y : EReal
a : ℝ
coe : ((↑a : EReal) + ⊥).exp = (↑a : EReal).exp * exp ⊥
coe₁ : ∀ (a_1 : ℝ), ((↑a : EReal) + (↑a_1 : EReal)).exp = (↑a : EReal).exp * (↑a_1 : EReal).exp
coe₂ : ((↑a : EReal) + ⊤).exp = (↑a : EReal).exp * exp ⊤
⊢ ((↑a : EReal) + y).exp = (↑a : EReal).exp * y.exp

Tactic:
induction y
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
a : ℝ
⊢ ((↑a : EReal) + ⊥).exp = (↑a : EReal).exp * exp ⊥

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
a a_1 : ℝ
coe : ENNReal.ofReal (Real.exp (a + a_1)) = ENNReal.ofReal (Real.exp a * Real.exp a_1)
coe₁ coe₂ : ENNReal.ofReal (Real.exp a * Real.exp a_1) = ENNReal.ofReal (Real.exp a * Real.exp a_1)
⊢ ENNReal.ofReal (Real.exp (a + a_1)) = ENNReal.ofReal (Real.exp a) * ENNReal.ofReal (Real.exp a_1)

Tactic:
rw [← ENNReal.ofReal_mul (Real.exp_nonneg _), Real.exp_add]

Premises used: ENNReal.ofReal_mul, Real.exp_nonneg, Real.exp_add
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
a : ℝ
coe : ENNReal.ofReal (Real.exp a) ≠ 0
⊢ ∞ = ENNReal.ofReal (Real.exp a) * ∞

Tactic:
rw [ENNReal.mul_top]

Premises used: ENNReal.mul_top
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
a : ℝ
⊢ ENNReal.ofReal (Real.exp a) ≠ 0

Tactic:
simp [Real.exp_pos]

Premises used: Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
y : EReal
top : (HAdd.hAdd (α := EReal) ⊤ ⊥).exp = exp ⊤ * exp ⊥
top₁ : ∀ (a : ℝ), (⊤ + (↑a : EReal)).exp = exp ⊤ * (↑a : EReal).exp
top₂ : (HAdd.hAdd (α := EReal) ⊤ ⊤).exp = exp ⊤ * exp ⊤
⊢ (⊤ + y).exp = exp ⊤ * y.exp

Tactic:
induction y
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
⊢ (HAdd.hAdd (α := EReal) ⊤ ⊥).exp = exp ⊤ * exp ⊥

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
a : ℝ
top : ENNReal.ofReal (Real.exp a) ≠ 0
⊢ ∞ = ∞ * ENNReal.ofReal (Real.exp a)

Tactic:
rw [ENNReal.top_mul]

Premises used: ENNReal.top_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
⊢ (HAdd.hAdd (α := EReal) ⊤ ⊤).exp = exp ⊤ * exp ⊤

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
simp : ¬Tendsto (β := ℝ) (fun (t : ℝ) ↦ (log t * t)⁻¹) (nhdsWithin 0 {0}ᶜ) (nhds (deriv (fun (x : ℝ) ↦ (log x)⁻¹) 0))
⊢ ¬DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ (log x)⁻¹) 0

Tactic:
simp only [← hasDerivAt_deriv_iff, hasDerivAt_iff_tendsto_slope_zero, zero_add, log_zero,
    inv_zero, sub_zero, smul_eq_mul, ← mul_inv, mul_comm _ (log _)]

Premises used: sub_zero, mul_inv, inv_zero, hasDerivAt_deriv_iff, zero_add, Real.log, hasDerivAt_iff_tendsto_slope_zero, mul_comm, smul_eq_mul, Real.log_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (nhdsWithin 0 (Set.Iio 0)) (nhdsWithin 0 (Set.Ioi 0))

Tactic:
tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
      tendsto_log_mul_self_nhdsLT_zero ?_

Premises used: tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within, tendsto_log_mul_self_nhdsLT_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
refine : ∀ᶠ (x : ℝ) in nhdsWithin 0 (Set.Iio 0), Membership.mem (γ := Set ℝ) (Set.Ioi 0) (log x * x)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (nhdsWithin 0 (Set.Iio 0)) (nhdsWithin 0 (Set.Ioi 0))

Tactic:
refine tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
      tendsto_log_mul_self_nhdsLT_zero ?_

Premises used: tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within, tendsto_log_mul_self_nhdsLT_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
simp : ∀ᶠ (x : ℝ) in nhdsWithin 0 (Set.Ioo (-1) 0), 0 < log x * x
⊢ ∀ᶠ (x : ℝ) in nhdsWithin 0 (Set.Iio 0), Membership.mem (γ := Set ℝ) (Set.Ioi 0) (log x * x)

Tactic:
simp only [← nhdsWithin_Ioo_eq_nhdsLT neg_one_lt_zero, Set.mem_Ioi]

Premises used: nhdsWithin_Ioo_eq_nhdsLT, Set.mem_Ioi, neg_one_lt_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
⊢ ∀ᶠ (x : ℝ) in nhdsWithin 0 (Set.Ioo (-1) 0), 0 < log x * x

Tactic:
eventually_nhdsWithin_of_forall fun x ⟨hx₁, hx₂⟩ ↦ mul_pos_of_neg_of_neg ?_ hx₂

Premises used: HMul.hMul, Real.log, LT.lt, _private.0.Real.not_differentiableAt_inv_log_zero.match_4, OfNat.ofNat, mul_pos_of_neg_of_neg, eventually_nhdsWithin_of_forall
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
refine : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 0) x → ∀ (hx₁ : -1 < x) (hx₂ : x < 0), log x < 0
⊢ ∀ᶠ (x : ℝ) in nhdsWithin 0 (Set.Ioo (-1) 0), 0 < log x * x

Tactic:
refine eventually_nhdsWithin_of_forall fun x ⟨hx₁, hx₂⟩ ↦ mul_pos_of_neg_of_neg ?_ hx₂

Premises used: eventually_nhdsWithin_of_forall
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
x : ℝ
h : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 0) x
hx₁ : -1 < x
hx₂ : x < 0
⊢ log x < 0

Tactic:
log_neg_eq_log x ▸ log_neg ?_ ?_

Premises used: Real.log_neg_eq_log, Eq.rec, Real.log_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
x : ℝ
h : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 0) x
hx₁ : -1 < x
hx₂ : x < 0
refine_1 : 0 < -x
refine_2 : -x < 1
⊢ log x < 0

Tactic:
refine log_neg_eq_log x ▸ log_neg ?_ ?_
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
x : ℝ
h : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 0) x
hx₁ : -1 < x
hx₂ : x < 0
⊢ 0 < -x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
x : ℝ
h : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 0) x
hx₁ : -1 < x
hx₂ : x < 0
⊢ -x < 1

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (nhdsWithin 0 (Set.Iio 0)) (nhdsWithin 0 (Set.Ioi 0))

Tactic:
have H' : Tendsto (fun x ↦ log x * x) (nhdsWithin 0 (Set.Iio 0)) (nhdsWithin 0 (Set.Ioi 0)) := by
    refine tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
      tendsto_log_mul_self_nhdsLT_zero ?_
    simp only [← nhdsWithin_Ioo_eq_nhdsLT neg_one_lt_zero, Set.mem_Ioi]
    refine eventually_nhdsWithin_of_forall fun x ⟨hx₁, hx₂⟩ ↦ mul_pos_of_neg_of_neg ?_ hx₂
    refine log_neg_eq_log x ▸ log_neg ?_ ?_ <;> grind
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
H' : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (nhdsWithin 0 (Set.Iio 0)) (nhdsWithin 0 (Set.Ioi 0))
H : Tendsto (β := ℝ) (fun (t : ℝ) ↦ (log t * t)⁻¹) (nhdsWithin 0 {0}ᶜ) (nhds (deriv (fun (x : ℝ) ↦ (log x)⁻¹) 0))
⊢ Subset (α := Set ℝ) (Set.Iio 0) {0}ᶜ

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
H' : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (nhdsWithin 0 (Set.Iio 0)) (nhdsWithin 0 (Set.Ioi 0))
H : Tendsto (β := ℝ) (fun (t : ℝ) ↦ (log t * t)⁻¹) (nhdsWithin 0 {0}ᶜ) (nhds (deriv (fun (x : ℝ) ↦ (log x)⁻¹) 0))
⊢ Disjoint (α := Filter ℝ) (nhds (deriv (fun (x : ℝ) ↦ (log x)⁻¹) 0)) atTop

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
H' : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (nhdsWithin 0 (Set.Iio 0)) (nhdsWithin 0 (Set.Ioi 0))
⊢ ¬Tendsto (β := ℝ) (fun (t : ℝ) ↦ (log t * t)⁻¹) (nhdsWithin 0 {0}ᶜ) (nhds (deriv (fun (x : ℝ) ↦ (log x)⁻¹) 0))

Tactic:
exact fun H ↦ (tendsto_nhdsWithin_mono_left (show Set.Iio (0 : ℝ) ⊆ _ by grind) H).not_tendsto
    (by simp) (tendsto_inv_nhdsGT_zero.comp H')

Premises used: tendsto_nhdsWithin_mono_left, tendsto_inv_nhdsGT_zero, Filter.Tendsto.not_tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
suffices : Tendsto (fun (x : ℝ) ↦ (log x)⁻¹) (nhdsWithin 1 {1}ᶜ) (Bornology.cobounded ℝ)
⊢ ¬ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ (log x)⁻¹) 1

Tactic:
suffices Tendsto (fun x ↦ (log x)⁻¹) (nhdsWithin 1 {1}ᶜ) (Bornology.cobounded ℝ) from
    not_continuousAt_of_tendsto this nhdsWithin_le_nhds (Metric.disjoint_nhds_cobounded _)
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
⊢ HasDerivAt log 1 1

Tactic:
simpa using hasDerivAt_log one_ne_zero

Premises used: Real.hasDerivAt_log, one_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
⊢ Tendsto log (nhdsWithin 1 {1}ᶜ) (nhdsWithin (log 1) {log 1}ᶜ)

Tactic:
have H := HasDerivAt.tendsto_nhdsNE (by simpa using hasDerivAt_log one_ne_zero) one_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
H : Tendsto log (nhdsWithin 1 {1}ᶜ) (nhdsWithin (log 1) {log 1}ᶜ)
⊢ Tendsto (fun (x : ℝ) ↦ (log x)⁻¹) (nhdsWithin 1 {1}ᶜ) (Bornology.cobounded ℝ)

Tactic:
tendsto_inv₀_nhdsNE_zero.comp <| log_one ▸ H

Premises used: Eq.rec, Real.log_one, Filter.Tendsto.comp, Filter.tendsto_inv₀_nhdsNE_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
H : Tendsto log (nhdsWithin 1 {1}ᶜ) (nhdsWithin (log 1) {log 1}ᶜ)
⊢ Tendsto (fun (x : ℝ) ↦ (log x)⁻¹) (nhdsWithin 1 {1}ᶜ) (Bornology.cobounded ℝ)

Tactic:
exact tendsto_inv₀_nhdsNE_zero.comp <| log_one ▸ H

Premises used: Filter.Tendsto.comp, Filter.tendsto_inv₀_nhdsNE_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
⊢ ¬ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ (log x)⁻¹) (-1)

Tactic:
fun H ↦ not_continuousAt_inv_log_one ?_

Premises used: Real.not_continuousAt_inv_log_one, Not
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
refine : ∀ (H : ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ (log x)⁻¹) (-1)), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ (log x)⁻¹) 1
⊢ ¬ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ (log x)⁻¹) (-1)

Tactic:
refine fun H ↦ not_continuousAt_inv_log_one ?_

Premises used: Real.not_continuousAt_inv_log_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
H : ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ (log x)⁻¹) (-1)
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ (log x)⁻¹) 1

Tactic:
simpa only [log_neg_eq_log] using ContinuousAt.comp' H continuousAt_neg

Premises used: Real.log_neg_eq_log, continuousAt_neg, ContinuousAt.comp'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
x : ℝ
inl : deriv (fun (x : ℝ) ↦ (log x)⁻¹) 0 = -0⁻¹ / HPow.hPow (β := ℕ) (log 0) 2
inr : ∀ (h0 : x ≠ 0), deriv (fun (x : ℝ) ↦ (log x)⁻¹) x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
⊢ deriv (fun (x : ℝ) ↦ (log x)⁻¹) x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2

Tactic:
rcases eq_or_ne x 0 with rfl | h0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
⊢ deriv (fun (x : ℝ) ↦ (log x)⁻¹) 0 = -0⁻¹ / HPow.hPow (β := ℕ) (log 0) 2

Tactic:
simpa using deriv_zero_of_not_differentiableAt not_differentiableAt_inv_log_zero

Premises used: deriv_zero_of_not_differentiableAt, Real.not_differentiableAt_inv_log_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
x : ℝ
h0 : x ≠ 0
inr : ∀ (h0 : Ne (α := ℝ) 1 0), deriv (fun (x : ℝ) ↦ (log x)⁻¹) 1 = -1⁻¹ / HPow.hPow (β := ℕ) (log 1) 2
inr₁ : ∀ (h1 : x ≠ 1), deriv (fun (x : ℝ) ↦ (log x)⁻¹) x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
⊢ deriv (fun (x : ℝ) ↦ (log x)⁻¹) x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2

Tactic:
rcases eq_or_ne x 1 with rfl | h1

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
h0 : Ne (α := ℝ) 1 0
⊢ deriv (fun (x : ℝ) ↦ (log x)⁻¹) 1 = -1⁻¹ / HPow.hPow (β := ℕ) (log 1) 2

Tactic:
simpa using deriv_zero_of_not_differentiableAt <|
      mt DifferentiableAt.continuousAt not_continuousAt_inv_log_one

Premises used: deriv_zero_of_not_differentiableAt, DifferentiableAt.continuousAt, mt, Real.not_continuousAt_inv_log_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
x : ℝ
h0 : x ≠ 0
h1 : x ≠ 1
inr :
  ∀ (h0 : Ne (α := ℝ) (-1) 0) (h1 : Ne (α := ℝ) (-1) 1),
    deriv (fun (x : ℝ) ↦ (log x)⁻¹) (-1) = -(-1)⁻¹ / HPow.hPow (β := ℕ) (log (-1)) 2
inr₁ : ∀ (h2 : x ≠ -1), deriv (fun (x : ℝ) ↦ (log x)⁻¹) x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
⊢ deriv (fun (x : ℝ) ↦ (log x)⁻¹) x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2

Tactic:
rcases eq_or_ne x (-1) with rfl | h2

Premises used: eq_or_ne, OfNat.ofNat, Neg.neg, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
h0 : Ne (α := ℝ) (-1) 0
h1 : Ne (α := ℝ) (-1) 1
⊢ deriv (fun (x : ℝ) ↦ (log x)⁻¹) (-1) = -(-1)⁻¹ / HPow.hPow (β := ℕ) (log (-1)) 2

Tactic:
simpa using deriv_zero_of_not_differentiableAt <|
      mt DifferentiableAt.continuousAt not_continuousAt_inv_log_neg_one

Premises used: Real.not_continuousAt_inv_log_neg_one, deriv_zero_of_not_differentiableAt, DifferentiableAt.continuousAt, mt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog
Goal:
x : ℝ
h0 : x ≠ 0
h1 : x ≠ 1
h2 : x ≠ -1
⊢ deriv (fun (x : ℝ) ↦ (log x)⁻¹) x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
Goal:
⊢ StrictMonoOn (β := ℝ) (fun (x : ℝ) ↦ x * log x) (Ici (rexp (-1)))

Tactic:
strictMonoOn_of_deriv_pos (convex_Ici _) continuous_mul_log.continuousOn fun x hx ↦ ?_

Premises used: Real.continuous_mul_log, Continuous.continuousOn, convex_Ici, strictMonoOn_of_deriv_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
Goal:
refine : ∀ (x : ℝ) (hx : x ∈ interior (Ici (rexp (-1)))), LT.lt (α := ℝ) 0 (deriv (fun (x : ℝ) ↦ x * log x) x)
⊢ StrictMonoOn (β := ℝ) (fun (x : ℝ) ↦ x * log x) (Ici (rexp (-1)))

Tactic:
refine strictMonoOn_of_deriv_pos (convex_Ici _) continuous_mul_log.continuousOn fun x hx ↦ ?_

Premises used: Real.continuous_mul_log, Continuous.continuousOn, convex_Ici, strictMonoOn_of_deriv_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
Goal:
x : ℝ
hx : x ∈ interior (Ici (rexp (-1)))
⊢ rexp (-1) < x

Tactic:
simpa using hx
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
Goal:
x : ℝ
hx : x ∈ interior (Ici (rexp (-1)))
⊢ rexp (-1) < x

Tactic:
have hlt : rexp (-1) < x := by simpa using hx
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
Goal:
x : ℝ
hx : x ∈ interior (Ici (rexp (-1)))
hlt : rexp (-1) < x
⊢ 0 < x

Tactic:
grind [Real.exp_pos]

Premises used: Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
Goal:
x : ℝ
hx : x ∈ interior (Ici (rexp (-1)))
hlt : rexp (-1) < x
⊢ 0 < x

Tactic:
have hpos : 0 < x := by grind [Real.exp_pos]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
Goal:
x : ℝ
hx : x ∈ interior (Ici (rexp (-1)))
hlt : rexp (-1) < x
hpos : 0 < x
⊢ LT.lt (α := ℝ) 0 (deriv (fun (x : ℝ) ↦ x * log x) x)

Tactic:
grind [deriv_mul_log, Real.lt_log_iff_exp_lt hpos |>.mpr hlt]

Premises used: Iff.mpr, Real.lt_log_iff_exp_lt, Real.deriv_mul_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
Goal:
⊢ rexp (-1) < 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
Goal:
⊢ MonotoneOn (β := ℝ) (fun (x : ℝ) ↦ log x * x) {x : ℝ | 1 ≤ x}

Tactic:
grind [mul_log_strictMonoOn.monotoneOn, MonotoneOn.mono, show exp (-1) < 1 by norm_num]

Premises used: Real.mul_log_strictMonoOn, StrictMonoOn.monotoneOn, MonotoneOn.mono
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
Goal:
⊢ StrictAntiOn (β := ℝ) (fun (x : ℝ) ↦ x * log x) (Icc 0 (rexp (-1)))

Tactic:
strictAntiOn_of_deriv_neg (convex_Icc ..) continuous_mul_log.continuousOn fun x hx ↦ ?_

Premises used: Real.continuous_mul_log, Continuous.continuousOn, convex_Icc, strictAntiOn_of_deriv_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
Goal:
refine : ∀ (x : ℝ) (hx : x ∈ interior (Icc 0 (rexp (-1)))), LT.lt (α := ℝ) (deriv (fun (x : ℝ) ↦ x * log x) x) 0
⊢ StrictAntiOn (β := ℝ) (fun (x : ℝ) ↦ x * log x) (Icc 0 (rexp (-1)))

Tactic:
refine strictAntiOn_of_deriv_neg (convex_Icc ..) continuous_mul_log.continuousOn fun x hx ↦ ?_

Premises used: Real.continuous_mul_log, Continuous.continuousOn, convex_Icc, strictAntiOn_of_deriv_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
Goal:
x : ℝ
hx : x ∈ interior (Icc 0 (rexp (-1)))
⊢ x < rexp (-1)

Tactic:
simp_all [interior_Icc, mem_Ioo]

Premises used: Set.mem_Ioo, interior_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
Goal:
x : ℝ
hx : x ∈ interior (Icc 0 (rexp (-1)))
⊢ x < rexp (-1)

Tactic:
have hgt : x < rexp (-1) := by simp_all [interior_Icc, mem_Ioo]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
Goal:
x : ℝ
hx : x ∈ interior (Icc 0 (rexp (-1)))
hgt : x < rexp (-1)
⊢ 0 < x

Tactic:
simp_all [interior_Icc, mem_Ioo]

Premises used: Set.mem_Ioo, interior_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
Goal:
x : ℝ
hx : x ∈ interior (Icc 0 (rexp (-1)))
hgt : x < rexp (-1)
⊢ 0 < x

Tactic:
have hpos : 0 < x := by simp_all [interior_Icc, mem_Ioo]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
Goal:
x : ℝ
hx : x ∈ interior (Icc 0 (rexp (-1)))
hgt : x < rexp (-1)
hpos : 0 < x
⊢ LT.lt (α := ℝ) (deriv (fun (x : ℝ) ↦ x * log x) x) 0

Tactic:
grind [deriv_mul_log, Real.log_lt_iff_lt_exp hpos |>.mpr hgt]

Premises used: Iff.mpr, Real.log_lt_iff_lt_exp, Real.deriv_mul_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
Goal:
x : ℝ
hex : x ∈ Ici (rexp 1)
y : ℝ
hey : y ∈ Ici (rexp 1)
hxy : x ≤ y
⊢ 0 < x

Tactic:
have x_pos : 0 < x := (exp_pos 1).trans_le hex
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
Goal:
x : ℝ
hex : x ∈ Ici (rexp 1)
y : ℝ
hey : y ∈ Ici (rexp 1)
hxy : x ≤ y
x_pos : 0 < x
⊢ 0 < y

Tactic:
have y_pos : 0 < y := (exp_pos 1).trans_le hey
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
Goal:
x : ℝ
hex : x ∈ Ici (rexp 1)
y : ℝ
hey : y ∈ Ici (rexp 1)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
rwa rwa₁ rwa₂ rwa₃ : rexp 1 ≤ x
⊢ 1 ≤ log x

Tactic:
rwa [le_log_iff_exp_le x_pos]

Premises used: Real.le_log_iff_exp_le
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
Goal:
x : ℝ
hex : x ∈ Ici (rexp 1)
y : ℝ
hey : y ∈ Ici (rexp 1)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ 1 ≤ log x

Tactic:
have hlogx : 1 ≤ log x := by rwa [le_log_iff_exp_le x_pos]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
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
rwa : HAdd.hAdd (α := ℝ) 0 1 ≤ y / x
rwa₁ : HAdd.hAdd (α := ℝ) 0 1 * x ≤ y
rwa₂ : 1 * x ≤ y
rwa₃ rwa₄ rwa₅ rwa₆ : x ≤ y
⊢ 0 ≤ y / x - 1

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

Premises used: zero_add, le_sub_iff_add_le, le_div_iff₀, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
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
⊢ 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]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
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
rw : log y - log x ≤ (fun (x : ℝ) ↦ log x / x) x * y - log x
⊢ LE.le (α := ℝ) ((fun (x : ℝ) ↦ log x / x) y) ((fun (x : ℝ) ↦ log x / x) x)

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

Premises used: div_le_iff₀, sub_le_sub_iff_right, Real.log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
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
rw rw₁ : log y - log x = log y - log x
⊢ log y - log x = log (y / x)

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

Premises used: Real.log_div, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
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 / x) ≤ y / x - 1

Tactic:
log_le_sub_one_of_pos (div_pos y_pos x_pos)

Premises used: div_pos, Real.log_le_sub_one_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
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
⊢ y / x - 1 ≤ log x * (y / x - 1)

Tactic:
le_mul_of_one_le_left hyx hlogx

Premises used: le_mul_of_one_le_left
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
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 x * (y / x - 1) = log x / x * y - log x

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
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)
log₁ : Real.log x * (y / x - 1) = Real.log x / x * y - Real.log x
⊢ Real.log y - Real.log x ≤ (fun (x : ℝ) ↦ Real.log x / 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

Premises used: le_mul_of_one_le_left, HSub.hSub, HDiv.hDiv, Real.log, div_pos, OfNat.ofNat, Real.log_le_sub_one_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone
Goal:
a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
_ : y ∈ Ici (rexp a⁻¹) → x ≤ y → LE.le (α := ℝ) ((fun (x : ℝ) ↦ log x / x ^ a) y) ((fun (x : ℝ) ↦ log x / x ^ a) x)
⊢ y ∈ Ici (rexp a⁻¹) → x ≤ y → LE.le (α := ℝ) ((fun (x : ℝ) ↦ log x / x ^ a) y) ((fun (x : ℝ) ↦ log x / x ^ a) x)

Tactic:
_
-- 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
⊢ 0 < x

Tactic:
have x_pos : 0 < x := lt_of_lt_of_le (exp_pos a⁻¹) (le_of_le_of_eq hex rfl)
-- 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
linarith : y ≤ 0 → x - y + (0 - x) + (y - 0) = 0
⊢ 0 < y

Tactic:
linarith
-- 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
⊢ 0 < y

Tactic:
have y_pos : 0 < y := by linarith
-- 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
nth_rw : log (HPow.hPow (β := ℝ) y 1) / y ^ a ≤ log (HPow.hPow (β := ℝ) x 1) / x ^ a
⊢ log y / y ^ a ≤ log x / x ^ a

Tactic:
nth_rw 1 [← rpow_one y, ← rpow_one x]

Premises used: Real.rpow_one