Rearranging using ENNReal.ofReal_mul, ENNReal.mul_inv_cancel

Stream: mathlib4

[Tommy Löfgren]

I think ENNReal.ofReal_mul and ENNReal.mul_inv_cancel would be useful tactics. The assumptions of ENNReal.mul_inv_cancel are here satisfied per construction and since we integrate over 0 to 1 we should have that NNReal.ofReal_mul work as well. Regarding the latter I tried to use conv => lhs etc. but did not manage to manipluate using the range of x. For the cancel part intutitively we should be able to multiply on both sides by the inverse of the rhs and cancel but or div_eq_one_iff_eq but I could not make it work. Could someone please help me.

import Mathlib

#check ENNReal.ofReal_mul
#check ENNReal.mul_inv_cancel

example (a b : ℝ) (h : ENNReal.ofReal b ≠ 0) (h' : ENNReal.ofReal b ≠ ⊤):  ∫⁻ (x : ℝ) in Set.Ioo 0 1,
        ENNReal.ofReal x * ENNReal.ofReal a = ENNReal.ofReal b
        ↔ 1/ ENNReal.ofReal b * ∫⁻ (x : ℝ) in Set.Ioo 0 1,
        ENNReal.ofReal (x * a) = 1 := by
        sorry