-- Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean
theorem log_rpow {x : ℝ≥0∞} {y : ℝ} : log (x ^ y) = y * log x

Proof state:
case inl.inr.inl
y : ℝ
y_neg : y < 0
⊢ (⊤ ^ y).log = ↑y * ⊤.log

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

Result:
no goals

Proof state:
case inr.inr.inr.inr
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:
norm_cast

Result:
case inr.inr.inr.inr
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

Proof state:
case inr.inl
x : ℝ≥0∞
⊢ (x ^ 0).log = ↑0 * x.log

Tactic:
simp

Result:
no goals

Proof state:
case inr.inr.inr.inr
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

Result:
no goals

Proof state:
case inr.inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ (⊤ ^ y).log = ↑y * ⊤.log

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

Result:
case inr.inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ 0 < ↑y

Proof state:
case inl.inr.inr
x : ℝ≥0∞
y : ℝ
y_neg : y < 0
x_real : 0 < x.toReal
x_ne_zero : x ≠ 0
⊢ (x ^ y).log = ↑y * x.log

Tactic:
have x_ne_top := (ENNReal.toReal_pos_iff.1 x_real).2.ne

Result:
case inl.inr.inr
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 * x.log

Proof state:
case inr.inr.inr.inr
x : ℝ≥0∞
y : ℝ
y_pos : 0 < y
x_real : 0 < x.toReal
⊢ (x ^ y).log = ↑y * x.log

Tactic:
have x_ne_zero := (ENNReal.toReal_pos_iff.1 x_real).1.ne'

Result:
case inr.inr.inr.inr
x : ℝ≥0∞
y : ℝ
y_pos : 0 < y
x_real : 0 < x.toReal
x_ne_zero : x ≠ 0
⊢ (x ^ y).log = ↑y * x.log

Proof state:
case inl
x : ℝ≥0∞
y : ℝ
y_neg : y < 0
⊢ (x ^ y).log = ↑y * x.log

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

Result:
case inl.inl
y : ℝ
y_neg : y < 0
⊢ (0 ^ y).log = ↑y * log 0

case inl.inr.inl
y : ℝ
y_neg : y < 0
⊢ (⊤ ^ y).log = ↑y * ⊤.log

case inl.inr.inr
x : ℝ≥0∞
y : ℝ
y_neg : y < 0
x_real : 0 < x.toReal
⊢ (x ^ y).log = ↑y * x.log

Proof state:
x : ℝ≥0∞
y : ℝ
⊢ (x ^ y).log = ↑y * x.log

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

Result:
case inl
x : ℝ≥0∞
y : ℝ
y_neg : y < 0
⊢ (x ^ y).log = ↑y * x.log

case inr.inl
x : ℝ≥0∞
⊢ (x ^ 0).log = ↑0 * x.log

case inr.inr
x : ℝ≥0∞
y : ℝ
y_pos : 0 < y
⊢ (x ^ y).log = ↑y * x.log

Proof state:
case inl.inr.inr
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

Result:
no goals

Proof state:
case inl.inr.inr
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 * 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]

Result:
case inl.inr.inr
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)

Proof state:
case inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ (0 ^ y).log = ↑y * log 0

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

Result:
case inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ 0 < ↑y

Proof state:
case inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ 0 < ↑y

Tactic:
norm_cast

Result:
no goals

Proof state:
case inl.inr.inr
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:
norm_cast

Result:
case inl.inr.inr
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

Proof state:
case inr.inr.inr.inr
x : ℝ≥0∞
y : ℝ
y_pos : 0 < y
x_real : 0 < x.toReal
x_ne_zero : x ≠ 0
⊢ (x ^ y).log = ↑y * x.log

Tactic:
have x_ne_top := (ENNReal.toReal_pos_iff.1 x_real).2.ne

Result:
case inr.inr.inr.inr
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 * x.log

Proof state:
case inl.inl
y : ℝ
y_neg : y < 0
⊢ (0 ^ y).log = ↑y * log 0

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

Result:
no goals

Proof state:
case inr.inr.inr.inr
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 * 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]

Result:
case inr.inr.inr.inr
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)

Proof state:
case inr.inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ 0 < ↑y

Tactic:
norm_cast

Result:
no goals

Proof state:
case inl.inr.inr
x : ℝ≥0∞
y : ℝ
y_neg : y < 0
x_real : 0 < x.toReal
⊢ (x ^ y).log = ↑y * x.log

Tactic:
have x_ne_zero := (ENNReal.toReal_pos_iff.1 x_real).1.ne'

Result:
case inl.inr.inr
x : ℝ≥0∞
y : ℝ
y_neg : y < 0
x_real : 0 < x.toReal
x_ne_zero : x ≠ 0
⊢ (x ^ y).log = ↑y * x.log

Proof state:
case inr.inr
x : ℝ≥0∞
y : ℝ
y_pos : 0 < y
⊢ (x ^ y).log = ↑y * x.log

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

Result:
case inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ (0 ^ y).log = ↑y * log 0

case inr.inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ (⊤ ^ y).log = ↑y * ⊤.log

case inr.inr.inr.inr
x : ℝ≥0∞
y : ℝ
y_pos : 0 < y
x_real : 0 < x.toReal
⊢ (x ^ y).log = ↑y * x.log