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