case intro
α : Type ?u.796547
β : Type ?u.796550
b c d : ℝ≥0∞
r p q : ℝ≥0
hb : b ≠ ⊤
a : ℝ≥0
⊢ ENNReal.toReal ↑a < ENNReal.toReal b ↔ ↑a < b
α : Type ?u.796547
β : Type ?u.796550
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ ENNReal.toReal a < ENNReal.toReal b ↔ a < b
lift a to ℝ≥0 using ha
case intro.intro
α : Type ?u.796547
β : Type ?u.796550
c d : ℝ≥0∞
r p q a b : ℝ≥0
⊢ ENNReal.toReal ↑a < ENNReal.toReal ↑b ↔ ↑a < ↑b
case intro
α : Type ?u.796547
β : Type ?u.796550
b c d : ℝ≥0∞
r p q : ℝ≥0
hb : b ≠ ⊤
a : ℝ≥0
⊢ ENNReal.toReal ↑a < ENNReal.toReal b ↔ ↑a < b
lift b to ℝ≥0 using hb
no goals
case intro.intro
α : Type ?u.796547
β : Type ?u.796550
c d : ℝ≥0∞
r p q a b : ℝ≥0
⊢ ENNReal.toReal ↑a < ENNReal.toReal ↑b ↔ ↑a < ↑b
norm_cast