α : Type ?u.25525
β : Type ?u.25528
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ
h : ENNReal.toReal (ENNReal.ofReal a) = a
⊢ 0 ≤ ENNReal.toReal (ENNReal.ofReal a)
α : Type ?u.25525
β : Type ?u.25528
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ
h : ENNReal.toReal (ENNReal.ofReal a) = a
⊢ 0 ≤ a
rw [← h]
no goals
α : Type ?u.25525
β : Type ?u.25528
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ
h : ENNReal.toReal (ENNReal.ofReal a) = a
⊢ 0 ≤ ENNReal.toReal (ENNReal.ofReal a)
exact toReal_nonneg