apply_fun (λ e => e - q.1) at hl
case intro
p q : ℤ × ℤ
hl : q.1 + p.2 = q.1 + q.2
hr : p.1 = q.1
⊢ p.1 = q.1 ∧ p.2 = q.2
case intro
p q : ℤ × ℤ
hr : p.1 = q.1
hl : q.1 + p.2 - q.1 = q.1 + q.2 - q.1
⊢ p.1 = q.1 ∧ p.2 = q.2