case inl
a : ℤ
h : a = ↑(natAbs a)
⊢ ∃ u x, ↑(natAbs a) = u * a

case inr
a : ℤ
h : a = -↑(natAbs a)
⊢ ∃ u x, ↑(natAbs a) = u * a
a : ℤ
⊢ ∃ u x, ↑(natAbs a) = u * a
cases' natAbs_eq a with h h
case inl
a : ℤ
h : a = ↑(natAbs a)
⊢ ↑(natAbs a) = 1 * a
case inl
a : ℤ
h : a = ↑(natAbs a)
⊢ ∃ u x, ↑(natAbs a) = u * a
use 1, isUnit_one
no goals
case inl
a : ℤ
h : a = ↑(natAbs a)
⊢ ↑(natAbs a) = 1 * a
rw [← h, one_mul]
case inr
a : ℤ
h : a = -↑(natAbs a)
⊢ ↑(natAbs a) = -1 * a
case inr
a : ℤ
h : a = -↑(natAbs a)
⊢ ∃ u x, ↑(natAbs a) = u * a
use -1, isUnit_one.neg
case inr
a : ℤ
h : a = -↑(natAbs a)
⊢ -a = -1 * a
case inr
a : ℤ
h : a = -↑(natAbs a)
⊢ ↑(natAbs a) = -1 * a
rw [← neg_eq_iff_eq_neg.mpr h]
no goals
case inr
a : ℤ
h : a = -↑(natAbs a)
⊢ -a = -1 * a
simp only [neg_mul, one_mul]