case inl
x : ℝ
h : 0 ≤ x
⊢ ↑x = ↑↑(Real.toNNReal x) - ↑↑(Real.toNNReal (-x))

case inr
x : ℝ
h : x ≤ 0
⊢ ↑x = ↑↑(Real.toNNReal x) - ↑↑(Real.toNNReal (-x))
x : ℝ
⊢ ↑x = ↑↑(Real.toNNReal x) - ↑↑(Real.toNNReal (-x))
rcases le_total 0 x with (h | h)
case inl.intro
x : ℝ≥0
⊢ ↑↑x = ↑↑(Real.toNNReal ↑x) - ↑↑(Real.toNNReal (-↑x))
case inl
x : ℝ
h : 0 ≤ x
⊢ ↑x = ↑↑(Real.toNNReal x) - ↑↑(Real.toNNReal (-x))
lift x to ℝ≥0 using h
case inl.intro
x : ℝ≥0
⊢ ↑↑x = ↑↑x
case inl.intro
x : ℝ≥0
⊢ ↑↑x = ↑↑(Real.toNNReal ↑x) - ↑↑(Real.toNNReal (-↑x))
rw [Real.toNNReal_of_nonpos (neg_nonpos.mpr x.coe_nonneg), Real.toNNReal_coe, ENNReal.coe_zero,
  coe_ennreal_zero, sub_zero]
no goals
case inl.intro
x : ℝ≥0
⊢ ↑↑x = ↑↑x
rfl
case inr.hr
x : ℝ
h : x ≤ 0
⊢ 0 ≤ -x
case inr
x : ℝ
h : x ≤ 0
⊢ ↑x = ↑↑(Real.toNNReal x) - ↑↑(Real.toNNReal (-x))
rw [Real.toNNReal_of_nonpos h, ENNReal.coe_zero, coe_ennreal_zero, coe_nnreal_eq_coe_real,
  Real.coe_toNNReal, zero_sub, coe_neg, neg_neg]
no goals
case inr.hr
x : ℝ
h : x ≤ 0
⊢ 0 ≤ -x
exact neg_nonneg.2 h