case intro
α : Type ?u.104939
β : Type ?u.104942
a✝ b✝ c d : ℝ≥0∞
r p q b a : ℝ≥0
h : ↑a ≤ ↑b
⊢ ENNReal.toReal ↑a ≤ ↑b
α : Type ?u.104939
β : Type ?u.104942
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
b : ℝ≥0
h : a ≤ ↑b
⊢ ENNReal.toReal a ≤ ↑b
lift a to ℝ≥0 using ne_top_of_le_ne_top coe_ne_top h
no goals
case intro
α : Type ?u.104939
β : Type ?u.104942
a✝ b✝ c d : ℝ≥0∞
r p q b a : ℝ≥0
h : ↑a ≤ ↑b
⊢ ENNReal.toReal ↑a ≤ ↑b
simpa using h