-- Mathlib/Data/ENNReal/Real.lean
theorem trichotomy₂ {p q : ℝ≥0∞} (hpq : p ≤ q) :
    p = 0 ∧ q = 0 ∨
      p = 0 ∧ q = ∞ ∨
        p = 0 ∧ 0 < q.toReal ∨
          p = ∞ ∧ q = ∞ ∨
            0 < p.toReal ∧ q = ∞ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal

Proof state:
case inr
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ⊤ ∨
      p = 0 ∧ 0 < q.toReal ∨ p = ⊤ ∧ q = ⊤ ∨ 0 < p.toReal ∧ q = ⊤ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal

Tactic:
rcases eq_or_lt_of_le (le_top : q ≤ ∞) with (rfl | hq)

Result:
case inr.inl
p : ℝ≥0∞
hp : 0 < p
hpq : p ≤ ⊤
⊢ p = 0 ∧ ⊤ = 0 ∨
    p = 0 ∧ ⊤ = ⊤ ∨
      p = 0 ∧ 0 < ⊤.toReal ∨ p = ⊤ ∧ ⊤ = ⊤ ∨ 0 < p.toReal ∧ ⊤ = ⊤ ∨ 0 < p.toReal ∧ 0 < ⊤.toReal ∧ p.toReal ≤ ⊤.toReal

case inr.inr
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ⊤
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ⊤ ∨
      p = 0 ∧ 0 < q.toReal ∨ p = ⊤ ∧ q = ⊤ ∨ 0 < p.toReal ∧ q = ⊤ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal

Proof state:
case inl
q : ℝ≥0∞
hpq : 0 ≤ q
⊢ 0 = 0 ∧ q = 0 ∨
    0 = 0 ∧ q = ⊤ ∨
      0 = 0 ∧ 0 < q.toReal ∨
        0 = ⊤ ∧ q = ⊤ ∨ 0 < ENNReal.toReal 0 ∧ q = ⊤ ∨ 0 < ENNReal.toReal 0 ∧ 0 < q.toReal ∧ ENNReal.toReal 0 ≤ q.toReal

Tactic:
simpa using q.trichotomy

Result:
no goals

Proof state:
case inr.inr.h.h.h.h.h
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ⊤
hq' : 0 < q
hp' : p < ⊤
⊢ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal

Tactic:
simp [ENNReal.toReal_mono hq.ne hpq, ENNReal.toReal_pos_iff, hp, hp', hq', hq]

Result:
no goals

Proof state:
case inr.inr
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ⊤
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ⊤ ∨
      p = 0 ∧ 0 < q.toReal ∨ p = ⊤ ∧ q = ⊤ ∨ 0 < p.toReal ∧ q = ⊤ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal

Tactic:
repeat' right

Result:
case inr.inr.h.h.h.h.h
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ⊤
⊢ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal

Proof state:
case inr.inl
p : ℝ≥0∞
hp : 0 < p
hpq : p ≤ ⊤
⊢ p = 0 ∧ ⊤ = 0 ∨
    p = 0 ∧ ⊤ = ⊤ ∨
      p = 0 ∧ 0 < ⊤.toReal ∨ p = ⊤ ∧ ⊤ = ⊤ ∨ 0 < p.toReal ∧ ⊤ = ⊤ ∨ 0 < p.toReal ∧ 0 < ⊤.toReal ∧ p.toReal ≤ ⊤.toReal

Tactic:
simpa using p.trichotomy

Result:
no goals

Proof state:
case inr.inr.h.h.h.h.h
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ⊤
⊢ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal

Tactic:
have hq' : 0 < q := lt_of_lt_of_le hp hpq

Result:
case inr.inr.h.h.h.h.h
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ⊤
hq' : 0 < q
⊢ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal

Proof state:
p q : ℝ≥0∞
hpq : p ≤ q
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ⊤ ∨
      p = 0 ∧ 0 < q.toReal ∨ p = ⊤ ∧ q = ⊤ ∨ 0 < p.toReal ∧ q = ⊤ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal

Tactic:
rcases eq_or_lt_of_le (bot_le : 0 ≤ p) with ((rfl : 0 = p) | (hp : 0 < p))

Result:
case inl
q : ℝ≥0∞
hpq : 0 ≤ q
⊢ 0 = 0 ∧ q = 0 ∨
    0 = 0 ∧ q = ⊤ ∨
      0 = 0 ∧ 0 < q.toReal ∨
        0 = ⊤ ∧ q = ⊤ ∨ 0 < ENNReal.toReal 0 ∧ q = ⊤ ∨ 0 < ENNReal.toReal 0 ∧ 0 < q.toReal ∧ ENNReal.toReal 0 ≤ q.toReal

case inr
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ⊤ ∨
      p = 0 ∧ 0 < q.toReal ∨ p = ⊤ ∧ q = ⊤ ∨ 0 < p.toReal ∧ q = ⊤ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal

Proof state:
case inr.inr.h.h.h.h.h
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ⊤
hq' : 0 < q
⊢ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal

Tactic:
have hp' : p < ∞ := lt_of_le_of_lt hpq hq

Result:
case inr.inr.h.h.h.h.h
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ⊤
hq' : 0 < q
hp' : p < ⊤
⊢ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal

Proof state:
case inr.inr.h.h.h.h
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ⊤
⊢ 0 < p.toReal ∧ q = ⊤ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal

Tactic:
right

Result:
case inr.inr.h.h.h.h.h
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ⊤
⊢ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal