[GOAL]
a b : ℤ
⊢ natAbs a = natAbs b ↔ Associated a b
[PROOFSTEP]
refine' Int.natAbs_eq_natAbs_iff.trans _
[GOAL]
a b : ℤ
⊢ a = b ∨ a = -b ↔ Associated a b
[PROOFSTEP]
constructor
[GOAL]
case mp
a b : ℤ
⊢ a = b ∨ a = -b → Associated a b
[PROOFSTEP]
rintro (rfl | rfl)
[GOAL]
case mp.inl
a : ℤ
⊢ Associated a a
[PROOFSTEP]
rfl
[GOAL]
case mp.inr
b : ℤ
⊢ Associated (-b) b
[PROOFSTEP]
exact ⟨-1, by simp⟩
[GOAL]
b : ℤ
⊢ -b * ↑(-1) = b
[PROOFSTEP]
simp
[GOAL]
case mpr
a b : ℤ
⊢ Associated a b → a = b ∨ a = -b
[PROOFSTEP]
rintro ⟨u, rfl⟩
[GOAL]
case mpr.intro
a : ℤ
u : ℤˣ
⊢ a = a * ↑u ∨ a = -(a * ↑u)
[PROOFSTEP]
obtain rfl | rfl := Int.units_eq_one_or u
[GOAL]
case mpr.intro.inl
a : ℤ
⊢ a = a * ↑1 ∨ a = -(a * ↑1)
[PROOFSTEP]
exact Or.inl (by simp)
[GOAL]
a : ℤ
⊢ a = a * ↑1
[PROOFSTEP]
simp
[GOAL]
case mpr.intro.inr
a : ℤ
⊢ a = a * ↑(-1) ∨ a = -(a * ↑(-1))
[PROOFSTEP]
exact Or.inr (by simp)
[GOAL]
a : ℤ
⊢ a = -(a * ↑(-1))
[PROOFSTEP]
simp
