rw [Prod.eq_iff_fst_eq_snd_eq]
case intro
p q : ℤ × ℤ
hl : p.1 + p.2 = q.1 + q.2
hr : 2 * p.1 + p.2 = 2 * q.1 + q.2
⊢ p = q
case intro
p q : ℤ × ℤ
hl : p.1 + p.2 = q.1 + q.2
hr : 2 * p.1 + p.2 = 2 * q.1 + q.2
⊢ p.1 = q.1 ∧ p.2 = q.2