apply_fun (λ e => e - (p.1 + p.2)) at hr
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
case intro
p q : ℤ × ℤ
hl : p.1 + p.2 = q.1 + q.2
hr : 2 * p.1 + p.2 - (p.1 + p.2) = 2 * q.1 + q.2 - (p.1 + p.2)
⊢ p.1 = q.1 ∧ p.2 = q.2