case intro
α : Type ?u.809256
β : Type ?u.809259
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ
b : ℝ≥0
⊢ ENNReal.ofReal a ≤ ↑b ↔ a ≤ ENNReal.toReal ↑b
α : Type ?u.809256
β : Type ?u.809259
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ
b : ℝ≥0∞
hb : b ≠ ⊤
⊢ ENNReal.ofReal a ≤ b ↔ a ≤ ENNReal.toReal b
lift b to ℝ≥0 using hb
no goals
case intro
α : Type ?u.809256
β : Type ?u.809259
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ
b : ℝ≥0
⊢ ENNReal.ofReal a ≤ ↑b ↔ a ≤ ENNReal.toReal ↑b
simpa [ENNReal.ofReal, ENNReal.toReal] using Real.toNNReal_le_iff_le_coe