case intro
α : Type ?u.795291
β : Type ?u.795294
b c d : ℝ≥0∞
r p q : ℝ≥0
hb : b ≠ ⊤
a : ℝ≥0
⊢ ENNReal.toReal ↑a ≤ ENNReal.toReal b ↔ ↑a ≤ b
α : Type ?u.795291
β : Type ?u.795294
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.795291
β : Type ?u.795294
c d : ℝ≥0∞
r p q a b : ℝ≥0
⊢ ENNReal.toReal ↑a ≤ ENNReal.toReal ↑b ↔ ↑a ≤ ↑b
case intro
α : Type ?u.795291
β : Type ?u.795294
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.795291
β : Type ?u.795294
c d : ℝ≥0∞
r p q a b : ℝ≥0
⊢ ENNReal.toReal ↑a ≤ ENNReal.toReal ↑b ↔ ↑a ≤ ↑b
norm_cast