a b : ℤ
⊢ a = b ∨ a = -b ↔ Associated a b
a b : ℤ
⊢ natAbs a = natAbs b ↔ Associated a b
refine' Int.natAbs_eq_natAbs_iff.trans _
case mp
a b : ℤ
⊢ a = b ∨ a = -b → Associated a b

case mpr
a b : ℤ
⊢ Associated a b → a = b ∨ a = -b
a b : ℤ
⊢ a = b ∨ a = -b ↔ Associated a b
constructor
case mp.inl
a : ℤ
⊢ Associated a a

case mp.inr
b : ℤ
⊢ Associated (-b) b
case mp
a b : ℤ
⊢ a = b ∨ a = -b → Associated a b
rintro (rfl | rfl)
no goals
case mp.inl
a : ℤ
⊢ Associated a a
rfl
no goals
case mp.inr
b : ℤ
⊢ Associated (-b) b
exact ⟨-1, by simp⟩
no goals
b : ℤ
⊢ -b * ↑(-1) = b
simp
case mpr.intro
a : ℤ
u : ℤˣ
⊢ a = a * ↑u ∨ a = -(a * ↑u)
case mpr
a b : ℤ
⊢ Associated a b → a = b ∨ a = -b
rintro ⟨u, rfl⟩
case mpr.intro.inl
a : ℤ
⊢ a = a * ↑1 ∨ a = -(a * ↑1)

case mpr.intro.inr
a : ℤ
⊢ a = a * ↑(-1) ∨ a = -(a * ↑(-1))
case mpr.intro
a : ℤ
u : ℤˣ
⊢ a = a * ↑u ∨ a = -(a * ↑u)
obtain rfl | rfl := Int.units_eq_one_or u
no goals
case mpr.intro.inl
a : ℤ
⊢ a = a * ↑1 ∨ a = -(a * ↑1)
exact Or.inl (by simp)
no goals
a : ℤ
⊢ a = a * ↑1
simp
no goals
case mpr.intro.inr
a : ℤ
⊢ a = a * ↑(-1) ∨ a = -(a * ↑(-1))
exact Or.inr (by simp)
no goals
a : ℤ
⊢ a = -(a * ↑(-1))
simp