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