-- Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean
theorem log_strictMono : StrictMono log

Proof state:
case inr.inr
x y : ℝ≥0∞
h : x < y
x_real : 0 < x.toReal
⊢ (if x = 0 then ⊥ else if x = ⊤ then ⊤ else ↑(Real.log x.toReal)) <
    if y = 0 then ⊥ else if y = ⊤ then ⊤ else ↑(Real.log y.toReal)

Tactic:
simp only [(ENNReal.toReal_pos_iff.1 x_real).1.ne',
  (ENNReal.toReal_pos_iff.1 x_real).2.ne, if_false]

Result:
case inr.inr
x y : ℝ≥0∞
h : x < y
x_real : 0 < x.toReal
⊢ ↑(Real.log x.toReal) < if y = 0 then ⊥ else if y = ⊤ then ⊤ else ↑(Real.log y.toReal)

Proof state:
case inr.inr.inl
x : ℝ≥0∞
x_real : 0 < x.toReal
h : x < ⊥
⊢ False

Tactic:
exact not_lt_bot h

Result:
no goals

Proof state:
case inr.inr.inr.inr
x y : ℝ≥0∞
h : x < y
x_real : 0 < x.toReal
y_real : 0 < y.toReal
⊢ ↑(Real.log x.toReal) < if y = 0 then ⊥ else if y = ⊤ then ⊤ else ↑(Real.log y.toReal)

Tactic:
simp only [(ENNReal.toReal_pos_iff.1 y_real).1.ne', ↓reduceIte,
  (ENNReal.toReal_pos_iff.1 y_real).2.ne, EReal.coe_lt_coe_iff]

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

Proof state:
case inl
y : ℝ≥0∞
h : 0 < y
⊢ (if 0 = 0 then ⊥ else if 0 = ⊤ then ⊤ else ↑(Real.log (ENNReal.toReal 0))) <
    if y = 0 then ⊥ else if y = ⊤ then ⊤ else ↑(Real.log y.toReal)

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

Result:
case inl.inl
h : 0 < 0
⊢ (if 0 = 0 then ⊥ else if 0 = ⊤ then ⊤ else ↑(Real.log (ENNReal.toReal 0))) <
    if 0 = 0 then ⊥ else if 0 = ⊤ then ⊤ else ↑(Real.log (ENNReal.toReal 0))

case inl.inr.inl
h : 0 < ⊤
⊢ (if 0 = 0 then ⊥ else if 0 = ⊤ then ⊤ else ↑(Real.log (ENNReal.toReal 0))) <
    if ⊤ = 0 then ⊥ else if ⊤ = ⊤ then ⊤ else ↑(Real.log ⊤.toReal)

case inl.inr.inr
y : ℝ≥0∞
h : 0 < y
y_real : 0 < y.toReal
⊢ (if 0 = 0 then ⊥ else if 0 = ⊤ then ⊤ else ↑(Real.log (ENNReal.toReal 0))) <
    if y = 0 then ⊥ else if y = ⊤ then ⊤ else ↑(Real.log y.toReal)

Proof state:
x y : ℝ≥0∞
h : x < y
⊢ x.log < y.log

Tactic:
unfold log

Result:
x y : ℝ≥0∞
h : x < y
⊢ (if x = 0 then ⊥ else if x = ⊤ then ⊤ else ↑(Real.log x.toReal)) <
    if y = 0 then ⊥ else if y = ⊤ then ⊤ else ↑(Real.log y.toReal)

Proof state:
case inr.inr.inr.inl
x : ℝ≥0∞
x_real : 0 < x.toReal
h : x < ⊤
⊢ ↑(Real.log x.toReal) < if ⊤ = 0 then ⊥ else if ⊤ = ⊤ then ⊤ else ↑(Real.log ⊤.toReal)

Tactic:
simp

Result:
no goals

Proof state:
case inr.inl
y : ℝ≥0∞
h : ⊤ < y
⊢ False

Tactic:
exact not_top_lt h

Result:
no goals

Proof state:
case inl.inl
h : 0 < 0
⊢ (if 0 = 0 then ⊥ else if 0 = ⊤ then ⊤ else ↑(Real.log (ENNReal.toReal 0))) <
    if 0 = 0 then ⊥ else if 0 = ⊤ then ⊤ else ↑(Real.log (ENNReal.toReal 0))

Tactic:
exfalso

Result:
case inl.inl
h : 0 < 0
⊢ False

Proof state:
case inl.inr.inl
h : 0 < ⊤
⊢ (if 0 = 0 then ⊥ else if 0 = ⊤ then ⊤ else ↑(Real.log (ENNReal.toReal 0))) <
    if ⊤ = 0 then ⊥ else if ⊤ = ⊤ then ⊤ else ↑(Real.log ⊤.toReal)

Tactic:
simp

Result:
no goals

Proof state:
case inr.inr.inl
x : ℝ≥0∞
x_real : 0 < x.toReal
h : x < 0
⊢ False

Tactic:
rw [← ENNReal.bot_eq_zero] at h

Result:
case inr.inr.inl
x : ℝ≥0∞
x_real : 0 < x.toReal
h : x < ⊥
⊢ False

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

Tactic:
exact (ENNReal.toReal_lt_toReal (ENNReal.toReal_pos_iff.1 x_real).2.ne
  (ENNReal.toReal_pos_iff.1 y_real).2.ne).2 h

Result:
no goals

Proof state:
case inl.inr.inr
y : ℝ≥0∞
h : 0 < y
y_real : 0 < y.toReal
⊢ (if 0 = 0 then ⊥ else if 0 = ⊤ then ⊤ else ↑(Real.log (ENNReal.toReal 0))) <
    if y = 0 then ⊥ else if y = ⊤ then ⊤ else ↑(Real.log y.toReal)

Tactic:
simp [(ENNReal.toReal_pos_iff.1 y_real).1.ne',
  (ENNReal.toReal_pos_iff.1 y_real).2.ne, EReal.bot_lt_coe]

Result:
no goals

Proof state:
case inr.inl
y : ℝ≥0∞
h : ⊤ < y
⊢ (if ⊤ = 0 then ⊥ else if ⊤ = ⊤ then ⊤ else ↑(Real.log ⊤.toReal)) <
    if y = 0 then ⊥ else if y = ⊤ then ⊤ else ↑(Real.log y.toReal)

Tactic:
exfalso

Result:
case inr.inl
y : ℝ≥0∞
h : ⊤ < y
⊢ False

Proof state:
x y : ℝ≥0∞
h : x < y
⊢ (if x = 0 then ⊥ else if x = ⊤ then ⊤ else ↑(Real.log x.toReal)) <
    if y = 0 then ⊥ else if y = ⊤ then ⊤ else ↑(Real.log y.toReal)

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

Result:
case inl
y : ℝ≥0∞
h : 0 < y
⊢ (if 0 = 0 then ⊥ else if 0 = ⊤ then ⊤ else ↑(Real.log (ENNReal.toReal 0))) <
    if y = 0 then ⊥ else if y = ⊤ then ⊤ else ↑(Real.log y.toReal)

case inr.inl
y : ℝ≥0∞
h : ⊤ < y
⊢ (if ⊤ = 0 then ⊥ else if ⊤ = ⊤ then ⊤ else ↑(Real.log ⊤.toReal)) <
    if y = 0 then ⊥ else if y = ⊤ then ⊤ else ↑(Real.log y.toReal)

case inr.inr
x y : ℝ≥0∞
h : x < y
x_real : 0 < x.toReal
⊢ (if x = 0 then ⊥ else if x = ⊤ then ⊤ else ↑(Real.log x.toReal)) <
    if y = 0 then ⊥ else if y = ⊤ then ⊤ else ↑(Real.log y.toReal)

Proof state:
case inr.inr
x y : ℝ≥0∞
h : x < y
x_real : 0 < x.toReal
⊢ ↑(Real.log x.toReal) < if y = 0 then ⊥ else if y = ⊤ then ⊤ else ↑(Real.log y.toReal)

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

Result:
case inr.inr.inl
x : ℝ≥0∞
x_real : 0 < x.toReal
h : x < 0
⊢ ↑(Real.log x.toReal) < if 0 = 0 then ⊥ else if 0 = ⊤ then ⊤ else ↑(Real.log (ENNReal.toReal 0))

case inr.inr.inr.inl
x : ℝ≥0∞
x_real : 0 < x.toReal
h : x < ⊤
⊢ ↑(Real.log x.toReal) < if ⊤ = 0 then ⊥ else if ⊤ = ⊤ then ⊤ else ↑(Real.log ⊤.toReal)

case inr.inr.inr.inr
x y : ℝ≥0∞
h : x < y
x_real : 0 < x.toReal
y_real : 0 < y.toReal
⊢ ↑(Real.log x.toReal) < if y = 0 then ⊥ else if y = ⊤ then ⊤ else ↑(Real.log y.toReal)

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

Tactic:
apply Real.log_lt_log x_real

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

Proof state:
⊢ StrictMono log

Tactic:
intro x y h

Result:
x y : ℝ≥0∞
h : x < y
⊢ x.log < y.log

Proof state:
case inr.inr.inl
x : ℝ≥0∞
x_real : 0 < x.toReal
h : x < 0
⊢ ↑(Real.log x.toReal) < if 0 = 0 then ⊥ else if 0 = ⊤ then ⊤ else ↑(Real.log (ENNReal.toReal 0))

Tactic:
exfalso

Result:
case inr.inr.inl
x : ℝ≥0∞
x_real : 0 < x.toReal
h : x < 0
⊢ False

Proof state:
case inl.inl
h : 0 < 0
⊢ False

Tactic:
exact lt_irrefl 0 h

Result:
no goals