rw [ha, hb]
case intro.intro
x y a : ℤ
ha : x = a + a
b : ℤ
hb : y = b + b
⊢ ∃ r, x ^ 2 + y ^ 2 = r + r
case intro.intro
x y a : ℤ
ha : x = a + a
b : ℤ
hb : y = b + b
⊢ ∃ r, (a + a) ^ 2 + (b + b) ^ 2 = r + r