α : Type ?u.25366
β : Type ?u.25369
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : ENNReal.ofReal (ENNReal.toReal a) = a
⊢ ENNReal.ofReal (ENNReal.toReal a) ≠ ⊤
α : Type ?u.25366
β : Type ?u.25369
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : ENNReal.ofReal (ENNReal.toReal a) = a
⊢ a ≠ ⊤
rw [← h]
no goals
α : Type ?u.25366
β : Type ?u.25369
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : ENNReal.ofReal (ENNReal.toReal a) = a
⊢ ENNReal.ofReal (ENNReal.toReal a) ≠ ⊤
exact ofReal_ne_top