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