norm_num on ENNReal

Stream: mathlib4

[Floris van Doorn]

It would be nice if norm_num can deal with goals in ENNReal, e.g. the following is currently quite painful

import Mathlib

open scoped ENNReal NNReal
example : ((2 : ℝ≥0∞) * 2 ^ (-4 : ℤ) + 2 ^ (- 2 : ℤ)) ≤ (2 : ℝ≥0∞) ^ (-1 : ℤ) := by
  change ((2 : ℝ≥0) : ℝ≥0∞) * (2 : ℝ≥0) ^ (-4 : ℤ) + (2 : ℝ≥0) ^ (-2 : ℤ) ≤ (2 : ℝ≥0) ^ (-1 : ℤ)
  repeat rw [← ENNReal.coe_zpow (show (2 : ℝ≥0) ≠ 0 by norm_num)]
  rw_mod_cast [← NNReal.coe_le_coe]; norm_num

[Yaël Dillies]

This is due to norm_num representing numerals as a Rat. @Eric Wieser (and I, a bit) has thought about this issue

[Eric Wieser]

I have an open (incomplete) PR that adds support to norm_num for semifields like NNReal, but even this wouldn't help on ENNReal, which isn't a semifield

[Floris van Doorn]

The above proof uses norm_num on NNReal, presumably by immediately transferring it to Real?

[Eric Wieser]

norm_num works fine for the Semiring operations on NNReal (by transferring to Nat), just not division (without my PR)