ENNReal fractions

Stream: Is there code for X?

[Peter]

I'm working with ENNReal right now, and I'm wondering if there's some way to prove this in one or two lines:

import Mathlib

lemma problem (a b c : ENNReal) : a / (c * d) = a / c / d := by sorry

It seems this should be a one-liner, but can't find anything in Mathlib.

[Aaron Liu]

#new members > Performing arithmetic with ENNReals

[Kenny Lau]

import Mathlib

open ENNReal

lemma problem (h : ∀ (a c d : ENNReal), a / (c * d) = a / c / d) : False := by
  specialize h 1 0 ∞
  simp at h

[Aaron Liu]

yeah that's a problem

[Kenny Lau]

yeah, it's a bit hard to prove False unless you were using a version of mathlib a few months ago