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

Proof state:
case inr.inl.inr.inr
y : ℝ≥0∞
y_real : 0 < y.toReal
⊢ (if y = 0 then 0 else ⊤) = ⊤

Tactic:
simp only [ite_eq_right_iff, zero_ne_top, imp_false]

Result:
case inr.inl.inr.inr
y : ℝ≥0∞
y_real : 0 < y.toReal
⊢ ¬y = 0

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

Tactic:
simp

Result:
no goals

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

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

Result:
case inr.inr.inl
x : ℝ≥0∞
x_real : 0 < x.toReal
⊢ (x * 0).log = ↑(Real.log x.toReal) + log 0

case inr.inr.inr.inl
x : ℝ≥0∞
x_real : 0 < x.toReal
⊢ (x * ⊤).log = ↑(Real.log x.toReal) + ⊤.log

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

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

Result:
no goals

Proof state:
case inr.inr.inr.inr
x y : ℝ≥0∞
x_real : 0 < x.toReal
y_real : 0 < y.toReal
⊢ 0 < x.toReal * y.toReal

Tactic:
positivity

Result:
no goals

Proof state:
case inr.inr.inr.inl
x : ℝ≥0∞
x_real : 0 < x.toReal
⊢ (x * ⊤).log = ↑(Real.log x.toReal) + ⊤.log

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

Result:
no goals

Proof state:
case inr.inl.inr.inr
y : ℝ≥0∞
y_real : 0 < y.toReal
⊢ (⊤ * y).log = ⊤ + y.log

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

Result:
case inr.inl.inr.inr
y : ℝ≥0∞
y_real : 0 < y.toReal
⊢ (if y = 0 then 0 else ⊤) = ⊤

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

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

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

case inr.inr.inr.inr
x y : ℝ≥0∞
x_real : 0 < x.toReal
y_real : 0 < y.toReal
⊢ 0 < (x * y).toReal

Proof state:
case inr.inl.inl

⊢ (⊤ * 0).log = ⊤ + log 0

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

Result:
no goals

Proof state:
case inr.inl.inr.inl

⊢ (⊤ * ⊤).log = ⊤ + ⊤.log

Tactic:
simp

Result:
no goals

Proof state:
case inr.inl
y : ℝ≥0∞
⊢ (⊤ * y).log = ⊤ + y.log

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

Result:
case inr.inl.inl

⊢ (⊤ * 0).log = ⊤ + log 0

case inr.inl.inr.inl

⊢ (⊤ * ⊤).log = ⊤ + ⊤.log

case inr.inl.inr.inr
y : ℝ≥0∞
y_real : 0 < y.toReal
⊢ (⊤ * y).log = ⊤ + y.log

Proof state:
case inr.inl.inr.inr
y : ℝ≥0∞
y_real : 0 < y.toReal
⊢ ¬y = 0

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

Result:
no goals

Proof state:
case inr.inl
y : ℝ≥0∞
⊢ (⊤ * y).log = ⊤.log + y.log

Tactic:
rw [log_top]

Result:
case inr.inl
y : ℝ≥0∞
⊢ (⊤ * y).log = ⊤ + y.log

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

Tactic:
rw [log_pos_real' x_real]

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

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

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

Result:
case inl
y : ℝ≥0∞
⊢ (0 * y).log = log 0 + y.log

case inr.inl
y : ℝ≥0∞
⊢ (⊤ * y).log = ⊤.log + y.log

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

Proof state:
case inl
y : ℝ≥0∞
⊢ (0 * y).log = log 0 + y.log

Tactic:
simp

Result:
no goals

Proof state:
case inr.inr.inr.inr
x y : ℝ≥0∞
x_real : 0 < x.toReal
y_real : 0 < y.toReal
⊢ 0 < (x * y).toReal

Tactic:
rw [toReal_mul]

Result:
case inr.inr.inr.inr
x y : ℝ≥0∞
x_real : 0 < x.toReal
y_real : 0 < y.toReal
⊢ 0 < x.toReal * y.toReal