case inl
α : Type ?u.796201
β : Type ?u.796204
b c d : ℝ≥0∞
r p q : ℝ≥0
h : ⊤ ≤ b
ht : b = ⊤ → ⊤ = ⊤
⊢ ENNReal.toReal ⊤ ≤ ENNReal.toReal b

case inr
α : Type ?u.796201
β : Type ?u.796204
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b
ht : b = ⊤ → a = ⊤
ha : a ≠ ⊤
⊢ ENNReal.toReal a ≤ ENNReal.toReal b
α : Type ?u.796201
β : Type ?u.796204
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b
ht : b = ⊤ → a = ⊤
⊢ ENNReal.toReal a ≤ ENNReal.toReal b
rcases eq_or_ne a ∞ with rfl | ha
no goals
case inl
α : Type ?u.796201
β : Type ?u.796204
b c d : ℝ≥0∞
r p q : ℝ≥0
h : ⊤ ≤ b
ht : b = ⊤ → ⊤ = ⊤
⊢ ENNReal.toReal ⊤ ≤ ENNReal.toReal b
exact toReal_nonneg
no goals
case inr
α : Type ?u.796201
β : Type ?u.796204
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b
ht : b = ⊤ → a = ⊤
ha : a ≠ ⊤
⊢ ENNReal.toReal a ≤ ENNReal.toReal b
exact toReal_mono (mt ht ha) h