awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ≥0∞
y : ℝ
y_pos : 0 < y
x_real : 0 < x.toReal
x_ne_zero : x ≠ 0
x_ne_top : x ≠ ∞
⊢ Real.log (x ^ y).toReal = y * Real.log x.toReal

Tactic:
exact ENNReal.toReal_rpow x y ▸ Real.log_rpow x_real y
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ≥0∞
n : ℕ
rw : (HPow.hPow (β := ℝ) x (↑n : ℝ)).log = (↑n : EReal) * x.log
rw₁ : (↑(↑n : ℝ) : EReal) * x.log = (↑n : EReal) * x.log
rw₂ rw₃ : (↑n : EReal) * x.log = (↑n : EReal) * x.log
⊢ (x ^ n).log = (↑n : EReal) * x.log

Tactic:
rw [← rpow_natCast, log_rpow, EReal.coe_natCast]

Premises used: ENNReal.rpow_natCast, EReal.coe_natCast, ENNReal.log_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ≥0∞
⊢ x⁻¹.log = -x.log

Tactic:
simp [← rpow_neg_one, log_rpow]

Premises used: ENNReal.log_rpow, ENNReal.rpow_neg_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
x : EReal
bot : (exp ⊥).log = ⊥
coe : ∀ (a : ℝ), (↑a : EReal).exp.log = (↑a : EReal)
top : (exp ⊤).log = ⊤
⊢ x.exp.log = x

Tactic:
induction x
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
⊢ (exp ⊥).log = ⊥

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
a : ℝ
coe : (ENNReal.ofReal (Real.exp a)).log = (↑a : EReal)
coe₁ : (if Real.exp a ≤ 0 then ⊥ else (↑(Real.log (Real.exp a)) : EReal)) = (↑a : EReal)
coe₂ : (↑(Real.log (Real.exp a)) : EReal) = (↑a : EReal)
coe₃ coe₄ : (↑a : EReal) = (↑a : EReal)
⊢ (↑a : EReal).exp.log = (↑a : EReal)

Tactic:
rw [exp_coe, log_ofReal, if_neg (not_le.mpr (Real.exp_pos _)), Real.log_exp]

Premises used: not_le, Iff.mpr, Real.log_exp, EReal.exp_coe, if_neg, Real.exp_pos, ENNReal.log_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
⊢ (exp ⊤).log = ⊤

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
x : ℝ≥0∞
pos : ∀ (hx_top : x = ∞), x.log.exp = x
neg : ∀ (hx_top : ¬x = ∞), x.log.exp = x
⊢ x.log.exp = x

Tactic:
by_cases hx_top : x = ∞
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
x : ℝ≥0∞
hx_top : x = ∞
⊢ x.log.exp = x

Tactic:
simp [hx_top]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
x : ℝ≥0∞
hx_top : ¬x = ∞
pos : ∀ (hx_zero : x = 0), x.log.exp = x
neg : ∀ (hx_zero : ¬x = 0), x.log.exp = x
⊢ x.log.exp = x

Tactic:
by_cases hx_zero : x = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
x : ℝ≥0∞
hx_top : ¬x = ∞
hx_zero : x = 0
⊢ x.log.exp = x

Tactic:
simp [hx_zero]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
x : ℝ≥0∞
hx_top : ¬x = ∞
hx_zero : ¬x = 0
⊢ 0 < x.toReal

Tactic:
have hx_pos : 0 < x.toReal := ENNReal.toReal_pos hx_zero hx_top
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
x : ℝ≥0∞
hx_top : ¬x = ∞
hx_zero : ¬x = 0
hx_pos : 0 < x.toReal
neg : (ENNReal.ofReal x.toReal).log.exp = ENNReal.ofReal x.toReal
neg₁ : (↑(Real.log x.toReal) : EReal).exp = ENNReal.ofReal x.toReal
neg₂ : ENNReal.ofReal (Real.exp (Real.log x.toReal)) = ENNReal.ofReal x.toReal
neg₃ neg₄ : ENNReal.ofReal x.toReal = ENNReal.ofReal x.toReal
⊢ x.log.exp = x

Tactic:
rw [← ENNReal.ofReal_toReal hx_top, log_ofReal_of_pos hx_pos, exp_coe, Real.exp_log hx_pos]

Premises used: ENNReal.ofReal_toReal, EReal.exp_coe, Real.exp_log, ENNReal.log_ofReal_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
x : EReal
n : ℕ
simp_rw : ((↑n : EReal) * x).exp.log = (x.exp ^ n).log
simp_rw₁ : ((↑n : EReal) * x).exp.log = (↑n : EReal) * x.exp.log
⊢ ((↑n : EReal) * x).exp = x.exp ^ n

Tactic:
simp_rw [← log_eq_iff, log_pow, log_exp]

Premises used: ENNReal.log_eq_iff, ENNReal.log_pow, EReal.log_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
x : EReal
y : ℝ
rw : (x * (↑y : EReal)).exp.log = (x.exp ^ y).log
rw₁ : (x * (↑y : EReal)).exp.log = (↑y : EReal) * x.exp.log
rw₂ : x * (↑y : EReal) = (↑y : EReal) * x.exp.log
rw₃ : x * (↑y : EReal) = (↑y : EReal) * x
rw₄ rw₅ : (↑y : EReal) * x = (↑y : EReal) * x
⊢ (x * (↑y : EReal)).exp = x.exp ^ y

Tactic:
rw [← log_eq_iff, log_rpow, log_exp, log_exp, mul_comm]

Premises used: ENNReal.log_eq_iff, ENNReal.log_rpow, mul_comm, EReal.log_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
x : ℝ≥0∞
y : ℝ
rw : x ^ y = (x.log * (↑y : EReal)).exp
rw₁ : x ^ y = x.log.exp ^ y
rw₂ rw₃ : x ^ y = x ^ y
⊢ x ^ y = ((↑y : EReal) * x.log).exp

Tactic:
rw [mul_comm, EReal.exp_mul, exp_log]

Premises used: ENNReal.exp_log, EReal.exp_mul, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
⊢ ∀ {a b : ℝ≥0∞},
    LE.le (α := EReal)
        (({ toFun := log, invFun := exp, left_inv := ⋯, right_inv := ⋯ : ℝ≥0∞ ≃ EReal } : (a : ℝ≥0∞) → EReal) a : EReal)
        (({ toFun := log, invFun := exp, left_inv := ⋯, right_inv := ⋯ : ℝ≥0∞ ≃ EReal } : (a : ℝ≥0∞) → EReal) b :
          EReal) ↔
      a ≤ b

Tactic:
simp only [Equiv.coe_fn_mk, log_le_log_iff, forall_const]

Premises used: ENNReal.log_le_log_iff, Equiv.coe_fn_mk, forall_const
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
x : ℝ≥0∞
⊢ (logOrderIso : (a : ℝ≥0∞) → EReal) x = x.log

Tactic:
rfl

Premises used: ENNReal.log, rfl, ite
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
x : EReal
⊢ (expOrderIso : (a : EReal) → ℝ≥0∞) x = x.exp

Tactic:
rfl

Premises used: EReal.exp, EReal.rec, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
⊢ logOrderIso.symm = expOrderIso

Tactic:
rfl

Premises used: rfl, EReal.expOrderIso
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
⊢ expOrderIso.symm = logOrderIso

Tactic:
rfl

Premises used: ENNReal.log, RelIso.symm, OrderIso.symm, ENNReal.logOrderIso, EReal.exp, EReal.rec, Equiv.symm, rfl, ite
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
x : ℝ≥0∞
⊢ (logHomeomorph : (a : ℝ≥0∞) → EReal) x = x.log

Tactic:
rfl

Premises used: ENNReal.log, rfl, ite
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
x : EReal
⊢ (expHomeomorph : (a : EReal) → ℝ≥0∞) x = x.exp

Tactic:
rfl

Premises used: EReal.exp, EReal.rec, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
⊢ logHomeomorph.symm = expHomeomorph

Tactic:
rfl

Premises used: ENNReal.log, HomeomorphClass.toHomeomorph, EReal.exp, Homeomorph.symm, EReal.rec, Equiv.symm, EReal.expHomeomorph, EquivLike.toEquiv, rfl, ite
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
⊢ expHomeomorph.symm = logHomeomorph

Tactic:
rfl

Premises used: ENNReal.log, HomeomorphClass.toHomeomorph, EReal.exp, Homeomorph.symm, ENNReal.logHomeomorph, EReal.rec, Equiv.symm, EquivLike.toEquiv, rfl, ite
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
⊢ Continuous log

Tactic:
logOrderIso.continuous

Premises used: OrderIso.continuous, ENNReal.log, ENNReal.logOrderIso, ite
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
⊢ Continuous exp

Tactic:
expOrderIso.continuous

Premises used: OrderIso.continuous, EReal.exp, EReal.rec, EReal.expOrderIso
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
⊢ Filter.Tendsto exp (𝓝 ⊤) (𝓝 ∞)

Tactic:
continuous_exp.tendsto ⊤

Premises used: Continuous.tendsto, EReal.exp, ENNReal.continuous_exp, EReal.rec, Top.top
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
⊢ Filter.Tendsto exp (𝓝 0) (𝓝 (exp 0))

Tactic:
continuous_exp.tendsto 0

Premises used: Continuous.tendsto, ENNReal.continuous_exp, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
h : 1 = exp 0
⊢ Filter.Tendsto exp (𝓝 0) (𝓝 1)

Tactic:
convert! continuous_exp.tendsto 0

Premises used: Continuous.tendsto, ENNReal.continuous_exp, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
⊢ 1 = exp 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
⊢ Filter.Tendsto exp (𝓝 ⊥) (𝓝 0)

Tactic:
continuous_exp.tendsto ⊥

Premises used: Bot.bot, Continuous.tendsto, EReal.exp, ENNReal.continuous_exp, EReal.rec
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : 1 < b
simp_rw : Filter.Tendsto (β := ℝ≥0∞) (fun (x : ℝ) ↦ ((↑x : EReal) * b.log).exp) Filter.atTop (𝓝 ∞)
⊢ Filter.Tendsto (β := ℝ≥0∞) (fun (x : ℝ) ↦ b ^ x) Filter.atTop (𝓝 ∞)

Tactic:
simp_rw [ENNReal.rpow_eq_exp_mul_log]

Premises used: EReal.ENNReal.rpow_eq_exp_mul_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : 1 < b
⊢ Filter.Tendsto (β := ℝ≥0∞) (fun (x : ℝ) ↦ ((↑x : EReal) * b.log).exp) Filter.atTop (𝓝 ∞)

Tactic:
EReal.tendsto_exp_nhds_top_nhds_top.comp ?_

Premises used: EReal.tendsto_exp_nhds_top_nhds_top, EReal.exp, EReal.rec, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : 1 < b
refine : Filter.Tendsto (β := EReal) (fun (x : ℝ) ↦ (↑x : EReal) * b.log) Filter.atTop (𝓝 ⊤)
⊢ Filter.Tendsto (β := ℝ≥0∞) (fun (x : ℝ) ↦ ((↑x : EReal) * b.log).exp) Filter.atTop (𝓝 ∞)

Tactic:
refine EReal.tendsto_exp_nhds_top_nhds_top.comp ?_

Premises used: EReal.tendsto_exp_nhds_top_nhds_top, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : 1 < b
⊢ Filter.Tendsto (fun (x : ℝ) ↦ (↑x : EReal) * b.log) Filter.atTop (𝓝 (⊤ * b.log))

Tactic:
EReal.Tendsto.mul_const tendsto_coe_atTop _ _

Premises used: EReal.tendsto_coe_atTop, EReal.Tendsto.mul_const
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : 1 < b
h : ⊤ = ⊤ * b.log
convert_2 : Ne (α := EReal) ⊤ 0 ∨ b.log ≠ ⊥
convert_3 : Ne (α := EReal) ⊤ 0 ∨ b.log ≠ ⊤
⊢ Filter.Tendsto (β := EReal) (fun (x : ℝ) ↦ (↑x : EReal) * b.log) Filter.atTop (𝓝 ⊤)

Tactic:
convert! EReal.Tendsto.mul_const tendsto_coe_atTop _ _

Premises used: EReal.tendsto_coe_atTop, EReal.Tendsto.mul_const
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : 1 < b
h h₁ : Eq (α := EReal) ⊤ ⊤
⊢ ⊤ = ⊤ * b.log

Tactic:
rw [EReal.top_mul_of_pos (zero_lt_log_iff.2 hb)]

Premises used: Iff.mpr, EReal.top_mul_of_pos, ENNReal.zero_lt_log_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : 1 < b
⊢ Ne (α := EReal) ⊤ 0 ∨ b.log ≠ ⊥

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : 1 < b
⊢ Ne (α := EReal) ⊤ 0 ∨ b.log ≠ ⊤

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : b < 1
simp_rw : Filter.Tendsto (β := ℝ≥0∞) (fun (x : ℝ) ↦ ((↑x : EReal) * b.log).exp) Filter.atTop (𝓝 0)
⊢ Filter.Tendsto (β := ℝ≥0∞) (fun (x : ℝ) ↦ b ^ x) Filter.atTop (𝓝 0)

Tactic:
simp_rw [ENNReal.rpow_eq_exp_mul_log]

Premises used: EReal.ENNReal.rpow_eq_exp_mul_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : b < 1
⊢ Filter.Tendsto (β := ℝ≥0∞) (fun (x : ℝ) ↦ ((↑x : EReal) * b.log).exp) Filter.atTop (𝓝 0)

Tactic:
EReal.tendsto_exp_nhds_bot_nhds_zero.comp ?_

Premises used: EReal.tendsto_exp_nhds_bot_nhds_zero, EReal.exp, EReal.rec, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : b < 1
refine : Filter.Tendsto (β := EReal) (fun (x : ℝ) ↦ (↑x : EReal) * b.log) Filter.atTop (𝓝 ⊥)
⊢ Filter.Tendsto (β := ℝ≥0∞) (fun (x : ℝ) ↦ ((↑x : EReal) * b.log).exp) Filter.atTop (𝓝 0)

Tactic:
refine EReal.tendsto_exp_nhds_bot_nhds_zero.comp ?_

Premises used: EReal.tendsto_exp_nhds_bot_nhds_zero, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : b < 1
⊢ Filter.Tendsto (fun (x : ℝ) ↦ (↑x : EReal) * b.log) Filter.atTop (𝓝 (⊤ * b.log))

Tactic:
EReal.Tendsto.mul_const tendsto_coe_atTop _ _

Premises used: EReal.tendsto_coe_atTop, EReal.Tendsto.mul_const
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : b < 1
h : ⊥ = ⊤ * b.log
convert_2 : Ne (α := EReal) ⊤ 0 ∨ b.log ≠ ⊥
convert_3 : Ne (α := EReal) ⊤ 0 ∨ b.log ≠ ⊤
⊢ Filter.Tendsto (β := EReal) (fun (x : ℝ) ↦ (↑x : EReal) * b.log) Filter.atTop (𝓝 ⊥)

Tactic:
convert! EReal.Tendsto.mul_const tendsto_coe_atTop _ _

Premises used: EReal.tendsto_coe_atTop, EReal.Tendsto.mul_const
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : b < 1
h h₁ : Eq (α := EReal) ⊥ ⊥
⊢ ⊥ = ⊤ * b.log

Tactic:
rw [EReal.top_mul_of_neg (log_lt_zero_iff.2 hb)]

Premises used: Iff.mpr, ENNReal.log_lt_zero_iff, EReal.top_mul_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : b < 1
⊢ Ne (α := EReal) ⊤ 0 ∨ b.log ≠ ⊥

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : b < 1
⊢ Ne (α := EReal) ⊤ 0 ∨ b.log ≠ ⊤

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : 1 < b
simp_rw : Filter.Tendsto (β := ℝ≥0∞) (fun (x : ℝ) ↦ ((↑x : EReal) * b.log).exp) Filter.atBot (𝓝 0)
⊢ Filter.Tendsto (β := ℝ≥0∞) (fun (x : ℝ) ↦ b ^ x) Filter.atBot (𝓝 0)

Tactic:
simp_rw [ENNReal.rpow_eq_exp_mul_log]

Premises used: EReal.ENNReal.rpow_eq_exp_mul_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : 1 < b
⊢ Filter.Tendsto (β := ℝ≥0∞) (fun (x : ℝ) ↦ ((↑x : EReal) * b.log).exp) Filter.atBot (𝓝 0)

Tactic:
EReal.tendsto_exp_nhds_bot_nhds_zero.comp ?_

Premises used: EReal.tendsto_exp_nhds_bot_nhds_zero, EReal.exp, EReal.rec, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : 1 < b
refine : Filter.Tendsto (β := EReal) (fun (x : ℝ) ↦ (↑x : EReal) * b.log) Filter.atBot (𝓝 ⊥)
⊢ Filter.Tendsto (β := ℝ≥0∞) (fun (x : ℝ) ↦ ((↑x : EReal) * b.log).exp) Filter.atBot (𝓝 0)

Tactic:
refine EReal.tendsto_exp_nhds_bot_nhds_zero.comp ?_

Premises used: EReal.tendsto_exp_nhds_bot_nhds_zero, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : 1 < b
⊢ Filter.Tendsto (fun (x : ℝ) ↦ (↑x : EReal) * b.log) Filter.atBot (𝓝 (⊥ * b.log))

Tactic:
EReal.Tendsto.mul_const tendsto_coe_atBot _ _

Premises used: EReal.Tendsto.mul_const, EReal.tendsto_coe_atBot
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : 1 < b
h : ⊥ = ⊥ * b.log
convert_2 : Ne (α := EReal) ⊥ 0 ∨ b.log ≠ ⊥
convert_3 : Ne (α := EReal) ⊥ 0 ∨ b.log ≠ ⊤
⊢ Filter.Tendsto (β := EReal) (fun (x : ℝ) ↦ (↑x : EReal) * b.log) Filter.atBot (𝓝 ⊥)

Tactic:
convert! EReal.Tendsto.mul_const tendsto_coe_atBot _ _

Premises used: EReal.Tendsto.mul_const, EReal.tendsto_coe_atBot
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : 1 < b
h h₁ : Eq (α := EReal) ⊥ ⊥
⊢ ⊥ = ⊥ * b.log

Tactic:
rw [EReal.bot_mul_of_pos (zero_lt_log_iff.2 hb)]

Premises used: Iff.mpr, ENNReal.zero_lt_log_iff, EReal.bot_mul_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : 1 < b
⊢ Ne (α := EReal) ⊥ 0 ∨ b.log ≠ ⊥

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : 1 < b
⊢ Ne (α := EReal) ⊥ 0 ∨ b.log ≠ ⊤

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : b < 1
simp_rw : Filter.Tendsto (β := ℝ≥0∞) (fun (x : ℝ) ↦ ((↑x : EReal) * b.log).exp) Filter.atBot (𝓝 ∞)
⊢ Filter.Tendsto (β := ℝ≥0∞) (fun (x : ℝ) ↦ b ^ x) Filter.atBot (𝓝 ∞)

Tactic:
simp_rw [ENNReal.rpow_eq_exp_mul_log]

Premises used: EReal.ENNReal.rpow_eq_exp_mul_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : b < 1
⊢ Filter.Tendsto (β := ℝ≥0∞) (fun (x : ℝ) ↦ ((↑x : EReal) * b.log).exp) Filter.atBot (𝓝 ∞)

Tactic:
EReal.tendsto_exp_nhds_top_nhds_top.comp ?_

Premises used: EReal.tendsto_exp_nhds_top_nhds_top, EReal.exp, EReal.rec, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : b < 1
refine : Filter.Tendsto (β := EReal) (fun (x : ℝ) ↦ (↑x : EReal) * b.log) Filter.atBot (𝓝 ⊤)
⊢ Filter.Tendsto (β := ℝ≥0∞) (fun (x : ℝ) ↦ ((↑x : EReal) * b.log).exp) Filter.atBot (𝓝 ∞)

Tactic:
refine EReal.tendsto_exp_nhds_top_nhds_top.comp ?_

Premises used: EReal.tendsto_exp_nhds_top_nhds_top, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : b < 1
⊢ Filter.Tendsto (fun (x : ℝ) ↦ (↑x : EReal) * b.log) Filter.atBot (𝓝 (⊥ * b.log))

Tactic:
EReal.Tendsto.mul_const tendsto_coe_atBot _ _

Premises used: EReal.Tendsto.mul_const, EReal.tendsto_coe_atBot
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : b < 1
h : ⊤ = ⊥ * b.log
convert_2 : Ne (α := EReal) ⊥ 0 ∨ b.log ≠ ⊥
convert_3 : Ne (α := EReal) ⊥ 0 ∨ b.log ≠ ⊤
⊢ Filter.Tendsto (β := EReal) (fun (x : ℝ) ↦ (↑x : EReal) * b.log) Filter.atBot (𝓝 ⊤)

Tactic:
convert! EReal.Tendsto.mul_const tendsto_coe_atBot _ _

Premises used: EReal.Tendsto.mul_const, EReal.tendsto_coe_atBot
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : b < 1
h h₁ : Eq (α := EReal) ⊤ ⊤
⊢ ⊤ = ⊥ * b.log

Tactic:
rw [EReal.bot_mul_of_neg (log_lt_zero_iff.2 hb)]

Premises used: Iff.mpr, ENNReal.log_lt_zero_iff, EReal.bot_mul_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : b < 1
⊢ Ne (α := EReal) ⊥ 0 ∨ b.log ≠ ⊥

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
b : ℝ≥0∞
hb : b < 1
⊢ Ne (α := EReal) ⊥ 0 ∨ b.log ≠ ⊤

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
⊢ Measurable log

Tactic:
continuous_log.measurable

Premises used: ENNReal.continuous_log, Continuous.measurable
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
⊢ Measurable exp

Tactic:
continuous_exp.measurable

Premises used: ENNReal.continuous_exp, Continuous.measurable
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ Measurable (β := EReal) fun (x : α) ↦ (f x).log

Tactic:
measurable_log.comp hf

Premises used: Measurable.comp, ENNReal.log, ENNReal.measurable_log, ite
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → EReal
hf : Measurable f
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ (f x).exp

Tactic:
measurable_exp.comp hf

Premises used: EReal.measurable_exp, Measurable.comp, EReal.exp, EReal.rec
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Goal:
⊢ PolishSpace EReal

Tactic:
ENNReal.logOrderIso.symm.toHomeomorph.isClosedEmbedding.polishSpace

Premises used: OrderIso.symm, ENNReal.logOrderIso, OrderIso.toHomeomorph, Topology.IsClosedEmbedding.polishSpace, Homeomorph.isClosedEmbedding
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
⊢ exp ⊥ = 0

Tactic:
rfl

Premises used: EReal.exp, EReal.rec, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
⊢ exp 0 = 1

Tactic:
simp [exp, ← coe_zero]

Premises used: EReal.coe_zero, EReal.exp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
⊢ exp ⊤ = ∞

Tactic:
rfl

Premises used: EReal.exp, EReal.rec, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
x : ℝ
⊢ (↑x : EReal).exp = ENNReal.ofReal (Real.exp x)

Tactic:
rfl

Premises used: ENNReal.ofReal, EReal.exp, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
x : EReal
bot : exp ⊥ = 0 ↔ Eq (α := EReal) ⊥ ⊥
coe : ∀ (a : ℝ), (↑a : EReal).exp = 0 ↔ (↑a : EReal) = ⊥
top : exp ⊤ = 0 ↔ Eq (α := EReal) ⊤ ⊥
⊢ x.exp = 0 ↔ x = ⊥

Tactic:
induction x
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
⊢ exp ⊥ = 0 ↔ Eq (α := EReal) ⊥ ⊥

Tactic:
simp [Real.exp_pos]

Premises used: Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
a : ℝ
⊢ (↑a : EReal).exp = 0 ↔ (↑a : EReal) = ⊥

Tactic:
simp [Real.exp_pos]

Premises used: Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
⊢ exp ⊤ = 0 ↔ Eq (α := EReal) ⊤ ⊥

Tactic:
simp [Real.exp_pos]

Premises used: Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
x : EReal
bot : exp ⊥ = ∞ ↔ Eq (α := EReal) ⊥ ⊤
coe : ∀ (a : ℝ), (↑a : EReal).exp = ∞ ↔ (↑a : EReal) = ⊤
top : exp ⊤ = ∞ ↔ Eq (α := EReal) ⊤ ⊤
⊢ x.exp = ∞ ↔ x = ⊤

Tactic:
induction x
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
⊢ exp ⊥ = ∞ ↔ Eq (α := EReal) ⊥ ⊤

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
a : ℝ
⊢ (↑a : EReal).exp = ∞ ↔ (↑a : EReal) = ⊤

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
⊢ exp ⊤ = ∞ ↔ Eq (α := EReal) ⊤ ⊤

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

Tactic:
induction x
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
y : EReal
h : ⊥ < y
bot : ¬y = ⊥
⊢ exp ⊥ < y.exp

Tactic:
rw [exp_bot, pos_iff_ne_zero, ne_eq, exp_eq_zero_iff]

Premises used: EReal.exp_bot, ne_eq, EReal.exp_eq_zero_iff, pos_iff_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
y : EReal
h : ⊥ < y
⊢ ¬y = ⊥

Tactic:
h.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
y : EReal
h : ⊥ < y
⊢ ¬y = ⊥

Tactic:
exact h.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
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
coe₂ : ∀ (h : (↑a : EReal) < ⊤), (↑a : EReal).exp < exp ⊤
⊢ (↑a : EReal).exp < y.exp

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

Tactic:
simp at h
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
a a_1 : ℝ
h : (↑a : EReal) < (↑a_1 : EReal)
⊢ ENNReal.ofReal (Real.exp a) < ENNReal.ofReal (Real.exp a_1)

Tactic:
ENNReal.ofReal_lt_ofReal_iff'.mpr ⟨Real.exp_strictMono (mod_cast h), Real.exp_pos _⟩

Premises used: Iff.mpr, cast, EReal.coe_lt_coe_iff._simp_1, Real.exp_strictMono, And.intro, ENNReal.ofReal_lt_ofReal_iff', Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
a a_1 : ℝ
h : (↑a : EReal) < (↑a_1 : EReal)
⊢ ENNReal.ofReal (Real.exp a) < ENNReal.ofReal (Real.exp a_1)

Tactic:
exact ENNReal.ofReal_lt_ofReal_iff'.mpr ⟨Real.exp_strictMono (mod_cast h), Real.exp_pos _⟩

Premises used: Iff.mpr, Real.exp_strictMono, And.intro, ENNReal.ofReal_lt_ofReal_iff', Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
a : ℝ
h : (↑a : EReal) < ⊤
⊢ (↑a : EReal).exp < exp ⊤

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
y : EReal
h : ⊤ < y
⊢ exp ⊤ < y.exp

Tactic:
(not_top_lt h).elim

Premises used: False.elim, not_top_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
y : EReal
h : ⊤ < y
⊢ exp ⊤ < y.exp

Tactic:
exact (not_top_lt h).elim

Premises used: False.elim, not_top_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
⊢ Monotone exp

Tactic:
exp_strictMono.monotone

Premises used: EReal.exp_strictMono, StrictMono.monotone
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
a b : EReal
⊢ a.exp < b.exp ↔ a < b

Tactic:
exp_strictMono.lt_iff_lt

Premises used: EReal.exp_strictMono, StrictMono.lt_iff_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
a : EReal
⊢ 0 < a.exp ↔ ⊥ < a

Tactic:
exp_bot ▸ @exp_lt_exp_iff ⊥ a

Premises used: EReal.exp_bot, Eq.rec, EReal.exp_lt_exp_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
a : EReal
⊢ a.exp < ∞ ↔ a < ⊤

Tactic:
exp_top ▸ @exp_lt_exp_iff a ⊤

Premises used: Eq.rec, EReal.exp_lt_exp_iff, EReal.exp_top
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp
Goal:
a : EReal
⊢ a.exp < 1 ↔ a < 0

Tactic:
exp_zero ▸ @exp_lt_exp_iff a 0

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

Tactic:
exp_zero ▸ @exp_lt_exp_iff 0 a

Premises used: Eq.rec, EReal.exp_lt_exp_iff, EReal.exp_zero