ENNReal of nonnegative is equal to said nonnegative

Stream: Is there code for X?

[Peter]

Is there some way of proving this statement:

lemma step2 (num : Nat) (den : PNat) (h : 2 * num < den) (h1: (0 : ℝ) ≤ (↑↑den + 2 * ↑num) / (↑↑den - 2 * ↑num)):
(↑↑den + 2 * ↑num) / (↑↑den - 2 * ↑num) = ENNReal.ofReal ((↑↑den + 2 * ↑num) / (↑↑den - 2 * ↑num)) := by sorry

I've tried rewriting with ENNReal.ofReal_eq_coe_nnreal, but not sure how to deal with the coercions. Thanks!

[Kevin Buzzard]

Can you post a #mwe? Right now ↑↑den could be parsed in multiple ways.

[Robin Arnez]

I'm pretty sure

import Mathlib

lemma step2 (num : Nat) (den : PNat) (h : 2 * num < den) (h1: (0 : ℝ) ≤ (↑↑den + 2 * ↑num) / (↑↑den - 2 * ↑num)):
    (↑↑den + 2 * ↑num) / (↑↑den - 2 * ↑num) = ENNReal.ofReal ((↑↑den + 2 * ↑num) / (↑↑den - 2 * ↑num)) := by
  sorry

works correctly (↑↑ being PNat => Nat => Real)

[Kevin Buzzard]

It is annoying that this isn't easier in 2025. Here's my approach, which you can do without knowing the names of any lemmas, but you occasionally have to ask the system to find the lemmas for you.

import Mathlib

--example (a b : ℝ) : ENNReal.ofReal (a / b) = (ENNReal.ofReal a) / (ENNReal.ofReal b) := by apply?
-- leads me to `ENNReal.ofReal_div_of_pos`

lemma step2 (num : Nat) (den : PNat) (h : 2 * num < den) (h1: (0 : ℝ) ≤ (↑↑den + 2 * ↑num) / (↑↑den - 2 * ↑num)):
    (↑↑den + 2 * ↑num) / (↑↑den - 2 * ↑num) = ENNReal.ofReal ((↑↑den + 2 * ↑num) / (↑↑den - 2 * ↑num)) := by
  rw [ENNReal.ofReal_div_of_pos]
  · congr
    norm_cast
  · have foo : 2 * (num : ℝ) < (den : ℕ) := by exact_mod_cast h
    exact sub_pos.mpr foo -- found with `exact?`