awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
y : ℝ≥0∞
y_real : 0 < y.toReal
⊢ Eq (α := ℝ≥0∞) (if y = 0 then 0 else ∞) ∞
have inr : ¬y = 0
Tactic: simp only [ite_eq_right_iff, zero_ne_top, imp_false]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x y : ℝ≥0∞
x_real : 0 < x.toReal
⊢ (x * y).log = x.log + y.log
have inr : (x * y).log = (↑(Real.log x.toReal) : EReal) + y.log
Tactic: rw [log_pos_real' x_real]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x y : ℝ≥0∞
x_real : 0 < x.toReal
⊢ (x * y).log = (↑(Real.log x.toReal) : EReal) + y.log
have inr : (x * 0).log = (↑(Real.log x.toReal) : EReal) + log 0
Tactic: rcases ENNReal.trichotomy y with (rfl | rfl | y_real)
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x y : ℝ≥0∞
x_real : 0 < x.toReal
inr : (x * 0).log = (↑(Real.log x.toReal) : EReal) + log 0
⊢ (x * y).log = (↑(Real.log x.toReal) : EReal) + y.log
have inr₁ : (x * ∞).log = (↑(Real.log x.toReal) : EReal) + log ∞
Tactic: rcases ENNReal.trichotomy y with (rfl | rfl | y_real)
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x y : ℝ≥0∞
x_real : 0 < x.toReal
inr : (x * 0).log = (↑(Real.log x.toReal) : EReal) + log 0
inr₁ : (x * ∞).log = (↑(Real.log x.toReal) : EReal) + log ∞
⊢ (x * y).log = (↑(Real.log x.toReal) : EReal) + y.log
have inr₂ : ∀ (y_real : 0 < y.toReal), (x * y).log = (↑(Real.log x.toReal) : EReal) + y.log
Tactic: rcases ENNReal.trichotomy y with (rfl | rfl | y_real)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x y : ℝ≥0∞
x_real : 0 < x.toReal
y_real : 0 < y.toReal
⊢ (x * y).log = (↑(Real.log x.toReal) : EReal) + y.log
have inr : ∀ (x_real : 0 < x.toReal) (y_real : 0 < y.toReal),
  Real.log (x.toReal * y.toReal) = Real.log x.toReal + Real.log y.toReal
Tactic: rw_mod_cast [log_pos_real', log_pos_real' y_real, ENNReal.toReal_mul]
Cleared hypotheses: x_real, y_real
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x y : ℝ≥0∞
x_real : 0 < x.toReal
y_real : 0 < y.toReal
inr :
  ∀ (x_real : 0 < x.toReal) (y_real : 0 < y.toReal),
    Real.log (x.toReal * y.toReal) = Real.log x.toReal + Real.log y.toReal
⊢ (x * y).log = (↑(Real.log x.toReal) : EReal) + y.log
have inr₁ : ∀ (x_real : 0 < x.toReal) (y_real : 0 < y.toReal), 0 < (x * y).toReal
Tactic: rw_mod_cast [log_pos_real', log_pos_real' y_real, ENNReal.toReal_mul]
Cleared hypotheses: x_real, y_real
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x y : ℝ≥0∞
x_real : 0 < x.toReal
y_real : 0 < y.toReal
⊢ 0 < (x * y).toReal
have inr : 0 < x.toReal * y.toReal
Tactic: rw [toReal_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x : ℝ≥0∞
y : ℝ
⊢ (x ^ y).log = (↑y : EReal) * x.log
have inl : ∀ (y_neg : y < 0), (x ^ y).log = (↑y : EReal) * x.log
Tactic: rcases lt_trichotomy y 0 with (y_neg | rfl | y_pos)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x : ℝ≥0∞
y : ℝ
inl : ∀ (y_neg : y < 0), (x ^ y).log = (↑y : EReal) * x.log
⊢ (x ^ y).log = (↑y : EReal) * x.log
have inr : (HPow.hPow (β := ℝ) x 0).log = (↑0 : EReal) * x.log
Tactic: rcases lt_trichotomy y 0 with (y_neg | rfl | y_pos)
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x : ℝ≥0∞
y : ℝ
inl : ∀ (y_neg : y < 0), (x ^ y).log = (↑y : EReal) * x.log
inr : (HPow.hPow (β := ℝ) x 0).log = (↑0 : EReal) * x.log
⊢ (x ^ y).log = (↑y : EReal) * x.log
have inr₁ : ∀ (y_pos : 0 < y), (x ^ y).log = (↑y : EReal) * x.log
Tactic: rcases lt_trichotomy y 0 with (y_neg | rfl | y_pos)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x : ℝ≥0∞
y : ℝ
y_neg : y < 0
⊢ (x ^ y).log = (↑y : EReal) * x.log
have inl : (HPow.hPow (α := ℝ≥0∞) 0 y).log = (↑y : EReal) * log 0
Tactic: rcases ENNReal.trichotomy x with (rfl | rfl | x_real)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x : ℝ≥0∞
y : ℝ
y_neg : y < 0
inl : (HPow.hPow (α := ℝ≥0∞) 0 y).log = (↑y : EReal) * log 0
⊢ (x ^ y).log = (↑y : EReal) * x.log
have inl₁ : (HPow.hPow (α := ℝ≥0∞) ∞ y).log = (↑y : EReal) * log ∞
Tactic: rcases ENNReal.trichotomy x with (rfl | rfl | x_real)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x : ℝ≥0∞
y : ℝ
y_neg : y < 0
inl : (HPow.hPow (α := ℝ≥0∞) 0 y).log = (↑y : EReal) * log 0
inl₁ : (HPow.hPow (α := ℝ≥0∞) ∞ y).log = (↑y : EReal) * log ∞
⊢ (x ^ y).log = (↑y : EReal) * x.log
have inl₂ : ∀ (x_real : 0 < x.toReal), (x ^ y).log = (↑y : EReal) * x.log
Tactic: rcases ENNReal.trichotomy x with (rfl | rfl | x_real)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
y : ℝ
y_neg : y < 0
⊢ (HPow.hPow (α := ℝ≥0∞) ∞ y).log = (↑y : EReal) * log ∞
have inl : log 0 = (↑y : EReal) * log ∞
Tactic: rw [ENNReal.top_rpow_of_neg y_neg, log_zero, log_top, EReal.coe_mul_top_of_neg y_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
y : ℝ
y_neg : y < 0
inl : log 0 = (↑y : EReal) * log ∞
⊢ (HPow.hPow (α := ℝ≥0∞) ∞ y).log = (↑y : EReal) * log ∞
have inl₁ : ⊥ = (↑y : EReal) * log ∞
Tactic: rw [ENNReal.top_rpow_of_neg y_neg, log_zero, log_top, EReal.coe_mul_top_of_neg y_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
y : ℝ
y_neg : y < 0
inl : log 0 = (↑y : EReal) * log ∞
inl₁ : ⊥ = (↑y : EReal) * log ∞
⊢ (HPow.hPow (α := ℝ≥0∞) ∞ y).log = (↑y : EReal) * log ∞
have inl₂ : ⊥ = (↑y : EReal) * ⊤
Tactic: rw [ENNReal.top_rpow_of_neg y_neg, log_zero, log_top, EReal.coe_mul_top_of_neg y_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
y : ℝ
y_neg : y < 0
inl : log 0 = (↑y : EReal) * log ∞
inl₁ : ⊥ = (↑y : EReal) * log ∞
inl₂ : ⊥ = (↑y : EReal) * ⊤
⊢ (HPow.hPow (α := ℝ≥0∞) ∞ y).log = (↑y : EReal) * log ∞
have inl₃ : Eq (α := EReal) ⊥ ⊥
Tactic: rw [ENNReal.top_rpow_of_neg y_neg, log_zero, log_top, EReal.coe_mul_top_of_neg y_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (hypothesis)
Goal:
x : ℝ≥0∞
y : ℝ
y_neg : y < 0
x_real : 0 < x.toReal
⊢ (x ^ y).log = (↑y : EReal) * x.log
have x_ne_zero : x ≠ 0
Tactic: have x_ne_zero := (ENNReal.toReal_pos_iff.1 x_real).1.ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (hypothesis)
Goal:
x : ℝ≥0∞
y : ℝ
y_neg : y < 0
x_real : 0 < x.toReal
x_ne_zero : x ≠ 0
⊢ (x ^ y).log = (↑y : EReal) * x.log
have x_ne_top : x ≠ ∞
Tactic: have x_ne_top := (ENNReal.toReal_pos_iff.1 x_real).2.ne
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x : ℝ≥0∞
y : ℝ
y_neg : y < 0
x_real : 0 < x.toReal
x_ne_zero : x ≠ 0
x_ne_top : x ≠ ∞
⊢ (x ^ y).log = (↑y : EReal) * x.log
have inl : (↑(Real.log (x ^ y).toReal) : EReal) = (↑y : EReal) * (↑(Real.log x.toReal) : EReal)
Tactic: simp only [log, rpow_eq_zero_iff, x_ne_zero, false_and, x_ne_top, or_self, ↓reduceIte,
        rpow_eq_top_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x : ℝ≥0∞
y : ℝ
y_neg : y < 0
x_real : 0 < x.toReal
x_ne_zero : x ≠ 0
x_ne_top : x ≠ ∞
⊢ (↑(Real.log (x ^ y).toReal) : EReal) = (↑y : EReal) * (↑(Real.log x.toReal) : EReal)
have inl : Real.log (x ^ y).toReal = y * Real.log x.toReal
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x : ℝ≥0∞
y : ℝ
y_pos : 0 < y
⊢ (x ^ y).log = (↑y : EReal) * x.log
have inr : (HPow.hPow (α := ℝ≥0∞) 0 y).log = (↑y : EReal) * log 0
Tactic: rcases ENNReal.trichotomy x with (rfl | rfl | x_real)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x : ℝ≥0∞
y : ℝ
y_pos : 0 < y
inr : (HPow.hPow (α := ℝ≥0∞) 0 y).log = (↑y : EReal) * log 0
⊢ (x ^ y).log = (↑y : EReal) * x.log
have inr₁ : (HPow.hPow (α := ℝ≥0∞) ∞ y).log = (↑y : EReal) * log ∞
Tactic: rcases ENNReal.trichotomy x with (rfl | rfl | x_real)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x : ℝ≥0∞
y : ℝ
y_pos : 0 < y
inr : (HPow.hPow (α := ℝ≥0∞) 0 y).log = (↑y : EReal) * log 0
inr₁ : (HPow.hPow (α := ℝ≥0∞) ∞ y).log = (↑y : EReal) * log ∞
⊢ (x ^ y).log = (↑y : EReal) * x.log
have inr₂ : ∀ (x_real : 0 < x.toReal), (x ^ y).log = (↑y : EReal) * x.log
Tactic: rcases ENNReal.trichotomy x with (rfl | rfl | x_real)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
y : ℝ
y_pos : 0 < y
⊢ (HPow.hPow (α := ℝ≥0∞) 0 y).log = (↑y : EReal) * log 0
have inr : 0 < (↑y : EReal)
Tactic: rw [ENNReal.zero_rpow_of_pos y_pos, log_zero, EReal.mul_bot_of_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
y : ℝ
y_pos : 0 < y
⊢ (HPow.hPow (α := ℝ≥0∞) ∞ y).log = (↑y : EReal) * log ∞
have inr : 0 < (↑y : EReal)
Tactic: rw [ENNReal.top_rpow_of_pos y_pos, log_top, EReal.mul_top_of_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (hypothesis)
Goal:
x : ℝ≥0∞
y : ℝ
y_pos : 0 < y
x_real : 0 < x.toReal
⊢ (x ^ y).log = (↑y : EReal) * x.log
have x_ne_zero : x ≠ 0
Tactic: have x_ne_zero := (ENNReal.toReal_pos_iff.1 x_real).1.ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (hypothesis)
Goal:
x : ℝ≥0∞
y : ℝ
y_pos : 0 < y
x_real : 0 < x.toReal
x_ne_zero : x ≠ 0
⊢ (x ^ y).log = (↑y : EReal) * x.log
have x_ne_top : x ≠ ∞
Tactic: have x_ne_top := (ENNReal.toReal_pos_iff.1 x_real).2.ne
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x : ℝ≥0∞
y : ℝ
y_pos : 0 < y
x_real : 0 < x.toReal
x_ne_zero : x ≠ 0
x_ne_top : x ≠ ∞
⊢ (x ^ y).log = (↑y : EReal) * x.log
have inr : (↑(Real.log (x ^ y).toReal) : EReal) = (↑y : EReal) * (↑(Real.log x.toReal) : EReal)
Tactic: simp only [log, rpow_eq_zero_iff, x_ne_zero, false_and, x_ne_top, or_self, ↓reduceIte,
        rpow_eq_top_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
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) : EReal) = (↑y : EReal) * (↑(Real.log x.toReal) : EReal)
have inr : Real.log (x ^ y).toReal = y * Real.log x.toReal
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x : ℝ≥0∞
n : ℕ
⊢ (x ^ n).log = (↑n : EReal) * x.log
have rw : (HPow.hPow (β := ℝ) x (↑n : ℝ)).log = (↑n : EReal) * x.log
Tactic: rw [← rpow_natCast, log_rpow, EReal.coe_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x : ℝ≥0∞
n : ℕ
rw : (HPow.hPow (β := ℝ) x (↑n : ℝ)).log = (↑n : EReal) * x.log
⊢ (x ^ n).log = (↑n : EReal) * x.log
have rw₁ : (↑(↑n : ℝ) : EReal) * x.log = (↑n : EReal) * x.log
Tactic: rw [← rpow_natCast, log_rpow, EReal.coe_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog (goal)
Goal:
x : ℝ≥0∞
n : ℕ
rw : (HPow.hPow (β := ℝ) x (↑n : ℝ)).log = (↑n : EReal) * x.log
rw₁ : (↑(↑n : ℝ) : EReal) * x.log = (↑n : EReal) * x.log
⊢ (x ^ n).log = (↑n : EReal) * x.log
have rw₂ : (↑n : EReal) * x.log = (↑n : EReal) * x.log
Tactic: rw [← rpow_natCast, log_rpow, EReal.coe_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
x : EReal
⊢ x.exp.log = x
have bot : (exp ⊥).log = ⊥
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
x : EReal
bot : (exp ⊥).log = ⊥
⊢ x.exp.log = x
have coe : ∀ (a : ℝ), (↑a : EReal).exp.log = (↑a : EReal)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
x : EReal
bot : (exp ⊥).log = ⊥
coe : ∀ (a : ℝ), (↑a : EReal).exp.log = (↑a : EReal)
⊢ x.exp.log = x
have top : (exp ⊤).log = ⊤
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
a : ℝ
⊢ (↑a : EReal).exp.log = (↑a : EReal)
have coe : (ENNReal.ofReal (Real.exp a)).log = (↑a : EReal)
Tactic: rw [exp_coe, log_ofReal, if_neg (not_le.mpr (Real.exp_pos _)), Real.log_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
a : ℝ
coe : (ENNReal.ofReal (Real.exp a)).log = (↑a : EReal)
⊢ (↑a : EReal).exp.log = (↑a : EReal)
have coe₁ : (if Real.exp a ≤ 0 then ⊥ else (↑(Real.log (Real.exp a)) : EReal)) = (↑a : EReal)
Tactic: rw [exp_coe, log_ofReal, if_neg (not_le.mpr (Real.exp_pos _)), Real.log_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
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)
⊢ (↑a : EReal).exp.log = (↑a : EReal)
have coe₂ : (↑(Real.log (Real.exp a)) : EReal) = (↑a : EReal)
Tactic: rw [exp_coe, log_ofReal, if_neg (not_le.mpr (Real.exp_pos _)), Real.log_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
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)
⊢ (↑a : EReal).exp.log = (↑a : EReal)
have coe₃ : (↑a : EReal) = (↑a : EReal)
Tactic: rw [exp_coe, log_ofReal, if_neg (not_le.mpr (Real.exp_pos _)), Real.log_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
x : ℝ≥0∞
⊢ x.log.exp = x
have pos : ∀ (hx_top : x = ∞), x.log.exp = x
Tactic: by_cases hx_top : x = ∞
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
x : ℝ≥0∞
pos : ∀ (hx_top : x = ∞), x.log.exp = x
⊢ x.log.exp = x
have neg : ∀ (hx_top : ¬x = ∞), x.log.exp = x
Tactic: by_cases hx_top : x = ∞
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
x : ℝ≥0∞
hx_top : ¬x = ∞
⊢ x.log.exp = x
have pos : ∀ (hx_zero : x = 0), x.log.exp = x
Tactic: by_cases hx_zero : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
x : ℝ≥0∞
hx_top : ¬x = ∞
pos : ∀ (hx_zero : x = 0), x.log.exp = x
⊢ x.log.exp = x
have neg : ∀ (hx_zero : ¬x = 0), x.log.exp = x
Tactic: by_cases hx_zero : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (hypothesis)
Goal:
x : ℝ≥0∞
hx_top : ¬x = ∞
hx_zero : ¬x = 0
⊢ x.log.exp = x
have hx_pos : 0 < x.toReal
Tactic: have hx_pos : 0 < x.toReal := ENNReal.toReal_pos hx_zero hx_top
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
x : ℝ≥0∞
hx_top : ¬x = ∞
hx_zero : ¬x = 0
hx_pos : 0 < x.toReal
⊢ x.log.exp = x
have neg : (ENNReal.ofReal x.toReal).log.exp = ENNReal.ofReal x.toReal
Tactic: rw [← ENNReal.ofReal_toReal hx_top, log_ofReal_of_pos hx_pos, exp_coe, Real.exp_log hx_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
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
⊢ x.log.exp = x
have neg₁ : (↑(Real.log x.toReal) : EReal).exp = ENNReal.ofReal x.toReal
Tactic: rw [← ENNReal.ofReal_toReal hx_top, log_ofReal_of_pos hx_pos, exp_coe, Real.exp_log hx_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
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
⊢ x.log.exp = x
have neg₂ : ENNReal.ofReal (Real.exp (Real.log x.toReal)) = ENNReal.ofReal x.toReal
Tactic: rw [← ENNReal.ofReal_toReal hx_top, log_ofReal_of_pos hx_pos, exp_coe, Real.exp_log hx_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
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
⊢ x.log.exp = x
have neg₃ : ENNReal.ofReal x.toReal = ENNReal.ofReal x.toReal
Tactic: rw [← ENNReal.ofReal_toReal hx_top, log_ofReal_of_pos hx_pos, exp_coe, Real.exp_log hx_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
x : EReal
n : ℕ
⊢ ((↑n : EReal) * x).exp = x.exp ^ n
have simp_rw : ((↑n : EReal) * x).exp.log = (x.exp ^ n).log
Tactic: simp_rw [← log_eq_iff, log_pow, log_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
x : EReal
n : ℕ
simp_rw : ((↑n : EReal) * x).exp.log = (x.exp ^ n).log
⊢ ((↑n : EReal) * x).exp = x.exp ^ n
have simp_rw₁ : ((↑n : EReal) * x).exp.log = (↑n : EReal) * x.exp.log
Tactic: simp_rw [← log_eq_iff, log_pow, log_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
x : EReal
y : ℝ
⊢ (x * (↑y : EReal)).exp = x.exp ^ y
have rw : (x * (↑y : EReal)).exp.log = (x.exp ^ y).log
Tactic: rw [← log_eq_iff, log_rpow, log_exp, log_exp, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
x : EReal
y : ℝ
rw : (x * (↑y : EReal)).exp.log = (x.exp ^ y).log
⊢ (x * (↑y : EReal)).exp = x.exp ^ y
have rw₁ : (x * (↑y : EReal)).exp.log = (↑y : EReal) * x.exp.log
Tactic: rw [← log_eq_iff, log_rpow, log_exp, log_exp, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
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
⊢ (x * (↑y : EReal)).exp = x.exp ^ y
have rw₂ : x * (↑y : EReal) = (↑y : EReal) * x.exp.log
Tactic: rw [← log_eq_iff, log_rpow, log_exp, log_exp, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
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
⊢ (x * (↑y : EReal)).exp = x.exp ^ y
have rw₃ : x * (↑y : EReal) = (↑y : EReal) * x
Tactic: rw [← log_eq_iff, log_rpow, log_exp, log_exp, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
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
⊢ (x * (↑y : EReal)).exp = x.exp ^ y
have rw₄ : (↑y : EReal) * x = (↑y : EReal) * x
Tactic: rw [← log_eq_iff, log_rpow, log_exp, log_exp, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
x : ℝ≥0∞
y : ℝ
⊢ x ^ y = ((↑y : EReal) * x.log).exp
have rw : x ^ y = (x.log * (↑y : EReal)).exp
Tactic: rw [mul_comm, EReal.exp_mul, exp_log]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
x : ℝ≥0∞
y : ℝ
rw : x ^ y = (x.log * (↑y : EReal)).exp
⊢ x ^ y = ((↑y : EReal) * x.log).exp
have rw₁ : x ^ y = x.log.exp ^ y
Tactic: rw [mul_comm, EReal.exp_mul, exp_log]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
x : ℝ≥0∞
y : ℝ
rw : x ^ y = (x.log * (↑y : EReal)).exp
rw₁ : x ^ y = x.log.exp ^ y
⊢ x ^ y = ((↑y : EReal) * x.log).exp
have rw₂ : x ^ y = x ^ y
Tactic: rw [mul_comm, EReal.exp_mul, exp_log]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
⊢ Filter.Tendsto exp (𝓝 0) (𝓝 1)
have h : 1 = exp 0
Tactic: convert! continuous_exp.tendsto 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
b : ℝ≥0∞
hb : 1 < b
⊢ Filter.Tendsto (β := ℝ≥0∞) (fun (x : ℝ) ↦ b ^ x) Filter.atTop (𝓝 ∞)
have simp_rw : Filter.Tendsto (β := ℝ≥0∞) (fun (x : ℝ) ↦ ((↑x : EReal) * b.log).exp) Filter.atTop (𝓝 ∞)
Tactic: simp_rw [ENNReal.rpow_eq_exp_mul_log]
-- 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.atTop (𝓝 ∞)
have refine : Filter.Tendsto (β := EReal) (fun (x : ℝ) ↦ (↑x : EReal) * b.log) Filter.atTop (𝓝 ⊤)
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 : 1 < b
⊢ Filter.Tendsto (β := EReal) (fun (x : ℝ) ↦ (↑x : EReal) * b.log) Filter.atTop (𝓝 ⊤)
have h : ⊤ = ⊤ * b.log
Tactic: convert! EReal.Tendsto.mul_const tendsto_coe_atTop _ _
-- 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.atTop (𝓝 ⊤)
have convert_2 : Ne (α := EReal) ⊤ 0 ∨ b.log ≠ ⊥
Tactic: convert! EReal.Tendsto.mul_const tendsto_coe_atTop _ _
-- 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.atTop (𝓝 ⊤)
have convert_3 : Ne (α := EReal) ⊤ 0 ∨ b.log ≠ ⊤
Tactic: convert! EReal.Tendsto.mul_const tendsto_coe_atTop _ _
-- 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.top_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.atTop (𝓝 0)
have simp_rw : Filter.Tendsto (β := ℝ≥0∞) (fun (x : ℝ) ↦ ((↑x : EReal) * b.log).exp) Filter.atTop (𝓝 0)
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.atTop (𝓝 0)
have refine : Filter.Tendsto (β := EReal) (fun (x : ℝ) ↦ (↑x : EReal) * b.log) Filter.atTop (𝓝 ⊥)
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 : b < 1
⊢ Filter.Tendsto (β := EReal) (fun (x : ℝ) ↦ (↑x : EReal) * b.log) Filter.atTop (𝓝 ⊥)
have h : ⊥ = ⊤ * b.log
Tactic: convert! EReal.Tendsto.mul_const tendsto_coe_atTop _ _
-- 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.atTop (𝓝 ⊥)
have convert_2 : Ne (α := EReal) ⊤ 0 ∨ b.log ≠ ⊥
Tactic: convert! EReal.Tendsto.mul_const tendsto_coe_atTop _ _
-- 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.atTop (𝓝 ⊥)
have convert_3 : Ne (α := EReal) ⊤ 0 ∨ b.log ≠ ⊤
Tactic: convert! EReal.Tendsto.mul_const tendsto_coe_atTop _ _
-- 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.top_mul_of_neg (log_lt_zero_iff.2 hb)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp (goal)
Goal:
b : ℝ≥0∞
hb : 1 < b
⊢ Filter.Tendsto (β := ℝ≥0∞) (fun (x : ℝ) ↦ b ^ x) Filter.atBot (𝓝 0)
have simp_rw : Filter.Tendsto (β := ℝ≥0∞) (fun (x : ℝ) ↦ ((↑x : EReal) * b.log).exp) Filter.atBot (𝓝 0)
Tactic: simp_rw [ENNReal.rpow_eq_exp_mul_log]