use (2 * a ^ 2 + 2 * b ^ 2)
case intro.intro
x y a : ℤ
ha : x = a + a
b : ℤ
hb : y = b + b
⊢ ∃ r, (a + a) ^ 2 + (b + b) ^ 2 = r + r
case h
x y a : ℤ
ha : x = a + a
b : ℤ
hb : y = b + b
⊢ (a + a) ^ 2 + (b + b) ^ 2 = 2 * a ^ 2 + 2 * b ^ 2 + (2 * a ^ 2 + 2 * b ^ 2)