Having trouble proving something elementary in ENNReal

Stream: new members

[Alex Zani]

I'm trying to prove this elementary thing in ENNReal and I can't figure out how.

def p : ℝ≥0∞ := 0.5
theorem h : p ≤ 1 := by
  unfold p
  have hp : p ≠ ∞ := by unfold p; exact Ne.symm (ne_of_beq_false rfl)
  lift p to ℝ using hp

I tried lifting p to the reals, but that doesn't work. (I assume because p is bound)
I was able to figure things out if I defined p this way:

def p : ℝ≥0∞ := ENNReal.ofReal 0.5

but that feels like it shouldn't be necessary.

[Aaron Liu]

does norm_num work?

[Alex Zani]

Aaron Liu said:

does norm_num work?

Nope. It does nothing.

[Aaron Liu]

Someone should write a norm_num extension for ENNReal

[Eric Wieser]

Not possible, norm_num only supports division in division rings not division semirings

[Eric Wieser]

Unless you revive #9915

[Aaron Liu]

Should I revive #9915?

[Aaron Liu]

It seems to be over a year old

[Kevin Buzzard]

(deleted)

[Notification Bot]

This topic was moved here from #lean4 > Having trouble proving something elementary in ENNReal by Kevin Buzzard.

[Kevin Buzzard]

@Alex Zani the #lean4 channel is for questions about core Lean itself, not questions which involve mathlib. Your question would be easier to answer if you wrote it as a #mwe .

[Eric Wieser]

Aaron Liu said:

Should I revive #9915?

It needs reviving, but I think Mario and I had some private conversation about it that I probably should find and share first, to save you making the same mistakes