awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
b : ℝ≥0∞
hb : 1 < b
⊢ Filter.Tendsto (β := ℝ≥0∞) (fun (x : ℝ) ↦ ((↑x : EReal) * b.log).exp) Filter.atBot (𝓝 0)
have refine : Filter.Tendsto (β := EReal) (fun (x : ℝ) ↦ (↑x : EReal) * b.log) Filter.atBot (𝓝 ⊥)
Tactic: refine EReal.tendsto_exp_nhds_bot_nhds_zero.comp ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
b : ℝ≥0∞
hb : 1 < b
⊢ Filter.Tendsto (β := EReal) (fun (x : ℝ) ↦ (↑x : EReal) * b.log) Filter.atBot (𝓝 ⊥)
have h : ⊥ = ⊥ * b.log
Tactic: convert! EReal.Tendsto.mul_const tendsto_coe_atBot _ _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
b : ℝ≥0∞
hb : 1 < b
h : ⊥ = ⊥ * b.log
⊢ Filter.Tendsto (β := EReal) (fun (x : ℝ) ↦ (↑x : EReal) * b.log) Filter.atBot (𝓝 ⊥)
have convert_2 : Ne (α := EReal) ⊥ 0 ∨ b.log ≠ ⊥
Tactic: convert! EReal.Tendsto.mul_const tendsto_coe_atBot _ _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
b : ℝ≥0∞
hb : 1 < b
h : ⊥ = ⊥ * b.log
convert_2 : Ne (α := EReal) ⊥ 0 ∨ b.log ≠ ⊥
⊢ Filter.Tendsto (β := EReal) (fun (x : ℝ) ↦ (↑x : EReal) * b.log) Filter.atBot (𝓝 ⊥)
have convert_3 : Ne (α := EReal) ⊥ 0 ∨ b.log ≠ ⊤
Tactic: convert! EReal.Tendsto.mul_const tendsto_coe_atBot _ _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
b : ℝ≥0∞
hb : 1 < b
⊢ ⊥ = ⊥ * b.log
have h : Eq (α := EReal) ⊥ ⊥
Tactic: rw [EReal.bot_mul_of_pos (zero_lt_log_iff.2 hb)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
b : ℝ≥0∞
hb : b < 1
⊢ Filter.Tendsto (β := ℝ≥0∞) (fun (x : ℝ) ↦ b ^ x) Filter.atBot (𝓝 ∞)
have simp_rw : Filter.Tendsto (β := ℝ≥0∞) (fun (x : ℝ) ↦ ((↑x : EReal) * b.log).exp) Filter.atBot (𝓝 ∞)
Tactic: simp_rw [ENNReal.rpow_eq_exp_mul_log]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
b : ℝ≥0∞
hb : b < 1
⊢ Filter.Tendsto (β := ℝ≥0∞) (fun (x : ℝ) ↦ ((↑x : EReal) * b.log).exp) Filter.atBot (𝓝 ∞)
have refine : Filter.Tendsto (β := EReal) (fun (x : ℝ) ↦ (↑x : EReal) * b.log) Filter.atBot (𝓝 ⊤)
Tactic: refine EReal.tendsto_exp_nhds_top_nhds_top.comp ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
b : ℝ≥0∞
hb : b < 1
⊢ Filter.Tendsto (β := EReal) (fun (x : ℝ) ↦ (↑x : EReal) * b.log) Filter.atBot (𝓝 ⊤)
have h : ⊤ = ⊥ * b.log
Tactic: convert! EReal.Tendsto.mul_const tendsto_coe_atBot _ _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
b : ℝ≥0∞
hb : b < 1
h : ⊤ = ⊥ * b.log
⊢ Filter.Tendsto (β := EReal) (fun (x : ℝ) ↦ (↑x : EReal) * b.log) Filter.atBot (𝓝 ⊤)
have convert_2 : Ne (α := EReal) ⊥ 0 ∨ b.log ≠ ⊥
Tactic: convert! EReal.Tendsto.mul_const tendsto_coe_atBot _ _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
b : ℝ≥0∞
hb : b < 1
h : ⊤ = ⊥ * b.log
convert_2 : Ne (α := EReal) ⊥ 0 ∨ b.log ≠ ⊥
⊢ Filter.Tendsto (β := EReal) (fun (x : ℝ) ↦ (↑x : EReal) * b.log) Filter.atBot (𝓝 ⊤)
have convert_3 : Ne (α := EReal) ⊥ 0 ∨ b.log ≠ ⊤
Tactic: convert! EReal.Tendsto.mul_const tendsto_coe_atBot _ _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
b : ℝ≥0∞
hb : b < 1
⊢ ⊤ = ⊥ * b.log
have h : Eq (α := EReal) ⊤ ⊤
Tactic: rw [EReal.bot_mul_of_neg (log_lt_zero_iff.2 hb)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
x : EReal
⊢ x.exp = 0 ↔ x = ⊥
have bot : exp ⊥ = 0 ↔ Eq (α := EReal) ⊥ ⊥
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
x : EReal
bot : exp ⊥ = 0 ↔ Eq (α := EReal) ⊥ ⊥
⊢ x.exp = 0 ↔ x = ⊥
have coe : ∀ (a : ℝ), (↑a : EReal).exp = 0 ↔ (↑a : EReal) = ⊥
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
x : EReal
bot : exp ⊥ = 0 ↔ Eq (α := EReal) ⊥ ⊥
coe : ∀ (a : ℝ), (↑a : EReal).exp = 0 ↔ (↑a : EReal) = ⊥
⊢ x.exp = 0 ↔ x = ⊥
have top : exp ⊤ = 0 ↔ Eq (α := EReal) ⊤ ⊥
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
x : EReal
⊢ x.exp = ∞ ↔ x = ⊤
have bot : exp ⊥ = ∞ ↔ Eq (α := EReal) ⊥ ⊤
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
x : EReal
bot : exp ⊥ = ∞ ↔ Eq (α := EReal) ⊥ ⊤
⊢ x.exp = ∞ ↔ x = ⊤
have coe : ∀ (a : ℝ), (↑a : EReal).exp = ∞ ↔ (↑a : EReal) = ⊤
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
x : EReal
bot : exp ⊥ = ∞ ↔ Eq (α := EReal) ⊥ ⊤
coe : ∀ (a : ℝ), (↑a : EReal).exp = ∞ ↔ (↑a : EReal) = ⊤
⊢ x.exp = ∞ ↔ x = ⊤
have top : exp ⊤ = ∞ ↔ Eq (α := EReal) ⊤ ⊤
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
x y : EReal
h : x < y
⊢ x.exp < y.exp
have bot : ∀ (h : ⊥ < y), exp ⊥ < y.exp
Tactic: induction x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
x y : EReal
h : x < y
bot : ∀ (h : ⊥ < y), exp ⊥ < y.exp
⊢ x.exp < y.exp
have coe : ∀ (a : ℝ) (h : (↑a : EReal) < y), (↑a : EReal).exp < y.exp
Tactic: induction x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
x y : EReal
h : x < y
bot : ∀ (h : ⊥ < y), exp ⊥ < y.exp
coe : ∀ (a : ℝ) (h : (↑a : EReal) < y), (↑a : EReal).exp < y.exp
⊢ x.exp < y.exp
have top : ∀ (h : ⊤ < y), exp ⊤ < y.exp
Tactic: induction x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
y : EReal
h : ⊥ < y
⊢ exp ⊥ < y.exp
have bot : ¬y = ⊥
Tactic: rw [exp_bot, pos_iff_ne_zero, ne_eq, exp_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
y : EReal
a : ℝ
h : (↑a : EReal) < y
⊢ (↑a : EReal).exp < y.exp
have coe : ∀ (h : (↑a : EReal) < ⊥), (↑a : EReal).exp < exp ⊥
Tactic: induction y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
y : EReal
a : ℝ
h : (↑a : EReal) < y
coe : ∀ (h : (↑a : EReal) < ⊥), (↑a : EReal).exp < exp ⊥
⊢ (↑a : EReal).exp < y.exp
have coe₁ : ∀ (a_1 : ℝ) (h : (↑a : EReal) < (↑a_1 : EReal)), (↑a : EReal).exp < (↑a_1 : EReal).exp
Tactic: induction y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
y : EReal
a : ℝ
h : (↑a : EReal) < y
coe : ∀ (h : (↑a : EReal) < ⊥), (↑a : EReal).exp < exp ⊥
coe₁ : ∀ (a_1 : ℝ) (h : (↑a : EReal) < (↑a_1 : EReal)), (↑a : EReal).exp < (↑a_1 : EReal).exp
⊢ (↑a : EReal).exp < y.exp
have coe₂ : ∀ (h : (↑a : EReal) < ⊤), (↑a : EReal).exp < exp ⊤
Tactic: induction y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
x : EReal
⊢ (-x).exp = x.exp⁻¹
have bot : exp (-⊥) = (exp ⊥)⁻¹
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
x : EReal
bot : exp (-⊥) = (exp ⊥)⁻¹
⊢ (-x).exp = x.exp⁻¹
have coe : ∀ (a : ℝ), (-(↑a : EReal)).exp = (↑a : EReal).exp⁻¹
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
x : EReal
bot : exp (-⊥) = (exp ⊥)⁻¹
coe : ∀ (a : ℝ), (-(↑a : EReal)).exp = (↑a : EReal).exp⁻¹
⊢ (-x).exp = x.exp⁻¹
have top : exp (-⊤) = (exp ⊤)⁻¹
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
a : ℝ
⊢ (-(↑a : EReal)).exp = (↑a : EReal).exp⁻¹
have coe : (-(↑a : EReal)).exp = (ENNReal.ofReal (Real.exp a))⁻¹
Tactic: rw [exp_coe, ← EReal.coe_neg, exp_coe, ← ENNReal.ofReal_inv_of_pos (Real.exp_pos _),
      Real.exp_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
a : ℝ
coe : (-(↑a : EReal)).exp = (ENNReal.ofReal (Real.exp a))⁻¹
⊢ (-(↑a : EReal)).exp = (↑a : EReal).exp⁻¹
have coe₁ : (↑(-a) : EReal).exp = (ENNReal.ofReal (Real.exp a))⁻¹
Tactic: rw [exp_coe, ← EReal.coe_neg, exp_coe, ← ENNReal.ofReal_inv_of_pos (Real.exp_pos _),
      Real.exp_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
a : ℝ
coe : (-(↑a : EReal)).exp = (ENNReal.ofReal (Real.exp a))⁻¹
coe₁ : (↑(-a) : EReal).exp = (ENNReal.ofReal (Real.exp a))⁻¹
⊢ (-(↑a : EReal)).exp = (↑a : EReal).exp⁻¹
have coe₂ : ENNReal.ofReal (Real.exp (-a)) = (ENNReal.ofReal (Real.exp a))⁻¹
Tactic: rw [exp_coe, ← EReal.coe_neg, exp_coe, ← ENNReal.ofReal_inv_of_pos (Real.exp_pos _),
      Real.exp_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
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))⁻¹
⊢ (-(↑a : EReal)).exp = (↑a : EReal).exp⁻¹
have coe₃ : ENNReal.ofReal (Real.exp (-a)) = ENNReal.ofReal (Real.exp a)⁻¹
Tactic: rw [exp_coe, ← EReal.coe_neg, exp_coe, ← ENNReal.ofReal_inv_of_pos (Real.exp_pos _),
      Real.exp_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
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)⁻¹
⊢ (-(↑a : EReal)).exp = (↑a : EReal).exp⁻¹
have coe₄ : ENNReal.ofReal (Real.exp a)⁻¹ = ENNReal.ofReal (Real.exp a)⁻¹
Tactic: rw [exp_coe, ← EReal.coe_neg, exp_coe, ← ENNReal.ofReal_inv_of_pos (Real.exp_pos _),
      Real.exp_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
x y : EReal
⊢ (x + y).exp = x.exp * y.exp
have bot : (⊥ + y).exp = exp ⊥ * y.exp
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
x y : EReal
bot : (⊥ + y).exp = exp ⊥ * y.exp
⊢ (x + y).exp = x.exp * y.exp
have coe : ∀ (a : ℝ), ((↑a : EReal) + y).exp = (↑a : EReal).exp * y.exp
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
x y : EReal
bot : (⊥ + y).exp = exp ⊥ * y.exp
coe : ∀ (a : ℝ), ((↑a : EReal) + y).exp = (↑a : EReal).exp * y.exp
⊢ (x + y).exp = x.exp * y.exp
have top : (⊤ + y).exp = exp ⊤ * y.exp
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
y : EReal
a : ℝ
⊢ ((↑a : EReal) + y).exp = (↑a : EReal).exp * y.exp
have coe : ((↑a : EReal) + ⊥).exp = (↑a : EReal).exp * exp ⊥
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
y : EReal
a : ℝ
coe : ((↑a : EReal) + ⊥).exp = (↑a : EReal).exp * exp ⊥
⊢ ((↑a : EReal) + y).exp = (↑a : EReal).exp * y.exp
have coe₁ : ∀ (a_1 : ℝ), ((↑a : EReal) + (↑a_1 : EReal)).exp = (↑a : EReal).exp * (↑a_1 : EReal).exp
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
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
⊢ ((↑a : EReal) + y).exp = (↑a : EReal).exp * y.exp
have coe₂ : ((↑a : EReal) + ⊤).exp = (↑a : EReal).exp * exp ⊤
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
a a_1 : ℝ
⊢ ENNReal.ofReal (Real.exp (a + a_1)) = ENNReal.ofReal (Real.exp a) * ENNReal.ofReal (Real.exp a_1)
have coe : ENNReal.ofReal (Real.exp (a + a_1)) = ENNReal.ofReal (Real.exp a * Real.exp a_1)
Tactic: rw [← ENNReal.ofReal_mul (Real.exp_nonneg _), Real.exp_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
a a_1 : ℝ
coe : ENNReal.ofReal (Real.exp (a + 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)
have coe₁ : ENNReal.ofReal (Real.exp a * Real.exp a_1) = ENNReal.ofReal (Real.exp a * Real.exp a_1)
Tactic: rw [← ENNReal.ofReal_mul (Real.exp_nonneg _), Real.exp_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
a : ℝ
⊢ ∞ = ENNReal.ofReal (Real.exp a) * ∞
have coe : ENNReal.ofReal (Real.exp a) ≠ 0
Tactic: rw [ENNReal.mul_top]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
y : EReal
⊢ (⊤ + y).exp = exp ⊤ * y.exp
have top : (HAdd.hAdd (α := EReal) ⊤ ⊥).exp = exp ⊤ * exp ⊥
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
y : EReal
top : (HAdd.hAdd (α := EReal) ⊤ ⊥).exp = exp ⊤ * exp ⊥
⊢ (⊤ + y).exp = exp ⊤ * y.exp
have top₁ : ∀ (a : ℝ), (⊤ + (↑a : EReal)).exp = exp ⊤ * (↑a : EReal).exp
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
y : EReal
top : (HAdd.hAdd (α := EReal) ⊤ ⊥).exp = exp ⊤ * exp ⊥
top₁ : ∀ (a : ℝ), (⊤ + (↑a : EReal)).exp = exp ⊤ * (↑a : EReal).exp
⊢ (⊤ + y).exp = exp ⊤ * y.exp
have top₂ : (HAdd.hAdd (α := EReal) ⊤ ⊤).exp = exp ⊤ * exp ⊤
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ERealExp (goal)
Goal:
a : ℝ
⊢ ∞ = ∞ * ENNReal.ofReal (Real.exp a)
have top : ENNReal.ofReal (Real.exp a) ≠ 0
Tactic: rw [ENNReal.top_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.InvLog (goal)
Goal:
⊢ ¬DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ (log x)⁻¹) 0
have simp : ¬Tendsto (β := ℝ) (fun (t : ℝ) ↦ (log t * t)⁻¹) (nhdsWithin 0 {0}ᶜ) (nhds (deriv (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 _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.InvLog (goal)
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (nhdsWithin 0 (Set.Iio 0)) (nhdsWithin 0 (Set.Ioi 0))
have refine : ∀ᶠ (x : ℝ) in nhdsWithin 0 (Set.Iio 0), Membership.mem (γ := Set ℝ) (Set.Ioi 0) (log x * x)
Tactic: refine tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
      tendsto_log_mul_self_nhdsLT_zero ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.InvLog (goal)
Goal:
⊢ ∀ᶠ (x : ℝ) in nhdsWithin 0 (Set.Iio 0), Membership.mem (γ := Set ℝ) (Set.Ioi 0) (log x * x)
have simp : ∀ᶠ (x : ℝ) in nhdsWithin 0 (Set.Ioo (-1) 0), 0 < log x * x
Tactic: simp only [← nhdsWithin_Ioo_eq_nhdsLT neg_one_lt_zero, Set.mem_Ioi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.InvLog (goal)
Goal:
⊢ ∀ᶠ (x : ℝ) in nhdsWithin 0 (Set.Ioo (-1) 0), 0 < log x * x
have refine : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 0) x → ∀ (hx₁ : -1 < x) (hx₂ : x < 0), log x < 0
Tactic: refine eventually_nhdsWithin_of_forall fun x ⟨hx₁, hx₂⟩ ↦ mul_pos_of_neg_of_neg ?_ hx₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.InvLog (goal)
Goal:
x : ℝ
h : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 0) x
hx₁ : -1 < x
hx₂ : x < 0
⊢ log x < 0
have refine_1 : 0 < -x
Tactic: refine log_neg_eq_log x ▸ log_neg ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.InvLog (goal)
Goal:
x : ℝ
h : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 0) x
hx₁ : -1 < x
hx₂ : x < 0
refine_1 : 0 < -x
⊢ log x < 0
have refine_2 : -x < 1
Tactic: refine log_neg_eq_log x ▸ log_neg ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.InvLog (hypothesis)
Goal:
⊢ ¬Tendsto (β := ℝ) (fun (t : ℝ) ↦ (log t * t)⁻¹) (nhdsWithin 0 {0}ᶜ) (nhds (deriv (fun (x : ℝ) ↦ (log x)⁻¹) 0))
have H' : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.InvLog (goal)
Goal:
⊢ ¬ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ (log x)⁻¹) 1
have suffices : Tendsto (fun (x : ℝ) ↦ (log x)⁻¹) (nhdsWithin 1 {1}ᶜ) (Bornology.cobounded ℝ)
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 _)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.InvLog (hypothesis)
Goal:
⊢ Tendsto (fun (x : ℝ) ↦ (log x)⁻¹) (nhdsWithin 1 {1}ᶜ) (Bornology.cobounded ℝ)
have H : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.InvLog (goal)
Goal:
⊢ ¬ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ (log x)⁻¹) (-1)
have refine : ∀ (H : ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ (log x)⁻¹) (-1)), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ (log x)⁻¹) 1
Tactic: refine fun H ↦ not_continuousAt_inv_log_one ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.InvLog (goal)
Goal:
x : ℝ
⊢ deriv (fun (x : ℝ) ↦ (log x)⁻¹) x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
have inl : deriv (fun (x : ℝ) ↦ (log x)⁻¹) 0 = -0⁻¹ / HPow.hPow (β := ℕ) (log 0) 2
Tactic: rcases eq_or_ne x 0 with rfl | h0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.InvLog (goal)
Goal:
x : ℝ
inl : deriv (fun (x : ℝ) ↦ (log x)⁻¹) 0 = -0⁻¹ / HPow.hPow (β := ℕ) (log 0) 2
⊢ deriv (fun (x : ℝ) ↦ (log x)⁻¹) x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
have inr : ∀ (h0 : x ≠ 0), deriv (fun (x : ℝ) ↦ (log x)⁻¹) x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
Tactic: rcases eq_or_ne x 0 with rfl | h0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.InvLog (goal)
Goal:
x : ℝ
h0 : x ≠ 0
⊢ deriv (fun (x : ℝ) ↦ (log x)⁻¹) x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
have inr : ∀ (h0 : Ne (α := ℝ) 1 0), deriv (fun (x : ℝ) ↦ (log x)⁻¹) 1 = -1⁻¹ / HPow.hPow (β := ℕ) (log 1) 2
Tactic: rcases eq_or_ne x 1 with rfl | h1
Cleared hypotheses: x, h0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.InvLog (goal)
Goal:
x : ℝ
h0 : x ≠ 0
inr : ∀ (h0 : Ne (α := ℝ) 1 0), deriv (fun (x : ℝ) ↦ (log x)⁻¹) 1 = -1⁻¹ / HPow.hPow (β := ℕ) (log 1) 2
⊢ deriv (fun (x : ℝ) ↦ (log x)⁻¹) x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
have inr₁ : ∀ (h1 : x ≠ 1), deriv (fun (x : ℝ) ↦ (log x)⁻¹) x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
Tactic: rcases eq_or_ne x 1 with rfl | h1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.InvLog (goal)
Goal:
x : ℝ
h0 : x ≠ 0
h1 : x ≠ 1
⊢ deriv (fun (x : ℝ) ↦ (log x)⁻¹) x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
have inr : ∀ (h0 : Ne (α := ℝ) (-1) 0) (h1 : Ne (α := ℝ) (-1) 1),
  deriv (fun (x : ℝ) ↦ (log x)⁻¹) (-1) = -(-1)⁻¹ / HPow.hPow (β := ℕ) (log (-1)) 2
Tactic: rcases eq_or_ne x (-1) with rfl | h2
Cleared hypotheses: x, h0, h1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.InvLog (goal)
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
⊢ deriv (fun (x : ℝ) ↦ (log x)⁻¹) x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
have inr₁ : ∀ (h2 : x ≠ -1), deriv (fun (x : ℝ) ↦ (log x)⁻¹) x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
Tactic: rcases eq_or_ne x (-1) with rfl | h2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Monotone (goal)
Goal:
⊢ StrictMonoOn (β := ℝ) (fun (x : ℝ) ↦ x * log x) (Ici (rexp (-1)))
have refine : ∀ (x : ℝ) (hx : x ∈ interior (Ici (rexp (-1)))), LT.lt (α := ℝ) 0 (deriv (fun (x : ℝ) ↦ x * log x) x)
Tactic: refine strictMonoOn_of_deriv_pos (convex_Ici _) continuous_mul_log.continuousOn fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Monotone (hypothesis)
Goal:
x : ℝ
hx : x ∈ interior (Ici (rexp (-1)))
⊢ LT.lt (α := ℝ) 0 (deriv (fun (x : ℝ) ↦ x * log x) x)
have hlt : rexp (-1) < x
Tactic: have hlt : rexp (-1) < x := by simpa using hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Monotone (hypothesis)
Goal:
x : ℝ
hx : x ∈ interior (Ici (rexp (-1)))
hlt : rexp (-1) < x
⊢ LT.lt (α := ℝ) 0 (deriv (fun (x : ℝ) ↦ x * log x) x)
have hpos : 0 < x
Tactic: have hpos : 0 < x := by grind [Real.exp_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Monotone (goal)
Goal:
⊢ StrictAntiOn (β := ℝ) (fun (x : ℝ) ↦ x * log x) (Icc 0 (rexp (-1)))
have refine : ∀ (x : ℝ) (hx : x ∈ interior (Icc 0 (rexp (-1)))), LT.lt (α := ℝ) (deriv (fun (x : ℝ) ↦ x * log x) x) 0
Tactic: refine strictAntiOn_of_deriv_neg (convex_Icc ..) continuous_mul_log.continuousOn fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Monotone (hypothesis)
Goal:
x : ℝ
hx : x ∈ interior (Icc 0 (rexp (-1)))
⊢ LT.lt (α := ℝ) (deriv (fun (x : ℝ) ↦ x * log x) x) 0
have hgt : x < rexp (-1)
Tactic: have hgt : x < rexp (-1) := by simp_all [interior_Icc, mem_Ioo]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Monotone (hypothesis)
Goal:
x : ℝ
hx : x ∈ interior (Icc 0 (rexp (-1)))
hgt : x < rexp (-1)
⊢ LT.lt (α := ℝ) (deriv (fun (x : ℝ) ↦ x * log x) x) 0
have hpos : 0 < x
Tactic: have hpos : 0 < x := by simp_all [interior_Icc, mem_Ioo]
-- 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
⊢ LE.le (α := ℝ) ((fun (x : ℝ) ↦ log x / x) y) ((fun (x : ℝ) ↦ log x / x) x)
have x_pos : 0 < x
Tactic: have x_pos : 0 < x := (exp_pos 1).trans_le hex
-- 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
⊢ LE.le (α := ℝ) ((fun (x : ℝ) ↦ log x / x) y) ((fun (x : ℝ) ↦ log x / x) x)
have y_pos : 0 < y
Tactic: have y_pos : 0 < y := (exp_pos 1).trans_le hey
-- 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
⊢ 1 ≤ log x
have rwa : rexp 1 ≤ x
Tactic: rwa [le_log_iff_exp_le x_pos]
-- 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
⊢ LE.le (α := ℝ) ((fun (x : ℝ) ↦ log x / x) y) ((fun (x : ℝ) ↦ log x / x) x)
have hlogx : 1 ≤ log x
Tactic: have hlogx : 1 ≤ log x := by rwa [le_log_iff_exp_le x_pos]
-- 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
⊢ 0 ≤ y / x - 1
have rwa : HAdd.hAdd (α := ℝ) 0 1 ≤ y / x
Tactic: 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
rwa : HAdd.hAdd (α := ℝ) 0 1 ≤ y / x
⊢ 0 ≤ y / x - 1
have rwa₁ : HAdd.hAdd (α := ℝ) 0 1 * x ≤ y
Tactic: 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
rwa : HAdd.hAdd (α := ℝ) 0 1 ≤ y / x
rwa₁ : HAdd.hAdd (α := ℝ) 0 1 * x ≤ y
⊢ 0 ≤ y / x - 1
have rwa₂ : 1 * x ≤ y
Tactic: rwa [le_sub_iff_add_le, le_div_iff₀ x_pos, zero_add, one_mul]