awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
hx : 0 ≤ x
h : 2 * x / (x + 2) = 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑0 : ℝ) + 1)) * (x / (x + 2)) ^ (HMul.hMul (α := ℕ) 2 0 + 1)
⊢ 2 * x / (x + 2) ≤ log (1 + x)

Tactic:
convert! le_hasSum (hasSum_log_one_add hx) 0 (by intros; positivity) using 1

Premises used: Real.hasSum_log_one_add, le_hasSum, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
hx : 0 ≤ x
⊢ 2 * x / (x + 2) = 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑0 : ℝ) + 1)) * (x / (x + 2)) ^ (HMul.hMul (α := ℕ) 2 0 + 1)

Tactic:
simp [field]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
hx : 0 < x
j : ℕ
h : j ≠ 0
⊢ 0 ≤ 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑j : ℝ) + 1)) * (x / (x + 2)) ^ (2 * j + 1)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
hx : 0 < x
⊢ Ne (α := ℕ) 1 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
hx : 0 < x
⊢ 0 < 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑1 : ℝ) + 1)) * (x / (x + 2)) ^ (HMul.hMul (α := ℕ) 2 1 + 1)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
hx : 0 < x
h : 2 * x / (x + 2) = 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑0 : ℝ) + 1)) * (x / (x + 2)) ^ (HMul.hMul (α := ℕ) 2 0 + 1)
⊢ 2 * x / (x + 2) < log (1 + x)

Tactic:
convert!
    lt_hasSum (hasSum_log_one_add hx.le) 0 (by intros; positivity) 1 (by positivity)
      (by positivity) using 1

Premises used: Real.hasSum_log_one_add, LT.lt.le, OfNat.ofNat, lt_hasSum
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
hx : 0 < x
⊢ 2 * x / (x + 2) = 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑0 : ℝ) + 1)) * (x / (x + 2)) ^ (HMul.hMul (α := ℕ) 2 0 + 1)

Tactic:
simp [field]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
⊢ log 0 = ⊥

Tactic:
if_pos rfl

Premises used: ENNReal.log, if_pos, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
⊢ log 1 = 0

Tactic:
simp [log]

Premises used: ENNReal.log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
⊢ log ∞ = ⊤

Tactic:
rfl

Premises used: ENNReal.log, rfl, ite
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ
simp :
  (if x ≤ 0 then ⊥ else (↑(Real.log (ENNReal.ofReal x).toReal) : EReal)) = if x ≤ 0 then ⊥ else (↑(Real.log x) : EReal)
⊢ (ENNReal.ofReal x).log = if x ≤ 0 then ⊥ else (↑(Real.log x) : EReal)

Tactic:
simp only [log, ENNReal.ofReal_ne_top,
    ENNReal.ofReal_eq_zero, if_false]

Premises used: ENNReal.ofReal_eq_zero, if_false, ENNReal.log, ENNReal.ofReal_ne_top
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ
pos : ∀ (h_nonpos : x ≤ 0), Eq (α := EReal) ⊥ ⊥
neg : ∀ (h_nonpos : ¬x ≤ 0), (↑(Real.log (ENNReal.ofReal x).toReal) : EReal) = (↑(Real.log x) : EReal)
⊢ (if x ≤ 0 then ⊥ else (↑(Real.log (ENNReal.ofReal x).toReal) : EReal)) = if x ≤ 0 then ⊥ else (↑(Real.log x) : EReal)

Tactic:
split_ifs with h_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ
h_nonpos : x ≤ 0
⊢ Eq (α := EReal) ⊥ ⊥

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ
h_nonpos : ¬x ≤ 0
neg neg₁ : (↑(Real.log x) : EReal) = (↑(Real.log x) : EReal)
⊢ (↑(Real.log (ENNReal.ofReal x).toReal) : EReal) = (↑(Real.log x) : EReal)

Tactic:
rw [ENNReal.toReal_ofReal (not_le.mp h_nonpos).le]

Premises used: not_le, LT.lt.le, ENNReal.toReal_ofReal, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ
hx : 0 < x
rw : (if x ≤ 0 then ⊥ else (↑(Real.log x) : EReal)) = (↑(Real.log x) : EReal)
rw₁ rw₂ : (↑(Real.log x) : EReal) = (↑(Real.log x) : EReal)
⊢ (ENNReal.ofReal x).log = (↑(Real.log x) : EReal)

Tactic:
rw [log_ofReal, if_neg hx.not_ge]

Premises used: LT.lt.not_ge, if_neg, ENNReal.log_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ≥0∞
h : x ≠ 0
h' : x ≠ ∞
⊢ x.log = (↑(Real.log x.toReal) : EReal)

Tactic:
simp [log, h, h']

Premises used: ENNReal.log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ≥0∞
h : 0 < x.toReal
⊢ x.log = (↑(Real.log x.toReal) : EReal)

Tactic:
simp [log, (ENNReal.toReal_pos_iff.1 h).1.ne', (ENNReal.toReal_pos_iff.1 h).2.ne]

Premises used: ENNReal.toReal_pos_iff, ENNReal.log, LT.lt.ne', And.right, And.left, Iff.mp, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ≥0
h : x ≠ 0
⊢ (↑x : ℝ≥0∞).log = (↑(Real.log (↑x : ℝ)) : EReal)

Tactic:
simp [log, h]

Premises used: ENNReal.log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x y : ℝ≥0∞
h : x < y
pos : x = 0 → y = 0 → LT.lt (α := EReal) ⊥ ⊥
pos₁ : x = 0 → ¬y = 0 → y = ∞ → LT.lt (α := EReal) ⊥ ⊤
neg : x = 0 → ¬y = 0 → ¬y = ∞ → ⊥ < (↑(Real.log y.toReal) : EReal)
pos₂ : ¬x = 0 → x = ∞ → y = 0 → LT.lt (α := EReal) ⊤ ⊥
pos₃ : ¬x = 0 → x = ∞ → ¬y = 0 → y = ∞ → LT.lt (α := EReal) ⊤ ⊤
neg₁ : ¬x = 0 → x = ∞ → ¬y = 0 → ¬y = ∞ → ⊤ < (↑(Real.log y.toReal) : EReal)
pos₄ : ¬x = 0 → ¬x = ∞ → y = 0 → (↑(Real.log x.toReal) : EReal) < ⊥
pos₅ : ¬x = 0 → ¬x = ∞ → ¬y = 0 → y = ∞ → (↑(Real.log x.toReal) : EReal) < ⊤
neg₂ : ¬x = 0 → ¬x = ∞ → ¬y = 0 → ¬y = ∞ → (↑(Real.log x.toReal) : EReal) < (↑(Real.log y.toReal) : EReal)
⊢ (if x = 0 then ⊥ else if x = ∞ then ⊤ else (↑(Real.log x.toReal) : EReal)) <
    if y = 0 then ⊥ else if y = ∞ then ⊤ else (↑(Real.log y.toReal) : EReal)

Tactic:
split_ifs
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x y : ℝ≥0∞
h : x < y
h_1 : x = 0
h_2 : y = 0
⊢ LT.lt (α := EReal) ⊥ ⊥

Tactic:
simp_all [Real.log_lt_log, toReal_pos_iff, pos_iff_ne_zero, lt_top_iff_ne_top]

Premises used: ENNReal.toReal_pos_iff, Real.log_lt_log, lt_top_iff_ne_top, pos_iff_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x y : ℝ≥0∞
h : x < y
h_1 : x = 0
h_2 : ¬y = 0
h_3 : y = ∞
⊢ LT.lt (α := EReal) ⊥ ⊤

Tactic:
simp_all [Real.log_lt_log, toReal_pos_iff, pos_iff_ne_zero, lt_top_iff_ne_top]

Premises used: ENNReal.toReal_pos_iff, Real.log_lt_log, lt_top_iff_ne_top, pos_iff_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x y : ℝ≥0∞
h : x < y
h_1 : x = 0
h_2 : ¬y = 0
h_3 : ¬y = ∞
⊢ ⊥ < (↑(Real.log y.toReal) : EReal)

Tactic:
simp_all [Real.log_lt_log, toReal_pos_iff, pos_iff_ne_zero, lt_top_iff_ne_top]

Premises used: ENNReal.toReal_pos_iff, Real.log_lt_log, lt_top_iff_ne_top, pos_iff_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x y : ℝ≥0∞
h : x < y
h_1 : ¬x = 0
h_2 : x = ∞
h_3 : y = 0
⊢ LT.lt (α := EReal) ⊤ ⊥

Tactic:
simp_all [Real.log_lt_log, toReal_pos_iff, pos_iff_ne_zero, lt_top_iff_ne_top]

Premises used: ENNReal.toReal_pos_iff, Real.log_lt_log, lt_top_iff_ne_top, pos_iff_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x y : ℝ≥0∞
h : x < y
h_1 : ¬x = 0
h_2 : x = ∞
h_3 : ¬y = 0
h_4 : y = ∞
⊢ LT.lt (α := EReal) ⊤ ⊤

Tactic:
simp_all [Real.log_lt_log, toReal_pos_iff, pos_iff_ne_zero, lt_top_iff_ne_top]

Premises used: ENNReal.toReal_pos_iff, Real.log_lt_log, lt_top_iff_ne_top, pos_iff_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x y : ℝ≥0∞
h : x < y
h_1 : ¬x = 0
h_2 : x = ∞
h_3 : ¬y = 0
h_4 : ¬y = ∞
⊢ ⊤ < (↑(Real.log y.toReal) : EReal)

Tactic:
simp_all [Real.log_lt_log, toReal_pos_iff, pos_iff_ne_zero, lt_top_iff_ne_top]

Premises used: ENNReal.toReal_pos_iff, Real.log_lt_log, lt_top_iff_ne_top, pos_iff_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x y : ℝ≥0∞
h : x < y
h_1 : ¬x = 0
h_2 : ¬x = ∞
h_3 : y = 0
⊢ (↑(Real.log x.toReal) : EReal) < ⊥

Tactic:
simp_all [Real.log_lt_log, toReal_pos_iff, pos_iff_ne_zero, lt_top_iff_ne_top]

Premises used: ENNReal.toReal_pos_iff, Real.log_lt_log, lt_top_iff_ne_top, pos_iff_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x y : ℝ≥0∞
h : x < y
h_1 : ¬x = 0
h_2 : ¬x = ∞
h_3 : ¬y = 0
h_4 : y = ∞
⊢ (↑(Real.log x.toReal) : EReal) < ⊤

Tactic:
simp_all [Real.log_lt_log, toReal_pos_iff, pos_iff_ne_zero, lt_top_iff_ne_top]

Premises used: ENNReal.toReal_pos_iff, Real.log_lt_log, lt_top_iff_ne_top, pos_iff_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x y : ℝ≥0∞
h : x < y
h_1 : ¬x = 0
h_2 : ¬x = ∞
h_3 : ¬y = 0
h_4 : ¬y = ∞
⊢ (↑(Real.log x.toReal) : EReal) < (↑(Real.log y.toReal) : EReal)

Tactic:
simp_all [Real.log_lt_log, toReal_pos_iff, pos_iff_ne_zero, lt_top_iff_ne_top]

Premises used: ENNReal.toReal_pos_iff, Real.log_lt_log, lt_top_iff_ne_top, pos_iff_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
⊢ Monotone log

Tactic:
log_strictMono.monotone

Premises used: StrictMono.monotone, ENNReal.log_strictMono
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
⊢ Function.Injective log

Tactic:
log_strictMono.injective

Premises used: ENNReal.log_strictMono, StrictMono.injective
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
h : log 0 = ⊥
⊢ ∃ (a : ℝ≥0∞), a.log = ⊥

Tactic:
use 0
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
⊢ log 0 = ⊥

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
h : log ∞ = ⊤
⊢ ∃ (a : ℝ≥0∞), a.log = ⊤

Tactic:
use ⊤
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
⊢ log ∞ = ⊤

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
y : ℝ
h : (ENNReal.ofReal (Real.exp y)).log = (↑y : EReal)
⊢ ∃ (a : ℝ≥0∞), a.log = (↑y : EReal)

Tactic:
use ENNReal.ofReal (Real.exp y)

Premises used: ENNReal.ofReal, Real.exp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
y : ℝ
⊢ (ENNReal.ofReal (Real.exp y)).log = (↑y : EReal)

Tactic:
simp [Real.exp_pos]

Premises used: Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
y : EReal
bot : ∃ (a : ℝ≥0∞), a.log = ⊥
top : ∃ (a : ℝ≥0∞), a.log = ⊤
coe : ∀ (y : ℝ), ∃ (a : ℝ≥0∞), a.log = (↑y : EReal)
⊢ ∃ (a : ℝ≥0∞), a.log = y

Tactic:
cases y with
  | bot => use 0; simp
  | top => use ⊤; simp
  | coe y => use ENNReal.ofReal (Real.exp y); simp [Real.exp_pos]

Premises used: Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
⊢ Function.Bijective log

Tactic:
⟨log_injective, log_surjective⟩

Premises used: ENNReal.log_surjective, And.intro, Function.Bijective, ENNReal.log_injective
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x y : ℝ≥0∞
⊢ x.log = y.log ↔ x = y

Tactic:
log_injective.eq_iff

Premises used: Function.Injective.eq_iff, ENNReal.log_injective
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ≥0∞
⊢ x.log = ⊥ ↔ x = 0

Tactic:
log_zero ▸ @log_eq_iff x 0

Premises used: ENNReal.log_eq_iff, Eq.rec, ENNReal.log_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ≥0∞
⊢ x.log = 0 ↔ x = 1

Tactic:
log_one ▸ @log_eq_iff x 1

Premises used: ENNReal.log_eq_iff, Eq.rec, ENNReal.log_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ≥0∞
⊢ x.log = ⊤ ↔ x = ∞

Tactic:
log_top ▸ @log_eq_iff x ⊤

Premises used: ENNReal.log_top, ENNReal.log_eq_iff, Eq.rec
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x y : ℝ≥0∞
⊢ x.log < y.log ↔ x < y

Tactic:
log_strictMono.lt_iff_lt

Premises used: ENNReal.log_strictMono, StrictMono.lt_iff_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ≥0∞
⊢ ⊥ < x.log ↔ 0 < x

Tactic:
log_zero ▸ @log_lt_log_iff 0 x

Premises used: ENNReal.log_lt_log_iff, Eq.rec, ENNReal.log_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ≥0∞
⊢ x.log < ⊤ ↔ x < ∞

Tactic:
log_top ▸ @log_lt_log_iff x ⊤

Premises used: ENNReal.log_lt_log_iff, ENNReal.log_top, Eq.rec
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ≥0∞
⊢ x.log < 0 ↔ x < 1

Tactic:
log_one ▸ @log_lt_log_iff x 1

Premises used: ENNReal.log_lt_log_iff, Eq.rec, ENNReal.log_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ≥0∞
⊢ 0 < x.log ↔ 1 < x

Tactic:
log_one ▸ @log_lt_log_iff 1 x

Premises used: ENNReal.log_lt_log_iff, Eq.rec, ENNReal.log_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x y : ℝ≥0∞
⊢ x.log ≤ y.log ↔ x ≤ y

Tactic:
log_strictMono.le_iff_le

Premises used: ENNReal.log_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ≥0∞
⊢ x.log ≤ 0 ↔ x ≤ 1

Tactic:
log_one ▸ @log_le_log_iff x 1

Premises used: ENNReal.log_le_log_iff, Eq.rec, ENNReal.log_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ≥0∞
⊢ 0 ≤ x.log ↔ 1 ≤ x

Tactic:
log_one ▸ @log_le_log_iff 1 x

Premises used: ENNReal.log_le_log_iff, Eq.rec, ENNReal.log_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x y : ℝ≥0∞
h : x ≤ y
⊢ x.log ≤ y.log

Tactic:
log_monotone h

Premises used: ENNReal.log_monotone
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x y : ℝ≥0∞
h : x < y
⊢ x.log < y.log

Tactic:
log_strictMono h

Premises used: ENNReal.log_strictMono
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x y : ℝ≥0∞
inl : (0 * y).log = log 0 + y.log
inr : (∞ * y).log = log ∞ + y.log
inr₁ : ∀ (x_real : 0 < x.toReal), (x * y).log = x.log + y.log
⊢ (x * y).log = x.log + y.log

Tactic:
rcases ENNReal.trichotomy x with (rfl | rfl | x_real)

Premises used: ENNReal.trichotomy, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
y : ℝ≥0∞
⊢ (0 * y).log = log 0 + y.log

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
y : ℝ≥0∞
inr : (HMul.hMul (α := ℝ≥0∞) ∞ 0).log = ⊤ + log 0
inr₁ : (HMul.hMul (α := ℝ≥0∞) ∞ ∞).log = ⊤ + log ∞
inr₂ : ∀ (y_real : 0 < y.toReal), (∞ * y).log = ⊤ + y.log
⊢ (∞ * y).log = ⊤ + y.log

Tactic:
rcases ENNReal.trichotomy y with (rfl | rfl | y_real)

Premises used: ENNReal.trichotomy, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
inr : log 0 = ⊤ + log 0
inr₁ : ⊥ = HAdd.hAdd (α := EReal) ⊤ ⊥
inr₂ inr₃ : Eq (α := EReal) ⊥ ⊥
⊢ (HMul.hMul (α := ℝ≥0∞) ∞ 0).log = ⊤ + log 0

Tactic:
rw [mul_zero, log_zero, EReal.add_bot]

Premises used: EReal.add_bot, MulZeroClass.mul_zero, ENNReal.log_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
⊢ (HMul.hMul (α := ℝ≥0∞) ∞ ∞).log = ⊤ + log ∞

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
y : ℝ≥0∞
y_real : 0 < y.toReal
inr : Eq (α := ℝ≥0∞) (if y = 0 then 0 else ∞) ∞
⊢ (∞ * y).log = ⊤ + y.log

Tactic:
rw [log_pos_real' y_real, ENNReal.top_mul', EReal.top_add_coe, log_eq_top_iff]

Premises used: ENNReal.log_pos_real', EReal.top_add_coe, ENNReal.top_mul', ENNReal.log_eq_top_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
y : ℝ≥0∞
y_real : 0 < y.toReal
inr : ¬y = 0
⊢ Eq (α := ℝ≥0∞) (if y = 0 then 0 else ∞) ∞

Tactic:
simp only [ite_eq_right_iff, zero_ne_top, imp_false]

Premises used: imp_false, ENNReal.zero_ne_top, ite_eq_right_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
y : ℝ≥0∞
y_real : 0 < y.toReal
⊢ ¬y = 0

Tactic:
(ENNReal.toReal_pos_iff.1 y_real).1.ne'

Premises used: ENNReal.toReal_pos_iff, LT.lt.ne', And.left, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
y : ℝ≥0∞
y_real : 0 < y.toReal
⊢ ¬y = 0

Tactic:
exact (ENNReal.toReal_pos_iff.1 y_real).1.ne'

Premises used: ENNReal.toReal_pos_iff, LT.lt.ne', And.left, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x y : ℝ≥0∞
x_real : 0 < x.toReal
inr : (x * y).log = (↑(Real.log x.toReal) : EReal) + y.log
⊢ (x * y).log = x.log + y.log

Tactic:
rw [log_pos_real' x_real]

Premises used: ENNReal.log_pos_real'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
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 ∞
inr₂ : ∀ (y_real : 0 < y.toReal), (x * y).log = (↑(Real.log x.toReal) : EReal) + y.log
⊢ (x * y).log = (↑(Real.log x.toReal) : EReal) + y.log

Tactic:
rcases ENNReal.trichotomy y with (rfl | rfl | y_real)

Premises used: ENNReal.trichotomy, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ≥0∞
x_real : 0 < x.toReal
⊢ (x * 0).log = (↑(Real.log x.toReal) : EReal) + log 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ≥0∞
x_real : 0 < x.toReal
⊢ (x * ∞).log = (↑(Real.log x.toReal) : EReal) + log ∞

Tactic:
simp [(ENNReal.toReal_pos_iff.1 x_real).1.ne']

Premises used: ENNReal.toReal_pos_iff, LT.lt.ne', And.left, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
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
inr₁ : ∀ (x_real : 0 < x.toReal) (y_real : 0 < y.toReal), 0 < (x * y).toReal
⊢ (x * y).log = (↑(Real.log x.toReal) : EReal) + y.log

Tactic:
rw_mod_cast [log_pos_real', log_pos_real' y_real, ENNReal.toReal_mul]

Premises used: ENNReal.log_pos_real', ENNReal.toReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x y : ℝ≥0∞
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:
Real.log_mul x_real.ne' y_real.ne'

Premises used: LT.lt.ne', Real.log_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x y : ℝ≥0∞
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:
exact Real.log_mul x_real.ne' y_real.ne'

Premises used: LT.lt.ne', Real.log_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x y : ℝ≥0∞
x_real : 0 < x.toReal
y_real : 0 < y.toReal
inr : 0 < x.toReal * y.toReal
⊢ 0 < (x * y).toReal

Tactic:
rw [toReal_mul]

Premises used: ENNReal.toReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x y : ℝ≥0∞
x_real : 0 < x.toReal
y_real : 0 < y.toReal
⊢ 0 < x.toReal * y.toReal

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
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
inr₁ : ∀ (y_pos : 0 < y), (x ^ y).log = (↑y : EReal) * x.log
⊢ (x ^ y).log = (↑y : EReal) * x.log

Tactic:
rcases lt_trichotomy y 0 with (y_neg | rfl | y_pos)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
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 ∞
inl₂ : ∀ (x_real : 0 < x.toReal), (x ^ y).log = (↑y : EReal) * x.log
⊢ (x ^ y).log = (↑y : EReal) * x.log

Tactic:
rcases ENNReal.trichotomy x with (rfl | rfl | x_real)

Premises used: ENNReal.trichotomy, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
y : ℝ
y_neg : y < 0
⊢ (HPow.hPow (α := ℝ≥0∞) 0 y).log = (↑y : EReal) * log 0

Tactic:
simp only [ENNReal.zero_rpow_def y, not_lt_of_gt y_neg, y_neg.ne, if_false, log_top,
        log_zero, EReal.coe_mul_bot_of_neg y_neg]

Premises used: ENNReal.log_top, if_false, ENNReal.zero_rpow_def, ENNReal.log_zero, not_lt_of_gt, EReal.coe_mul_bot_of_neg, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
y : ℝ
y_neg : y < 0
inl : log 0 = (↑y : EReal) * log ∞
inl₁ : ⊥ = (↑y : EReal) * log ∞
inl₂ : ⊥ = (↑y : EReal) * ⊤
inl₃ inl₄ : Eq (α := EReal) ⊥ ⊥
⊢ (HPow.hPow (α := ℝ≥0∞) ∞ y).log = (↑y : EReal) * log ∞

Tactic:
rw [ENNReal.top_rpow_of_neg y_neg, log_zero, log_top, EReal.coe_mul_top_of_neg y_neg]

Premises used: ENNReal.log_top, ENNReal.log_zero, ENNReal.top_rpow_of_neg, EReal.coe_mul_top_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ≥0∞
y : ℝ
y_neg : y < 0
x_real : 0 < x.toReal
⊢ x ≠ 0

Tactic:
have x_ne_zero := (ENNReal.toReal_pos_iff.1 x_real).1.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ≥0∞
y : ℝ
y_neg : y < 0
x_real : 0 < x.toReal
x_ne_zero : x ≠ 0
⊢ x ≠ ∞

Tactic:
have x_ne_top := (ENNReal.toReal_pos_iff.1 x_real).2.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ≥0∞
y : ℝ
y_neg : y < 0
x_real : 0 < x.toReal
x_ne_zero : x ≠ 0
x_ne_top : x ≠ ∞
inl : (↑(Real.log (x ^ y).toReal) : EReal) = (↑y : EReal) * (↑(Real.log x.toReal) : EReal)
⊢ (x ^ y).log = (↑y : EReal) * x.log

Tactic:
simp only [log, rpow_eq_zero_iff, x_ne_zero, false_and, x_ne_top, or_self, ↓reduceIte,
        rpow_eq_top_iff]

Premises used: ENNReal.rpow_eq_zero_iff, false_and, ENNReal.log, ENNReal.rpow_eq_top_iff, or_self, reduceIte
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ≥0∞
y : ℝ
y_neg : y < 0
x_real : 0 < x.toReal
x_ne_zero : x ≠ 0
x_ne_top : x ≠ ∞
inl : Real.log (x ^ y).toReal = y * Real.log x.toReal
⊢ (↑(Real.log (x ^ y).toReal) : EReal) = (↑y : EReal) * (↑(Real.log x.toReal) : EReal)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
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 = y * Real.log x.toReal

Tactic:
ENNReal.toReal_rpow x y ▸ Real.log_rpow x_real y

Premises used: Real.log_rpow, Eq.rec, ENNReal.toReal_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
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 = 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∞
⊢ (HPow.hPow (β := ℝ) x 0).log = (↑0 : EReal) * x.log

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
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 ∞
inr₂ : ∀ (x_real : 0 < x.toReal), (x ^ y).log = (↑y : EReal) * x.log
⊢ (x ^ y).log = (↑y : EReal) * x.log

Tactic:
rcases ENNReal.trichotomy x with (rfl | rfl | x_real)

Premises used: ENNReal.trichotomy, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
y : ℝ
y_pos : 0 < y
inr : 0 < (↑y : EReal)
⊢ (HPow.hPow (α := ℝ≥0∞) 0 y).log = (↑y : EReal) * log 0

Tactic:
rw [ENNReal.zero_rpow_of_pos y_pos, log_zero, EReal.mul_bot_of_pos]

Premises used: ENNReal.zero_rpow_of_pos, EReal.mul_bot_of_pos, ENNReal.log_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
y : ℝ
y_pos : 0 < y
inr inr₁ inr₂ inr₃ : 0 < y
⊢ 0 < (↑y : EReal)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
y : ℝ
y_pos : 0 < y
inr : 0 < (↑y : EReal)
⊢ (HPow.hPow (α := ℝ≥0∞) ∞ y).log = (↑y : EReal) * log ∞

Tactic:
rw [ENNReal.top_rpow_of_pos y_pos, log_top, EReal.mul_top_of_pos]

Premises used: ENNReal.log_top, ENNReal.top_rpow_of_pos, EReal.mul_top_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
Goal:
x : ℝ≥0∞
y : ℝ
y_pos : 0 < y
x_real : 0 < x.toReal
⊢ x ≠ 0

Tactic:
have x_ne_zero := (ENNReal.toReal_pos_iff.1 x_real).1.ne'
-- 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 ≠ ∞

Tactic:
have x_ne_top := (ENNReal.toReal_pos_iff.1 x_real).2.ne
-- 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 ≠ ∞
inr : (↑(Real.log (x ^ y).toReal) : EReal) = (↑y : EReal) * (↑(Real.log x.toReal) : EReal)
⊢ (x ^ y).log = (↑y : EReal) * x.log

Tactic:
simp only [log, rpow_eq_zero_iff, x_ne_zero, false_and, x_ne_top, or_self, ↓reduceIte,
        rpow_eq_top_iff]

Premises used: ENNReal.rpow_eq_zero_iff, false_and, ENNReal.log, ENNReal.rpow_eq_top_iff, or_self, reduceIte
-- 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 ≠ ∞
inr : Real.log (x ^ y).toReal = y * Real.log x.toReal
⊢ (↑(Real.log (x ^ y).toReal) : EReal) = (↑y : EReal) * (↑(Real.log x.toReal) : EReal)

Tactic:
norm_cast
-- 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:
ENNReal.toReal_rpow x y ▸ Real.log_rpow x_real y

Premises used: Real.log_rpow, Eq.rec, ENNReal.toReal_rpow