no goals
α : Type ?u.816393
β : Type ?u.816396
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ
hx : 0 < x
⊢ (ENNReal.ofReal x)⁻¹ = ENNReal.ofReal x⁻¹
rw [ENNReal.ofReal, ENNReal.ofReal, ← @coe_inv (Real.toNNReal x) (by simp [hx]), coe_eq_coe,
  ← Real.toNNReal_inv]
no goals
α : Type ?u.816393
β : Type ?u.816396
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ
hx : 0 < x
⊢ Real.toNNReal x ≠ 0
simp [hx]