case inl
x : ℝ
hx : 0 ≤ x
⊢ toNNReal x⁻¹ = (toNNReal x)⁻¹

case inr
x : ℝ
hx : x ≤ 0
⊢ toNNReal x⁻¹ = (toNNReal x)⁻¹
x : ℝ
⊢ toNNReal x⁻¹ = (toNNReal x)⁻¹
cases' le_total 0 x with hx hx
case inl
x : ℝ
hx : 0 ≤ x
⊢ toNNReal (↑(toNNReal x))⁻¹ = (toNNReal x)⁻¹
case inl
x : ℝ
hx : 0 ≤ x
⊢ toNNReal x⁻¹ = (toNNReal x)⁻¹
nth_rw 1 [← Real.coe_toNNReal x hx]
no goals
case inl
x : ℝ
hx : 0 ≤ x
⊢ toNNReal (↑(toNNReal x))⁻¹ = (toNNReal x)⁻¹
rw [← NNReal.coe_inv, Real.toNNReal_coe]
no goals
case inr
x : ℝ
hx : x ≤ 0
⊢ toNNReal x⁻¹ = (toNNReal x)⁻¹
rw [toNNReal_eq_zero.mpr hx, inv_zero, toNNReal_eq_zero.mpr (inv_nonpos.mpr hx)]