Theorem: Int.natAbs_eq' (Util/Arithmetic.lean)

State before:
a b c d : ℤ
⊢ ↑(|a|) = a ∨ ↑(|a|) = -a
Tactic:
conv => lhs; rewrite [eq_comm]
State after:
a b c d : ℤ
⊢ a = ↑(|a|) ∨ ↑(|a|) = -a

State before:
a b c d : ℤ
⊢ a = ↑(|a|) ∨ ↑(|a|) = -a
Tactic:
conv => rhs; rewrite [eq_comm, Int.neg_eq_comm, eq_comm]
State after:
a b c d : ℤ
⊢ a = ↑(|a|) ∨ a = -↑(|a|)

State before:
a b c d : ℤ
⊢ a = ↑(|a|) ∨ a = -↑(|a|)
Tactic:
exact natAbs_eq a
State after:
no goals